Principal type scheme and unification for intersection type discipline
type: Item
instance of: scholarly article
title: Principal type scheme and unification for intersection type discipline
zbMATH Open document ID: 0656.68022
DOI: 10.1016/0304-3975(88)90101-6
published in: Theoretical Computer Science
publication date: 1988-01-01T00:00:00Z
review text: The intersection type discipline for the \(\lambda\)-calculus (ITD) is an extension of the classical functionality theory of Curry. In the ITD a term satisfying a given property has a principal type scheme in an extended meaning, i.e., there is a type scheme deducible for it from which all and only the type schemes deducible for it are reachable, by means of suitable operations. The problem of finding the principal type scheme for a term, if it exists, is semidecidable. In the paper a procedure is shown, building the principal type scheme of a term through the construction of the most general unifier for intersection type schemes.
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03B40
zbMATH DE Number: 4072355
zbMATH Keywords: unification
zbMATH Keywords: intersection type discipline
zbMATH Keywords: \(\lambda \) -calculus
zbMATH Keywords: principal type scheme
author: Simona Ronchi Della Rocca
describes a project that uses: ML
MaRDI profile type: Publication
full work available at URL: 0304-3975(88)90101-6
OpenAlex ID: W2123812977
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: A filter lambda model and the completeness of type assignment
cites work: An extension of basic functionality theory for \(\lambda\)-calculus
cites work: Q5565113
cites work: The Principal Type-Scheme of an Object in Combinatory Logic
cites work: The completeness theorem for typing lambda-terms
cites work: A theory of type polymorphism in programming
cites work: A Machine-Oriented Logic Based on the Resolution Principle
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 4072355