Re: CATS Re: Categorical model for Floyd-Hoare logic?

15 Feb 1998


      A semantics of loops (and while-loops) where objects are types (not
predicates) can be found in

@InProceedings(Jay91d,
	Author={Jay, C.B.},
	Title={Fixpoint and loop constructions as colimits},
	Booktitle="Proceedings Summer Conference on Category Theory, 
	Como 1990",
	Editor="A.~Carboni, M.C.~Pedicchio and G.~Rosolini",
	Series=Lecture Notes in Mathematics,
	Volume=1488,
	Publisher=sv,
	Year=1991,
	Pages={187--192})

and their use to account for tail-recursion is in

@Article(Jay93a,
	Author={Jay, C.B.},
	Title={Tail recursion through universal invariants},
	Journal=Theoretcial Computer Science,
	Volume=115,
	Year=1993,
	Pages={151--189})

Barry Jay