Strong Normalisation of Cut-Elimination That Simulates β-Reduction

DOI10.1007/978-3-540-78499-9_27MaRDI QIDQ5458374zbMATH OpenOpenAlexFDO

Authors Kentaro Kikuchi, Stéphane Lengrand

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

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

Recommendations

• Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions
• Strong normalisation of cut-elimination in classical logic
• Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation
• scientific article; zbMATH DE number 1722668
• scientific article; zbMATH DE number 1342291

Cites work

• A new deconstructive logic: linear logic
• An Isomorphism Between Cut-Elimination Procedure and Proof Reduction
• Call-by-value, call-by-name, and strong normalization for the classical sequent calculus
• Confluence of Cut-Elimination Procedures for the Intuitionistic Sequent Calculus
• Explicit substitution. On the edge of strong normalization
• scientific article; zbMATH DE number 1670856 (Why is no real title available?)
• scientific article; zbMATH DE number 2185727 (Why is no real title available?)
• scientific article; zbMATH DE number 3730111 (Why is no real title available?)
• scientific article; zbMATH DE number 3735770 (Why is no real title available?)
• scientific article; zbMATH DE number 1342291 (Why is no real title available?)
• scientific article; zbMATH DE number 1070568 (Why is no real title available?)
• scientific article; zbMATH DE number 2079018 (Why is no real title available?)
• scientific article; zbMATH DE number 1497485 (Why is no real title available?)
• scientific article; zbMATH DE number 786494 (Why is no real title available?)
• Lectures on the Curry-Howard isomorphism
• Normalization as a homomorphic image of cut-elimination
• On a Local-Step Cut-Elimination Procedure for the Intuitionistic Sequent Calculus
• Permutability of proofs in intuitionistic sequent calculi
• Perpetual reductions in -calculus
• Resource operators for \(\lambda\)-calculus
• Strong Normalisation of Cut-Elimination That Simulates β-Reduction
• Strong normalization from weak normalization in typed \(\lambda\)-calculi
• Strong Normalization of Herbelin's Explicit Substitution Calculus with Substitution Propagation
• Termination of term rewriting using dependency pairs
• The correspondence between cut-elimination and normalization
• The duality of computation
• λν, a calculus of explicit substitutions which preserves strong normalisation

Cited in

(6)

• Strong normalisation of cut-elimination in classical logic
• scientific article; zbMATH DE number 1722668 (Why is no real title available?)
• Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions
• scientific article; zbMATH DE number 1499092 (Why is no real title available?)
• scientific article; zbMATH DE number 7599997 (Why is no real title available?)
• Strong Normalisation of Cut-Elimination That Simulates β-Reduction

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

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