arXiv subjects
Publications and source records attributed to 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 operational behaviour of some typed terms.
In this paper, we introduce the $λμ^{\wedge \vee}$- 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 Andou which uses an extended parallel reduction method and complete development.
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 result serves to give characterizations of the computational behavior of some closed typed terms. We also prove a completeness result of our realizability semantics using a particular term model.
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 candidates introduced by J.-Y. Girard and simplified to the classical case by M. Parigot.