TY - GEN

T1 - A semantic model of types for applicative languages

AU - MacQueen, D. B.

AU - Sethi, Ravi

N1 - Publisher Copyright:
© 1982 ACM.

PY - 1982/8/15

Y1 - 1982/8/15

N2 - If integer constants are added to the syntax of the pure lambda calculus, then primitive integer values have to be added to the underlying domain V of values. Unlike functions, primitive values should not be applied; we want a run-time error to occur if an attempt is made to apply them as functions. Expressions that might lead to run-time errors are separated out by imposing a "type" structure on expressions. A systematic model of types is developed, in which types are formalized as "ideals" (sets with a certain structure). Polymorphic functions are handled by introducing a quantifier for taking conjunctions of types. Operations for constructing new types from old lead to the consideration of higher-order or meta types, which are called "kinds" to avoid confusion with types. Finally, the semantic model of types is applied to show the soundness of a proof system for inferring the types of expressions.

AB - If integer constants are added to the syntax of the pure lambda calculus, then primitive integer values have to be added to the underlying domain V of values. Unlike functions, primitive values should not be applied; we want a run-time error to occur if an attempt is made to apply them as functions. Expressions that might lead to run-time errors are separated out by imposing a "type" structure on expressions. A systematic model of types is developed, in which types are formalized as "ideals" (sets with a certain structure). Polymorphic functions are handled by introducing a quantifier for taking conjunctions of types. Operations for constructing new types from old lead to the consideration of higher-order or meta types, which are called "kinds" to avoid confusion with types. Finally, the semantic model of types is applied to show the soundness of a proof system for inferring the types of expressions.

UR - http://www.scopus.com/inward/record.url?scp=85035007783&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85035007783&partnerID=8YFLogxK

U2 - 10.1145/800068.802156

DO - 10.1145/800068.802156

M3 - Conference contribution

AN - SCOPUS:85035007783

SN - 0897910826

SN - 9780897910828

T3 - Proceedings of the 1982 ACM Symposium on LISP and Functional Programming, LFP 1982

SP - 243

EP - 252

BT - Proceedings of the 1982 ACM Symposium on LISP and Functional Programming, LFP 1982

PB - Association for Computing Machinery, Inc

T2 - 1982 ACM Symposium on LISP and Functional Programming, LFP 1982

Y2 - 15 August 1982 through 18 August 1982

ER -