Do-it-yourself type theory
- 1 March 1989
- journal article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 1 (1) , 19-84
- https://doi.org/10.1007/bf01887198
Abstract
This paper provides a tutorial introduction to a constructive theory of types based on, but incorporating some extensions to, that originally developed by Per Martin-Löf. The emphasis is on the relevance of the theory to the construction of computer programs and, in particular, on the formal relationship between program and data structure. Topics discussed include the principle of propositions as types, free types, congruence types, types with information loss and mutually recursive types. Several examples of program development within the theory are also discussed in detail.Keywords
This publication has 18 references indexed in Scilit:
- Constructive Mathematics and Computer ProgrammingPublished by Elsevier ,2014
- A theory of type polymorphism in programmingPublished by Elsevier ,2003
- Derivation of a parsing algorithm in martin-löf's theory of typesScience of Computer Programming, 1987
- Constructing recursion operators in intuitionistic type theoryJournal of Symbolic Computation, 1986
- A natural extension of natural deductionThe Journal of Symbolic Logic, 1984
- Finding repeated elementsScience of Computer Programming, 1982
- Proofs and the Meaning and Completeness of the Logical ConstantsPublished by Springer Nature ,1979
- Fast Pattern Matching in StringsSIAM Journal on Computing, 1977
- An Intuitionistic Theory of Types: Predicative PartPublished by Elsevier ,1975
- 3. Investigations into Logical DeductionPublished by Elsevier ,1969