"Judgements" for Syntactic Definition of Fixpoint Programs (2007)
Talk At Calculus, Yoshiki Kinoshita, If R, R Are Comm
In order to give a precise syntactic definition of fixpoint programs, we introduced "judgements" similar to those used in typed #-calculus. Hoare-He-Sanders[1] gave the following inductive...