### 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 language | English (US) |
---|---|

Title of host publication | Proceedings of the 1982 ACM Symposium on LISP and Functional Programming, LFP 1982 |

Publisher | Association for Computing Machinery, Inc |

Pages | 243-252 |

Number of pages | 10 |

ISBN (Print) | 0897910826, 9780897910828 |

DOIs | |

State | Published - Aug 15 1982 |

Externally published | Yes |

Event | 1982 ACM Symposium on LISP and Functional Programming, LFP 1982 - Pittsburgh, United States Duration: Aug 15 1982 → Aug 18 1982 |

### Other

Other | 1982 ACM Symposium on LISP and Functional Programming, LFP 1982 |
---|---|

Country | United States |

City | Pittsburgh |

Period | 8/15/82 → 8/18/82 |

### Fingerprint

### ASJC Scopus subject areas

- Computational Theory and Mathematics
- Modeling and Simulation
- Software
- Computational Mathematics

### Cite this

*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.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*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

}

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 -