Propositions and specifications of programs in Martin-Löf's type theory (Q800719)

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.