Propositions and specifications of programs in Martin-Löf's type theory (Q800719)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
scientific article; zbMATH DE number 3878345
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Propositions and specifications of programs in Martin-Löf's type theory |
scientific article; zbMATH DE number 3878345 |
Statements
Propositions and specifications of programs in Martin-Löf's type theory (English)
0 references
1984
0 references
The constructive meaning of mathematical propositions makes it possible to identify specifications for computer programs with propositions. In Martin-Löf's type theory, propositions are interpreted as types using Heyting's explanation of intuitionistic logic. Constructing a program satisfying a specification then corresponds to constructing an element of the corresponding type. One consequence of this approach is that specifications are not in general executable. These ideas are explained and some examples of specifications are given, including a specification for a compiler.
0 references
program specification
0 references
Martin-Löf's type theory
0 references
compiler
0 references
0.8309013843536377
0 references
0.8213550448417664
0 references
0.8011509776115417
0 references
0.7977251410484314
0 references
