Programming in Constructive Set Theory
Bengt Nordström · 1981
Per Martin-Löf's Constructive Set Theory is a mathematical language with computation rules. It is primarily designed to be a language for mathematical reasoning. The language has a very simple semantics and its rules have a simple structure. Since it is a language for constructive mathematics, it is possible to execute the proof (the construction of a proposition) as a program.