2024/12/10 by Amtoft, Torben, Banerjee, Anindya
#FOS: Computer and information sciences #Programming Languages (cs.PL)
paper · doi:10.48550/arxiv.2412.07086
When proving the correctness of a method for slicing probabilistic programs, it was previously discovered by the authors that for a fixed point iteration to work one needs a non-standard starting point for the iteration. This paper presents and explores this technique in a general setting; it states the lemmas that must be established to use the technique to prove the correctness of a program transformation, and sketches how to apply the technique to slicing of probabilistic programs.