10 citations · 19 across the 11 of their papers we have counts for
11 papers · 1 filter
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 direct proof of the confluence of combinatory strong reduction
René David
I give a proof of the confluence of combinatory strong reduction that does not use the one of lambda-calculus. I also give simple and direct proofs of a standardization theorem for…
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…