Strong Normalisation of Cut-Elimination That Simulates β-Reduction

DOI10.1007/978-3-540-78499-9_27zbMATH Open1139.03043OpenAlexW1578162183MaRDI QIDQ5458374FDOQ5458374

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

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

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (5)

• Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions
• Title not available (Why is that?)
• Title not available (Why is that?)
• Strong Normalisation of Cut-Elimination That Simulates β-Reduction
• Strong normalisation of cut-elimination in classical logic

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)