Principal type schemes for an extended type theory

DOI10.1016/0304-3975(83)90069-5zbMath0535.03007OpenAlexW2167904762MaRDI QIDQ790801

N. E. Zubov

Publication date: 1984

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

Full work available at URL: https://doi.org/10.1016/0304-3975(83)90069-5

zbMATH Keywords

natural deductionlambda calculusfunctionalitypolymorphic typesprincipal type scheme

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items (19)

Principality and type inference for intersection types using expansion variables ⋮ Intersection type assignment systems ⋮ Principal type scheme and unification for intersection type discipline ⋮ Ternary relations and relevant semantics ⋮ Strong normalization and typability with intersection types ⋮ Implicative algebras: a new foundation for realizability and forcing ⋮ 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 ⋮ The heart of intersection type assignment: Normalisation proofs revisited ⋮ A type assignment system for game semantics ⋮ Filter models for conjunctive-disjunctive \(\lambda\)-calculi ⋮ Complete restrictions of the intersection type discipline ⋮ Intersection types for combinatory logic ⋮ Types with intersection: An introduction ⋮ Cut-elimination in the strict intersection type assignment system is strongly normalizing ⋮ Full intersection types and topologies in lambda calculus ⋮ Infinite \(\lambda\)-calculus and types ⋮ Strongly Normalising Cut-Elimination with Strict Intersection Types ⋮ Normalization, approximation, and semantics for combinator systems

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The lambda calculus, its syntax and semantics
• A filter lambda model and the completeness of type assignment
• Functional Characters of Solvable Terms
• 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 schemes for an extended type theory