The Experts below are selected from a list of 2274 Experts worldwide ranked by ideXlab platform
Emmanuel Polonovski - One of the best experts on this subject based on the ideXlab platform.
-
Strong Normalization of \overline{\lambda}\mu\widetilde{\mu}-Calculus with Explicit Substitutions
Lecture Notes in Computer Science, 2004Co-Authors: Emmanuel PolonovskiAbstract:The \(\overline{\lambda}\mu\widetilde{\mu}\)-calculus, defined by Curien and Herbelin [7], is a variant of the λμ-calculus that exhibits symmetries such as term/context and call-by-name/call-by-value. Since it is a symmetric, and hence a non-deterministic calculus, usual proof techniques of Normalization needs some adjustments to be made to work in this setting. Here we prove the Strong Normalization (SN) of simply typed \(\overline{\lambda}\mu\widetilde{\mu}\)-calculus with explicit substitutions. For that purpose, we first prove SN of simply typed \(\overline{\lambda}\mu\widetilde{\mu}\)-calculus (by a variant of the reducibility technique from Barbanera and Berardi [2]), then we formalize a proof technique of SN via PSN (preservation of Strong Normalization), and we prove PSN by the perpetuality technique, as formalized by Bonelli [5].
-
Strong Normalization of overline lambda mu widetilde mu calculus with explicit substitutions
Foundations of Software Science and Computation Structure, 2004Co-Authors: Emmanuel PolonovskiAbstract:The \(\overline{\lambda}\mu\widetilde{\mu}\)-calculus, defined by Curien and Herbelin [7], is a variant of the λμ-calculus that exhibits symmetries such as term/context and call-by-name/call-by-value. Since it is a symmetric, and hence a non-deterministic calculus, usual proof techniques of Normalization needs some adjustments to be made to work in this setting. Here we prove the Strong Normalization (SN) of simply typed \(\overline{\lambda}\mu\widetilde{\mu}\)-calculus with explicit substitutions. For that purpose, we first prove SN of simply typed \(\overline{\lambda}\mu\widetilde{\mu}\)-calculus (by a variant of the reducibility technique from Barbanera and Berardi [2]), then we formalize a proof technique of SN via PSN (preservation of Strong Normalization), and we prove PSN by the perpetuality technique, as formalized by Bonelli [5].
-
Strong Normalization of λμμ calculus with explicit substitutions
Lecture Notes in Computer Science, 2004Co-Authors: Emmanuel PolonovskiAbstract:The λμμ-calculus, defined by Curien and Herbelin [7], is a variant of the λμ-calculus that exhibits symmetries such as term/context and call-by-name/call-by-value. Since it is a symmetric, and hence a non-deterministic calculus, usual proof techniques of Normalization needs some adjustments to be made to work in this setting. Here we prove the Strong Normalization (SN) of simply typed λμμ-calculus with explicit substitutions. For that purpose, we first prove SN of simply typed λμμ-calculus (by a variant of the reducibility technique from Barbanera and Berardi [2]), then we formalize a proof technique of SN via PSN (preservation of Strong Normalization), and we prove PSN by the perpetuality technique, as formalized by Bonelli [5].
Yoriyuki Yamagata - One of the best experts on this subject based on the ideXlab platform.
-
Strong Normalization of the second order symmetric λμ calculus
Information & Computation, 2004Co-Authors: Yoriyuki YamagataAbstract:Parigot [Computational Logic and Proof Theory, vol. 713, 1993, p. 263] suggested symmetric structural reduction rules to ensure unique representation of data types. We prove Strong Normalization of the second-order λµ-calculus with such rules.
-
Strong Normalization of a symmetric lambda calculus for second-order classical logic
Archive for Mathematical Logic, 2002Co-Authors: Yoriyuki YamagataAbstract:We extend Barbanera and Berardi's symmetric lambda calculus [2] to second-order classical propositional logic and prove its Strong Normalization.
-
Strong Normalization of second order symmetric lambda mu calculus
International Symposium on Theoretical Aspects of Computer Software, 2001Co-Authors: Yoriyuki YamagataAbstract:Parigot suggested symmetric structural reduction rules for application to µ-abstraction in [9]to ensure unique representation of data type. We prove Strong Normalization of second order ?µ-calculus with these rules.
-
TACS - Strong Normalization of Second Order Symmetric Lambda-mu Calculus
Lecture Notes in Computer Science, 2001Co-Authors: Yoriyuki YamagataAbstract:Parigot suggested symmetric structural reduction rules for application to µ-abstraction in [9]to ensure unique representation of data type. We prove Strong Normalization of second order ?µ-calculus with these rules.
Karim Nour - One of the best experts on this subject based on the ideXlab platform.
-
Strong Normalization results by translation
arXiv: Logic, 2009Co-Authors: René David, Karim NourAbstract:We prove the Strong Normalization of full classical natural deduction (i.e. with conjunction, disjunction and permutative conversions) by using a translation into the simply typed lambda-mu-calculus. We also extend Mendler's result on recursive equations to this system.
-
a short proof of the Strong Normalization of the simply typed lambda mu calculus
arXiv: Logic, 2009Co-Authors: René David, Karim NourAbstract:We give an elementary and purely arithmetical proof of the Strong Normalization of Parigot's simply typed $\lambda\mu$-calculus.
-
Arithmetical proofs of Strong Normalization results for the symmetric $\lambda \mu$-calculus
arXiv: Logic, 2009Co-Authors: René David, Karim NourAbstract:The symmetric $\lambda \mu$-calculus is the $\lambda \mu$-calculus introduced by Parigot in which the reduction rule $\m'$, which is the symmetric of $\mu$, is added. We give arithmetical proofs of some Strong Normalization results for this calculus. We show (this is a new result) that the $\mu\mu'$-reduction is Strongly normalizing for the un-typed calculus. We also show the Strong Normalization of the $\beta\mu\mu'$-reduction for the typed calculus: this was already known but the previous proofs use candidates of reducibility where the interpretation of a type was defined as the fix point of some increasing operator and thus, were highly non arithmetical.
-
a short proof of the Strong Normalization of classical natural deduction with disjunction
arXiv: Logic, 2009Co-Authors: René David, Karim NourAbstract:We give a direct, purely arithmetical and elementary proof of the Strong Normalization of the cut-elimination procedure for full (i.e. in presence of all the usual connectives) classical natural deduction.
-
arithmetical proofs of Strong Normalization results for symmetric λ calculi
Fundamenta Informaticae, 2007Co-Authors: René David, Karim NourAbstract:We give arithmetical proofs of the Strong Normalization of two symmetric λ-calculi corresponding to classical logic. The first one is the λ¯μμe-calculus introduced by Curien & Herbelin. It is derived via the Curry-Howard correspondence from Gentzen's classical sequent calculus LK in order to have a symmetry on one side between "program" and "context" and on other side between "call-by-name" and "callby-value". The second one is the symmetric λμ-calculus. It is the λμ-calculus introduced by Parigot in which the reduction rule μ', which is the symmetric of μ, is added. These results were already known but the previous proofs use candidates of reducibility where the interpretation of a type is defined as the fix point of some increasing operator and thus, are highly non arithmetical.
René David - One of the best experts on this subject based on the ideXlab platform.
-
Strong Normalization results by translation
arXiv: Logic, 2009Co-Authors: René David, Karim NourAbstract:We prove the Strong Normalization of full classical natural deduction (i.e. with conjunction, disjunction and permutative conversions) by using a translation into the simply typed lambda-mu-calculus. We also extend Mendler's result on recursive equations to this system.
-
a short proof of the Strong Normalization of the simply typed lambda mu calculus
arXiv: Logic, 2009Co-Authors: René David, Karim NourAbstract:We give an elementary and purely arithmetical proof of the Strong Normalization of Parigot's simply typed $\lambda\mu$-calculus.
-
Arithmetical proofs of Strong Normalization results for the symmetric $\lambda \mu$-calculus
arXiv: Logic, 2009Co-Authors: René David, Karim NourAbstract:The symmetric $\lambda \mu$-calculus is the $\lambda \mu$-calculus introduced by Parigot in which the reduction rule $\m'$, which is the symmetric of $\mu$, is added. We give arithmetical proofs of some Strong Normalization results for this calculus. We show (this is a new result) that the $\mu\mu'$-reduction is Strongly normalizing for the un-typed calculus. We also show the Strong Normalization of the $\beta\mu\mu'$-reduction for the typed calculus: this was already known but the previous proofs use candidates of reducibility where the interpretation of a type was defined as the fix point of some increasing operator and thus, were highly non arithmetical.
-
a short proof of the Strong Normalization of classical natural deduction with disjunction
arXiv: Logic, 2009Co-Authors: René David, Karim NourAbstract:We give a direct, purely arithmetical and elementary proof of the Strong Normalization of the cut-elimination procedure for full (i.e. in presence of all the usual connectives) classical natural deduction.
-
arithmetical proofs of Strong Normalization results for symmetric λ calculi
Fundamenta Informaticae, 2007Co-Authors: René David, Karim NourAbstract:We give arithmetical proofs of the Strong Normalization of two symmetric λ-calculi corresponding to classical logic. The first one is the λ¯μμe-calculus introduced by Curien & Herbelin. It is derived via the Curry-Howard correspondence from Gentzen's classical sequent calculus LK in order to have a symmetry on one side between "program" and "context" and on other side between "call-by-name" and "callby-value". The second one is the symmetric λμ-calculus. It is the λμ-calculus introduced by Parigot in which the reduction rule μ', which is the symmetric of μ, is added. These results were already known but the previous proofs use candidates of reducibility where the interpretation of a type is defined as the fix point of some increasing operator and thus, are highly non arithmetical.
Michel Parigot - One of the best experts on this subject based on the ideXlab platform.
-
Strong Normalization of second order symmetric lambda calculus
Foundations of Software Technology and Theoretical Computer Science, 2000Co-Authors: Michel ParigotAbstract:Typed symmetric λ-calculus is a simple computational interpretation of classical logic with an involutive negation. Its main distinguishing feature is to be a true non-confluent computational interpretation of classical logic. Its non-confluence reflects the computational freedom of classical logic (as compared to intuitionistic logic). Barbanera and Berardi proved in [1,2] that first order typed symmetric λ-calculus enjoys the Strong Normalization property and showed in [3] that it can be used to derive symmetric programs. In this paper we prove Strong Normalization for second order typed symmetric λ-calculus.
-
FSTTCS - Strong Normalization of Second Order Symmetric lambda-Calculus
FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science, 2000Co-Authors: Michel ParigotAbstract:Typed symmetric λ-calculus is a simple computational interpretation of classical logic with an involutive negation. Its main distinguishing feature is to be a true non-confluent computational interpretation of classical logic. Its non-confluence reflects the computational freedom of classical logic (as compared to intuitionistic logic). Barbanera and Berardi proved in [1,2] that first order typed symmetric λ-calculus enjoys the Strong Normalization property and showed in [3] that it can be used to derive symmetric programs. In this paper we prove Strong Normalization for second order typed symmetric λ-calculus.
