Propositions and specifications of programs in Martin-Löf's type theory (Q800719): Difference between revisions
From MaRDI portal
Added link to MaRDI item. |
Changed an Item |
||
| Property / describes a project that uses | |||
| Property / describes a project that uses: Automath / rank | |||
Normal rank | |||
Revision as of 07:28, 28 February 2024
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Propositions and specifications of programs in Martin-Löf's type theory |
scientific article |
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
