Propositional functions and families of types.
Open Access
- 1 June 1989
- journal article
- Published by Duke University Press in Notre Dame Journal of Formal Logic
- Vol. 30 (3) , 442-458
- https://doi.org/10.1305/ndjfl/1093635159
Abstract
IntroductionIn order to capture some of the programmers errors, several computer languages, likePascal and ML, are equipped with a type system. Using the Curry-Howard interpretationof propositions as types [3, 8], or as we shall say here, propositions as sets, a type systemcan be made strong enough to be used to specify the task a program is supposed to do.This is one of the basis for Martin-Lof's suggestion in [11] to use his formulation of typetheory for programming; his ideas are...Keywords
This publication has 0 references indexed in Scilit: