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

DOI10.1016/S1571-0661(04)80848-XzbMath1264.03121MaRDI QIDQ4924532

No author found.

Publication date: 6 June 2013

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

zbMATH Keywords

cut eliminationpure type systemssequent calculi

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Related Items (1)

Practical Proof Search for Coq by Type Inhabitation

Uses Software

• Automath

Cites Work

• Constructive logics. I: A tutorial on proof systems and typed \(\lambda\)- calculi
• Typing in pure type systems
• Proof-search in type-theoretic languages: An introduction
• Untersuchungen über das logische Schliessen. II
• Intersection and union types: Syntax and semantics
• A Cut-Free Sequent Calculus for Pure Type Systems Verifying the Structural Rules of Gentzen/Kleene
• Expansion postponement for normalising pure type systems
• Lambda terms for natural deduction, sequent calculus and cut elimination
• Completeness of type assignment systems with intersection, union, and type quantifiers
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Cut Elimination in a Class of Sequent Calculi for Pure Type Systems