6 citations · 17 across the 22 of their papers we have counts for
24 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…
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…