Jump to ContentJump to Main Navigation
Handbook of Logic in Computer Science: Volume 5. Algebraic and Logical Structures$
Users without a subscription are not able to see the full content.

S. Abramsky, Dov M. Gabbay, and T. S. E. Maibaum

Print publication date: 2001

Print ISBN-13: 9780198537816

Published to Oxford Scholarship Online: November 2020

DOI: 10.1093/oso/9780198537816.001.0001

Show Summary Details
Page of

PRINTED FROM OXFORD SCHOLARSHIP ONLINE (oxford.universitypressscholarship.com). (c) Copyright Oxford University Press, 2021. All Rights Reserved. An individual user may print out a PDF of a single chapter of a monograph in OSO for personal use. date: 14 June 2021

Martin-Löf’s type theory

Martin-Löf’s type theory

Chapter:
(p.19) Martin-Löf’s type theory
Source:
Handbook of Logic in Computer Science: Volume 5. Algebraic and Logical Structures
Author(s):

B. Nördstrom

K. Petersson

Publisher:
Oxford University Press
DOI:10.1093/oso/9780198537816.003.0001

The type theory described in this chapter has been developed by Martin-Löf with the original aim of being a clarification of constructive mathematics. Unlike most other formalizations of mathematics, type theory is not based on predicate logic. Instead, the logical constants are interpreted within type theory through the Curry-Howard correspondence between propositions and sets [Curry and Feys, 1958; Howard, 1980]: a proposition is interpreted as a set whose elements represent the proofs of the proposition. It is also possible to view a set as a problem description in a way similar to Kolmogorov’s explanation of the intuitionistic propositional calculus [Kolmogorov, 1932]. In particular, a set can be seen as a specification of a programming problem; the elements of the set are then the programs that satisfy the specification. An advantage of using type theory for program construction is that it is possible to express both specifications and programs within the same formalism. Furthermore, the proof rules can be used to derive a correct program from a specification as well as to verify that a given program has a certain property. As a programming language, type theory is similar to typed functional languages such as ML [Gordon et al., 1979; Milner et al., 1990] and Haskell [Hudak et al, 1992], but a major difference is that the evaluation of a well-typed program always terminates. The notion of constructive proof is closely related to the notion of computer program. To prove a proposition (∀xA)(∃yB)P(x, y) constructively means to give a function f which when applied to an element a in A gives an element b in B such that P(a, b) holds. So if the proposition (∀xA)(∃yB)P(x, y) expresses a specification, then the function f obtained from the proof is a program satisfying the specification. A constructive proof could therefore itself be seen as a computer program and the process of computing the value of a program corresponds to the process of normalizing a proof. It is by this computational content of a constructive proof that type theory can be used as a programming language; and since the program is obtained from a proof of its specification, type theory can be used as a programming logic.

Keywords:   Curry-Howard interpretation, abstraction condition, algebraic domain, concrete representation, order-sorted signature, predicate logic, term-model, uniform convergence

Oxford Scholarship Online requires a subscription or purchase to access the full text of books within the service. Public users can however freely search the site and view the abstracts and keywords for each book and chapter.

Please, subscribe or login to access full text content.

If you think you should have access to this title, please contact your librarian.

To troubleshoot, please check our FAQs , and if you can't find the answer there, please contact us .