Technical reports

New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic

Roy L. Crole, Andrew M. Pitts

August 1990, 37 pages

DOI: 10.48456/tr-204

Abstract

This paper introduces a new higher-order typed constructive predicate logic for fixpoint computations, which exploits the categorical semantics of computations introduced by Moggi and contains a strong version of Martin Löf’s ‘iteration type’. The type system enforces a separation of computations from values. The logic contains a novel form of fixpoint induction and can express partial and total correctness statements about evaluation of computations to values. The constructive nature of the logic is witnessed by strong metalogical properties which are proved using a category-theoretic version of the ‘logical relations’ method.

Full text

PS (0.1 MB)

BibTeX record

@TechReport{UCAM-CL-TR-204,
  author =	 {Crole, Roy L. and Pitts, Andrew M.},
  title = 	 {{New foundations for fixpoint computations:
         	   FIX-hyperdoctrines and the FIX-logic}},
  year = 	 1990,
  month = 	 aug,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-204.ps.gz},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-204},
  number = 	 {UCAM-CL-TR-204}
}