Completeness of type assignment systems with intersection, union, and type quantifiers

DOI10.1016/S0304-3975(00)00356-XzbMath0984.68027MaRDI QIDQ5958301

Hirofumi Yokouchi

Publication date: 3 March 2002

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

zbMATH Keywords

sequent calculusKripke modelscut-eliminationlambda calculustype systems

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (1)

Cut Elimination in a Class of Sequent Calculi for Pure Type Systems

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Kripke-style models for typed lambda calculus
• Polymorphic type inference and containment
• Constructivism in mathematics. An introduction. Volume I
• Combining type disciplines
• \(F\)-semantics for type assignment systems
• Typing and computational properties of lambda expressions
• The completeness theorem for typing lambda-terms
• Curry's type-rules are complete with respect to the F-semantics too
• Intersection and union types: Syntax and semantics
• Mathematical thought. An introduction to the philosophy of mathematics
• A proof of cut-elimination theorem in simple type-theory
• A filter lambda model and the completeness of type assignment
• An ideal model for recursive polymorphic types
• Functional Characters of Solvable Terms
• Hauptsatz for higher order logic
• Completeness in the theory of types
• Proof theory

This page was built for publication: Completeness of type assignment systems with intersection, union, and type quantifiers