4 papers
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…
Confluency property of the call-by-value -calculus
Karim Nour, Khelifa Saber
In this paper, we introduce the - call-by-value calculus and we give a proof of the Church-Rosser property of this system. This proof is an adaptation of that of…
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…
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…