Edinburgh Research Explorer

Deliverables: A Categorial Approach to Program Development in Type Theory

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

Original languageUndefined/Unknown
Title of host publicationMathematical Foundations of Computer Science 1993, 18th International Symposium, MFCS'93, Gdansk, Poland, August 30 - September 3, 1993, Proceedings
Pages32-67
Number of pages36
DOIs
Publication statusPublished - 3 Sep 1993
Event18th International Symposium, MFCS'93 Gdańsk, Poland - Gdańsk, Poland
Duration: 30 Aug 19933 Sep 1993
Conference number: 18
https://link.springer.com/book/10.1007/3-540-57182-5

Conference

Conference18th International Symposium, MFCS'93 Gdańsk, Poland
Abbreviated titleMFSC 1993
CountryPoland
CityGdańsk
Period30/08/933/09/93
Internet address

Abstract

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.

    Research areas

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

Event

18th International Symposium, MFCS'93 Gdańsk, Poland

30/08/933/09/93

Gdańsk, Poland

Event: Conference

ID: 95267018