Programming in Martin-Löf’s Type Theory: An Introduction

Clarendon Press (1990)
  Copy   BIBTEX

Abstract

In recent years, several formalisms for program construction have appeared. One such formalism is the type theory developed by Per Martin-L f. Well suited as a theory for program construction, it makes possible the expression of 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. This book contains a thorough introduction to type theory, with information on polymorphic sets, subsets, monomorphic sets, and a full set of helpful examples.

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 103,449

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

The strength of some Martin-Löf type theories.Edward Griffor & Michael Rathjen - 1994 - Archive for Mathematical Logic 33 (5):347-385.
The inconsistency of higher order extensions of Martin-löf's type theory.Bart Jacobs - 1989 - Journal of Philosophical Logic 18 (4):399 - 422.
Well-ordering proofs for Martin-Löf type theory.Anton Setzer - 1998 - Annals of Pure and Applied Logic 92 (2):113-159.
Extending Martin-Löf Type Theory by one Mahlo-universe.Anton Setzer - 2000 - Archive for Mathematical Logic 39 (3):155-181.

Analytics

Added to PP
2020-09-03

Downloads
18 (#1,157,809)

6 months
4 (#864,415)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Citations of this work

Harmony and autonomy in classical logic.Stephen Read - 2000 - Journal of Philosophical Logic 29 (2):123-154.
Studies in logical theory.John Dewey - 1903 - New York: AMS Press.
The entanglement of logic and set theory, constructively.Laura Crosilla - 2022 - Inquiry: An Interdisciplinary Journal of Philosophy 65 (6).
Formal semantics in modern type theories with coercive subtyping.Zhaohui Luo - 2012 - Linguistics and Philosophy 35 (6):491-513.

View all 30 citations / Add more citations

References found in this work

No references found.

Add more references