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