¿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

Programming in Martin-Löf's Type Theory

Programming in Martin-Löf's Type Theory

Puntuación: ---- | 0 votos
| Enviando voto
| ¡Votado!
|

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.

Categorías:

Etiquetas:

Cargando comentarios...

Escaneando listas...

El libro en números

Posición global

posición en categoría

en catálogo desde

21/07/2014

puntuación

Nothing yet...

votos

Nothing yet...

'LIKES' sociales

Nothing yet...

Visitas

Descargas

Esto puede tardar un momento

Interés

Segmentación por países

Esto puede tardar un momento

Páginas de entrada

Segmentación por sitios web

evolución

Esto puede tardar un momento

Cargando...