Paper: New foundations for fixpoint computations (at LICS 1990)

Authors: Roy L. Crole Andrew M. Pitts

Abstract

A novel higher-order typed constructive predicate logic for fixpoint computations which exploits the categorical semantics of computations introduced by E. Moggi (1989) and contains a strong version of P. Martin-Lof's (1983) iteration type is introduced. 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

BibTeX

  @InProceedings{CrolePitts-Newfoundationsforfi,
    author = 	 {Roy L. Crole and Andrew M. Pitts},
    title = 	 {New foundations for fixpoint computations},
    booktitle =  {Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990)},
    year =	 {1990},
    month =	 {June}, 
    pages =      {489--497},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }