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.
Original language | Undefined/Unknown |
---|---|
Title of host publication | Mathematical Foundations of Computer Science 1993, 18th International Symposium, MFCS'93, Gdansk, Poland, August 30 - September 3, 1993, Proceedings |
Pages | 32-67 |
Number of pages | 36 |
DOIs | |
Publication status | Published - 3 Sept 1993 |
Event | 18th International Symposium, MFCS'93 Gdańsk, Poland - Gdańsk, Poland Duration: 30 Aug 1993 → 3 Sept 1993 Conference number: 18 https://link.springer.com/book/10.1007/3-540-57182-5 |
Conference
Conference | 18th International Symposium, MFCS'93 Gdańsk, Poland |
---|---|
Abbreviated title | MFSC 1993 |
Country/Territory | Poland |
City | Gdańsk |
Period | 30/08/93 → 3/09/93 |
Internet address |
Keywords / Materials (for Non-textual outputs)
- Type Theory
- Function Component
- Correctness Proof
- True Predicate
- Elimination Rule