¿Qué está mal?

Aviso: Antes de informar sobre un error con la descarga, por favor, prueba el enlace directo: Programming in Martin-Löf's Type Theory

Cargando...

Debes iniciar sesión para hacer esto.

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

## Varios

Puntuación: ---- | 0 votos
| Enviando voto
|

### Detalles del libro:

pos
Global
pos
Categoría
 Año: 2004 Editor: University of Göteborg Páginas: 211 páginas Idioma: inglés Desde: 21/07/2014 Tamaño: 602 KB Licencia: Pendiente de revisión

### Contenido:

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.

## Escaneando listas...

21/07/2014

Nothing yet...

Nothing yet...

Nothing yet...

### Descargas

Esto puede tardar un momento

### Interés

#### Segmentación por países

Esto puede tardar un momento