## 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 |

## ASJC Scopus subject areas

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