What is wrong?

Notice: Before sending an error with the download, please try the direct link first: Programming in Martin-Löf's Type Theory


You must sign in to do that.

Forgot password?

Programming in Martin-Löf's Type Theory

Programming in Martin-Löf's Type Theory

Programming in Martin-Löf's Type Theory

Score: ---- | 0 votes
| Sending vote
| Voted!

Book Details:

Publisher:University of Göteborg
Pages:211 pages
Size:602 KB
License:Pending review


In recent years several formalisms for program construction have been introduced. One such formalism is the type theory developed by Per Martin-Löf. It is well suited as a theory for program construction since 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. This book contains an introduction to type theory as a theory for program construction.

As a programming language, type theory is similar to typed functional languages such as Hope and ML, but a major difference is that the evaluation of a well-typed program always terminates. In type theory it is also possible to write specifications of programming tasks as well as to develop provably correct programs. Type theory is therefore more than a programming language and it should not be compared with programming languages, but with formalized programming logics such as LCF and PL/CV.

Type theory was originally developed with the aim of being a clarification of constructive mathematics, but unlike most other formalizations of mathematics type theory is not based on first order predicate logic. Instead, predicate logic is interpreted within type theory through the correspondence between propositions and sets. A proposition is interpreted as a set whose elements represent the proofs of the proposition. Hence, a false proposition is interpreted as the empty set and a true proposition as a non-empty set. Chapter 2 contains a detailed explanation of how the logical constants correspond to sets, thus explaining how a proposition could be interpreted as a set. A set cannot only be viewed as a proposition; it is also possible to see a set as a problem description.

This possibility is important for programming, because if a set can be seen as a description of a problem, it can, in particular, be used as a specification of a programming problem. When a set is seen as a problem, the elements of the set are the possible solutions to the problem; or similarly if we see the set as a specification, the elements are the programs that satisfy the specification. Hence, set membership and program correctness are the same problem in type theory, and because all programs terminate, correctness means total correctness.



Loading comments...

Scanning lists...

The book in numbers

global rank

rank in category

online since


rate score

Nothing yet...


Nothing yet...

Social likes

Nothing yet...



This may take several minutes


Countries segmentation

This may take several minutes

Source Referers

Websites segmentation


This may take several minutes