A semantic model of types for applicative languages

D. B. MacQueen, Ravi Sethi

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

35 Citations (Scopus)

Abstract

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
Pages243-252
Number of pages10
ISBN (Print)0897910826, 9780897910828
DOIs
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

Other

Other1982 ACM Symposium on LISP and Functional Programming, LFP 1982
CountryUnited States
CityPittsburgh
Period8/15/828/18/82

Fingerprint

Semantics
Integer
Lambda Calculus
Proof System
Quantifiers
Soundness
Model
Higher Order
Language
Syntax

ASJC Scopus subject areas

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

Cite this

MacQueen, D. B., & Sethi, R. (1982). A semantic model of types for applicative languages. In Proceedings of the 1982 ACM Symposium on LISP and Functional Programming, LFP 1982 (pp. 243-252). Association for Computing Machinery, Inc. https://doi.org/10.1145/800068.802156

A semantic model of types for applicative languages. / MacQueen, D. B.; Sethi, Ravi.

Proceedings of the 1982 ACM Symposium on LISP and Functional Programming, LFP 1982. Association for Computing Machinery, Inc, 1982. p. 243-252.

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

MacQueen, DB & Sethi, R 1982, A semantic model of types for applicative languages. in Proceedings of the 1982 ACM Symposium on LISP and Functional Programming, LFP 1982. Association for Computing Machinery, Inc, pp. 243-252, 1982 ACM Symposium on LISP and Functional Programming, LFP 1982, Pittsburgh, United States, 8/15/82. https://doi.org/10.1145/800068.802156
MacQueen DB, Sethi R. A semantic model of types for applicative languages. In Proceedings of the 1982 ACM Symposium on LISP and Functional Programming, LFP 1982. Association for Computing Machinery, Inc. 1982. p. 243-252 https://doi.org/10.1145/800068.802156
MacQueen, D. B. ; Sethi, Ravi. / A semantic model of types for applicative languages. Proceedings of the 1982 ACM Symposium on LISP and Functional Programming, LFP 1982. Association for Computing Machinery, Inc, 1982. pp. 243-252
@inproceedings{5e3cac91e1d34260a90a8ae41ea50940,
title = "A semantic model of types for applicative languages",
abstract = "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.",
author = "MacQueen, {D. B.} and Ravi Sethi",
year = "1982",
month = "8",
day = "15",
doi = "10.1145/800068.802156",
language = "English (US)",
isbn = "0897910826",
pages = "243--252",
booktitle = "Proceedings of the 1982 ACM Symposium on LISP and Functional Programming, LFP 1982",
publisher = "Association for Computing Machinery, Inc",

}

TY - GEN

T1 - A semantic model of types for applicative languages

AU - MacQueen, D. B.

AU - Sethi, Ravi

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

SN - 0897910826

SN - 9780897910828

SP - 243

EP - 252

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

PB - Association for Computing Machinery, Inc

ER -