Deliverables: A Categorial Approach to Program Development in Type Theory

James McKinna; Rod M. Burstall

doi:10.1007/3-540-57182-53

Deliverables: A Categorial Approach to Program Development in Type Theory

James McKinna, Rod M. Burstall

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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	https://doi.org/10.1007/3-540-57182-53
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	https://link.springer.com/book/10.1007/3-540-57182-5

Keywords / Materials (for Non-textual outputs)

Type Theory
Function Component
Correctness Proof
True Predicate
Elimination Rule

Access to Document

10.1007/3-540-57182-53

https://doi.org/10.1007/3-540-57182-53

Cite this

@inproceedings{d5e6765000064d5886828cb397c8902e,

title = "Deliverables: A Categorial Approach to Program Development in Type Theory",

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.",

keywords = "Type Theory, Function Component, Correctness Proof, True Predicate, Elimination Rule",

author = "James McKinna and Burstall, \{Rod M.\}",

year = "1993",

month = sep,

day = "3",

doi = "10.1007/3-540-57182-53",

language = "Undefined/Unknown",

pages = "32--67",

booktitle = "Mathematical Foundations of Computer Science 1993, 18th International Symposium, MFCS'93, Gdansk, Poland, August 30 - September 3, 1993, Proceedings",

note = "18th International Symposium, MFCS'93 Gda{\'n}sk, Poland ; Conference date: 30-08-1993 Through 03-09-1993",

url = "https://link.springer.com/book/10.1007/3-540-57182-5",

}

McKinna, J & Burstall, RM 1993, Deliverables: A Categorial Approach to Program Development in Type Theory. in Mathematical Foundations of Computer Science 1993, 18th International Symposium, MFCS'93, Gdansk, Poland, August 30 - September 3, 1993, Proceedings. pp. 32-67, 18th International Symposium, MFCS'93 Gdańsk, Poland, Gdańsk, Poland, 30/08/93. https://doi.org/10.1007/3-540-57182-53

TY - GEN

T1 - Deliverables: A Categorial Approach to Program Development in Type Theory

AU - McKinna, James

AU - Burstall, Rod M.

N1 - Conference code: 18

PY - 1993/9/3

Y1 - 1993/9/3

N2 - 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.

AB - 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.

KW - Type Theory

KW - Function Component

KW - Correctness Proof

KW - True Predicate

KW - Elimination Rule

U2 - 10.1007/3-540-57182-53

DO - 10.1007/3-540-57182-53

M3 - Conference contribution

SP - 32

EP - 67

BT - Mathematical Foundations of Computer Science 1993, 18th International Symposium, MFCS'93, Gdansk, Poland, August 30 - September 3, 1993, Proceedings

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

Y2 - 30 August 1993 through 3 September 1993

ER -