Combining type disciplines
type: Item
instance of: scholarly article
title: Combining type disciplines
zbMATH Open document ID: 0813.03009
DOI: 10.1016/0168-0072(94)90034-5
author: Felice Cardone
author: Mariangiola Dezani-Ciancaglini
author: Ugo de'Liguoro
published in: Annals of Pure and Applied Logic
publication date: 1995-06-07T00:00:00Z
review text: This paper presents a type inference system for pure \(\lambda\)-calculus combining the main constructors: arrow, union, intersection, quantifiers and recursion. After a description in a natural-deduction style, this system is reformulated in a sequent-calculus style. Having shown the equivalence of these two descriptions, the authors use the sequent calculus to investigate preservation of types under reduction. This preservation fails for \(\beta\)-reduction, but is true for a notion of parallel reduction generalizing Gross-Knuth reduction based on complete developments. This is shown using a modification of Gentzen's proof of the Hauptsatz. A model for this system is provided using a \(D_ \infty\) model for \(\lambda\)-calculus, in which types are interpreted as special subsets. This is applied to check soundness of the system. Both syntactical and semantical studies are compared to be closely related work by MacQueen, Plotkin and Sethi, and the authors emphasize the simplifications brought about by the present framework.
reviewed by: N. Bernard
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 03F05
zbMATH DE Number: 550134
zbMATH Keywords: proof theory
zbMATH Keywords: semantics
zbMATH Keywords: type inference system
zbMATH Keywords: \(\lambda\)-calculus
zbMATH Keywords: sequent calculus
zbMATH Keywords: preservation of types under reduction
zbMATH Keywords: parallel reduction
describes a project that uses: Forsythe
MaRDI profile type: Publication
full work available at URL: 0168-0072(94)90034-5
OpenAlex ID: W1979614647
cites work: Recursion over realizability structures
cites work: Intersection and union types: Syntax and semantics
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: Q5531462
cites work: Automatic synthesis of typed \(\Lambda\)-programs on term algebras
cites work: Recursive types for Fun
cites work: Type inference with recursive types: Syntax and semantics
cites work: Q3709890
cites work: An extension of basic functionality theory for \(\lambda\)-calculus
cites work: Type inference, abstract interpretation and strictness analysis
cites work: The calculus of constructions
cites work: Q5565113
cites work: Q5626271
cites work: Q4723730
cites work: An ideal model for recursive polymorphic types
cites work: Q5559220
cites work: Q5649639
cites work: Q5610986
description: scientific article; zbMATH DE number 550134