Strong Normalisation of Cut-Elimination That Simulates β-Reduction

DOI10.1007/978-3-540-78499-9_27zbMath1139.03043OpenAlexW1578162183MaRDI QIDQ5458374

Stéphane Lengrand, Kentaro Kikuchi

Publication date: 11 April 2008

Published in: Foundations of Software Science and Computational Structures (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-78499-9_27

Mathematics Subject Classification ID

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

Related Items (1)

Strong Normalisation of Cut-Elimination That Simulates β-Reduction

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Resource operators for \(\lambda\)-calculus
• Lectures on the Curry-Howard isomorphism
• Explicit substitution. On the edge of strong normalization
• Permutability of proofs in intuitionistic sequent calculi
• Perpetual reductions in \(\lambda\)-calculus
• Strong normalization from weak normalization in typed \(\lambda\)-calculi
• Termination of term rewriting using dependency pairs
• The duality of computation
• λν, a calculus of explicit substitutions which preserves strong normalisation
• An Isomorphism Between Cut-Elimination Procedure and Proof Reduction
• The correspondence between cut-elimination and normalization
• Normalization as a homomorphic image of cut-elimination
• A new deconstructive logic: linear logic
• Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation
• On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus
• Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus
• Strong Normalisation of Cut-Elimination That Simulates β-Reduction

This page was built for publication: Strong Normalisation of Cut-Elimination That Simulates β-Reduction