Deliverables: A Categorial Approach to Program Development in Type Theory

James McKinna, Rod M. Burstall

Research output: Chapter in Book/Report/Conference proceedingConference contribution

10 Citations (Scopus)


We describe a method for formally developing functional programs using the “propositions as types” paradigm. The idea is that a function together with its proof of correctness forms a morphism in a category whose objects are input/output specifications. The functionproof pairs, called “deliverables”, can be combined by the operations of a cartesian closed category, indeed by the same operations which are usually used to combine functions. The method has been implemented using the Lego proof assistant and tried on some examples.
Original languageEnglish
Title of host publicationMathematical Foundations of Computer Science 1993. MFCS 1993
Number of pages36
ISBN (Electronic)9783540479277
ISBN (Print)9783540571827
Publication statusPublished - 1993

Publication series

NameLecture Notes in Computer Science


  • Type Theory
  • Function Component
  • Correctness Proof
  • True Predicate
  • Elimination Rule


Dive into the research topics of 'Deliverables: A Categorial Approach to Program Development in Type Theory'. Together they form a unique fingerprint.

Cite this