Combining type disciplines

DOI10.1016/0168-0072(94)90034-5zbMath0813.03009MaRDI QIDQ1319505

Mariangiola Dezani-Ciancaglini, Ugo de'Liguoro, Felice Cardone

Publication date: 7 June 1995

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0168-0072(94)90034-5

zbMATH Keywords

sequent calculus; proof theory; semantics; \(\lambda\)-calculus; parallel reduction; type inference system; preservation of types under reduction

Mathematics Subject Classification ID

03F05: Cut-elimination and normal-form theorems

03B40: Combinatory logic and lambda calculus

Related Items

Completeness of type assignment systems with intersection, union, and type quantifiers, Higher-order subtyping and its decidability, Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca

Uses Software

• Forsythe

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Type inference with recursive types: Syntax and semantics
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Automatic synthesis of typed \(\Lambda\)-programs on term algebras
• The calculus of constructions
• An extension of basic functionality theory for \(\lambda\)-calculus
• Recursion over realizability structures
• Recursive types for Fun
• Type inference, abstract interpretation and strictness analysis
• Intersection and union types: Syntax and semantics
• An ideal model for recursive polymorphic types