Characterising Strongly Normalising Intuitionistic Sequent Terms

DOI10.1007/978-3-540-68103-8_6zbMath1138.03323OpenAlexW1595352090MaRDI QIDQ3499751

José Espírito Santo, Silvia Ghilezan, Jelena Ivetić

Publication date: 3 June 2008

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

Full work available at URL: http://hdl.handle.net/1822/11513

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
• Principal type scheme and unification for intersection type discipline
• Termination of permutative conversions in intuitionistic Gentzen calculi
• Intersection types for explicit substitutions
• A new type assignment for λ-terms
• Completing Herbelin’s Programme
• Lambda terms for natural deduction, sequent calculus and cut elimination
• Delayed Substitutions
• Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi

This page was built for publication: Characterising Strongly Normalising Intuitionistic Sequent Terms