Principal type scheme and unification for intersection type discipline

DOI10.1016/0304-3975(88)90101-6zbMath0656.68022OpenAlexW2123812977MaRDI QIDQ1110311

Simonetta Ronchi della Rocca

Publication date: 1988

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(88)90101-6

zbMATH Keywords

unificationprincipal type scheme\(\lambda \) -calculusintersection type discipline

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Combinatory logic and lambda calculus (03B40)

Related Items (16)

Principality and type inference for intersection types using expansion variables ⋮ Execution time of λ-terms via denotational semantics and intersection types ⋮ Semantic types and approximation for Featherweight Java ⋮ Type inference in polymorphic type discipline ⋮ Characterising Strongly Normalising Intuitionistic Sequent Terms ⋮ Type inference for rank-2 intersection types using set unification ⋮ On Isomorphisms of Intersection Types ⋮ Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca ⋮ On strong normalization and type inference in the intersection type discipline ⋮ Strong normalization through intersection types and memory ⋮ Complete restrictions of the intersection type discipline ⋮ Principal types of BCK-lambda-terms ⋮ Cut-elimination in the strict intersection type assignment system is strongly normalizing ⋮ Unnamed Item ⋮ Type inference, abstract interpretation and strictness analysis ⋮ Isomorphism of intersection and union types

Uses Software

• ML

Cites Work

• Unnamed Item
• Principal type schemes for an extended type theory
• The lambda calculus. Its syntax and semantics. Rev. ed.
• An extension of basic functionality theory for \(\lambda\)-calculus
• A theory of type polymorphism in programming
• The completeness theorem for typing lambda-terms
• A filter lambda model and the completeness of type assignment
• Characterization theorems for a filter lambda model
• A Machine-Oriented Logic Based on the Resolution Principle
• The Principal Type-Scheme of an Object in Combinatory Logic

This page was built for publication: Principal type scheme and unification for intersection type discipline