Combining type disciplines

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

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

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 calculusproof theorysemantics\(\lambda\)-calculusparallel reductiontype inference systempreservation of types under reduction

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Related Items (3)

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

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

This page was built for publication: Combining type disciplines