10 citations · 19 across the 11 of their papers we have counts for
11 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 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…