3 papers
math.LO2009
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…
math.LO2009
A semantical proof of the strong normalization theorem for full propositional classical natural deduction
Karim Nour, Khelifa Saber
We give in this paper a short semantical proof of the strong normalization for full propositional classical natural deduction. This proof is an adaptation of reducibility candidate…
math.LO2009
A completeness result for the simply typed -calculus
Karim Nour, Khelifa Saber
In this paper, we define a realizability semantics for the simply typed -calculus. We show that if a term is typable, then it inhabits the interpretation of its type. This resu…