6 citations · 17 across the 22 of their papers we have counts for
24 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…
A complete realisability semantics for intersection types and arbitrary expansion variables
Fairouz Kamareddine, Karim Nour, Vincent Rahli +1
Expansion was introduced at the end of the 1970s for calculating principal typings for -terms in intersection type systems. Expansion variables (E-variables) were introduced at…
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…