A semantic model of types for applicative languages

D. B. MacQueen, Ravi Sethi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

37 Scopus citations


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.

Original languageEnglish (US)
Title of host publicationProceedings of the 1982 ACM Symposium on LISP and Functional Programming, LFP 1982
PublisherAssociation for Computing Machinery, Inc
Number of pages10
ISBN (Print)0897910826, 9780897910828
StatePublished - Aug 15 1982
Externally publishedYes
Event1982 ACM Symposium on LISP and Functional Programming, LFP 1982 - Pittsburgh, United States
Duration: Aug 15 1982Aug 18 1982


Other1982 ACM Symposium on LISP and Functional Programming, LFP 1982
Country/TerritoryUnited States

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Modeling and Simulation
  • Software
  • Computational Mathematics


Dive into the research topics of 'A semantic model of types for applicative languages'. Together they form a unique fingerprint.

Cite this