10 citations · 19 across the 10 of their papers we have counts for
10 papers
Strong normalization results by translation
René David, Karim Nour
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…
Counting proofs in propositional logic
René David, Marek Zaionc
We give a procedure for counting the number of different proofs of a formula in various sorts of propositional logic. This number is either an integer (that may be 0 if the formula…
A short proof of the strong normalization of the simply typed -calculus
René David, Karim Nour
We give an elementary and purely arithmetical proof of the strong normalization of Parigot's simply typed -calculus.
Why the usual candidates of reducibility do not work for the symmetric -calculus
René David, Karim Nour
The symmetric -calculus is the -calculus introduced by Parigot in which the reduction rule , which is the symmetric of , is added. We give examples explaining why t…
Arithmetical proofs of strong normalization results for the symmetric -calculus
René David, Karim Nour
The symmetric -calculus is the -calculus introduced by Parigot in which the reduction rule $\m'$, which is the symmetric of , is added. We give arithmetical proofs of so…
An arithmetical proof of the strong normalization for the -calculus with recursive equations on types
René David, Karim Nour
We give an arithmetical proof of the strong normalization of the -calculus (and also of the -calculus) where the type system is the one of simple types with recursive equati…