Principal type scheme and unification for intersection type discipline

DOI10.1016/0304-3975(88)90101-6zbMath0656.68022MaRDI 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

unification; principal type scheme; \(\lambda \) -calculus; intersection type discipline

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

03B40: Combinatory logic and lambda calculus

Related Items

Cut-elimination in the strict intersection type assignment system is strongly normalizing, 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, Complete restrictions of the intersection type discipline, Principal types of BCK-lambda-terms, Type inference, abstract interpretation and strictness analysis, Principality and type inference for intersection types using expansion variables, Characterising Strongly Normalising Intuitionistic Sequent Terms, On Isomorphisms of Intersection 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