Principal type schemes for an extended type theory

DOI10.1016/0304-3975(83)90069-5MaRDI QIDQ790801zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• Principal type scheme and unification for intersection type discipline
• Extensional constructs in intensional type theory
• Principal Type Schemes for the Strict Type Assignment System
• Principal types and unification for simple intersection type systems
• Principal type-schemes and condensed detachment
• scientific article; zbMATH DE number 1302061
• Principal Typings for Explicit Substitutions Calculi
• scientific article; zbMATH DE number 2086682
• Principal Typing in a ∀Λ-Discipline
• The converse principal type-scheme theorem in lambda calculus

Cites work

• scientific article; zbMATH DE number 3637819 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3280068 (Why is no real title available?)
• A Machine-Oriented Logic Based on the Resolution Principle
• A filter lambda model and the completeness of type assignment
• Functional Characters of Solvable Terms
• The Principal Type-Scheme of an Object in Combinatory Logic
• The lambda calculus, its syntax and semantics

Cited in

(26)

• Cut-elimination in the strict intersection type assignment system is strongly normalizing
• The heart of intersection type assignment: Normalisation proofs revisited
• Full intersection types and topologies in lambda calculus
• Principal type scheme and unification for intersection type discipline
• Characterization of the principal type of normal forms in an intersection type system
• Complete restrictions of the intersection type discipline
• Ternary relations and relevant semantics
• Filter models for conjunctive-disjunctive \(\lambda\)-calculi
• Intersection type assignment systems
• Normalization, approximation, and semantics for combinator systems
• A type assignment system for game semantics
• Principal Typings for Explicit Substitutions Calculi
• Infinite \(\lambda\)-calculus and types
• Principality and type inference for intersection types using expansion variables
• Strong normalization and typability with intersection types
• Principal type-schemes and condensed detachment
• Principal type inference for GADTs
• scientific article; zbMATH DE number 2086682 (Why is no real title available?)
• Principal Type Schemes for the Strict Type Assignment System
• Implicative algebras: a new foundation for realizability and forcing
• Strongly normalising cut-elimination with strict 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
• Intersection types for combinatory logic
• Types with intersection: An introduction
• Principal Type Schemes for Modular Programs

This page was built for publication: Principal type schemes for an extended type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q790801)