What is wrong?

# Programming in Martin-Löf's Type Theory

## Various

| Sending vote
| Voted!
|

### Book Details:

pos
Global
pos
Category
 Year: 2004 Publisher: University of Göteborg Pages: 211 pages Language: english Since: 21/07/2014 Size: 602 KB License: Pending review

### Content:

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.

## Scanning lists...

21/07/2014

Nothing yet...

Nothing yet...

Nothing yet...

### Views

This may take several minutes

### Interest

#### Countries segmentation

This may take several minutes

### evolution

This may take several minutes