Types with intersection: An introduction
type: Item
instance of: scholarly article
title: Types with intersection: An introduction
zbMATH Open document ID: 0774.03002
DOI: 10.1007/BF01211394
author: J. Roger Hindley
published in: Formal Aspects of Computing
publication date: 1993-01-17T00:00:00Z
review text: This is a very lucid introduction to type theory with intersection. The author first clarifies and stresses the distinction between typed systems and type assignment systems, that is, the difference of interpretations of a function from a certain type to another (Church interpretation and Curry interpretation). The Coppo-Dezani type-assignment system \(TA_ \lambda(\land,\omega)\), the simplest of such systems with intersection, is introduced, and its most basic properties, such as \(\beta\)-invariance and characterization of solvable terms, are presented. Many illuminative examples are provided. A comprehensive bibliography up to the end of 1991 is included. Strongly recommended to the newcomer to this field.
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03-01
zbMATH DE Number: 97538
zbMATH Keywords: combination
zbMATH Keywords: lambda-calculus
zbMATH Keywords: type theory with intersection
reviewed by: Teruo Hikita
describes a project that uses: Forsythe
MaRDI profile type: Publication
cites work: Q4035227
cites work: Complete restrictions of the intersection type discipline
cites work: A filter lambda model and the completeness of type assignment
cites work: A formulation of the simple theory of types
cites work: Q3893285
cites work: A new type assignment for λ-terms
cites work: An extension of basic functionality theory for \(\lambda\)-calculus
cites work: Q3221961
cites work: Functional Characters of Solvable Terms
cites work: Type theories, normal forms, and \(D_{\infty}\)-lambda-models
cites work: Modified basic functionality in combinatory logic
cites work: Intersection types for combinatory logic
cites work: Q3345747
cites work: A characterization of F-complete type assignments
cites work: Q4722037
cites work: Q4723730
cites work: Q4724624
cites work: Principal Typing in a ∀Λ-Discipline
cites work: The completeness of provable realizability
cites work: Characterization theorems for a filter lambda model
cites work: Principal type schemes for an extended type theory
description: scientific article; zbMATH DE number 97538