6 citations · 20 across the 25 of their papers we have counts for
25 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…
Realisability Semantics for Intersection Types and Expansion Variables
Fairouz Kamareddine, Karim Nour, Vincent Rahli +1
Expansion was invented at the end of the 1970s for calculating principal typings for -terms in type systems with intersection types. Expansion variables (E-variables) were inven…
Parametric mixed sequent calculus
Karim Nour, Olivier Laurent
In this paper, we present a propositional sequent calculus containing disjoint copies of classical and intuitionistic logics. We prove a cut-elimination theorem and we establish a…
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.
A semantics of realisability for the classical propositional natural deduction
Karim Nour, Khelifa Saber
In this paper, we introduce a semantics of realisability for the classical propositional natural deduction and we prove a correctness theorem. This allows to characterize the opera…
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…