A semantics of realisability for the classical propositional natural deduction

MaRDI QIDQ2851691zbMATHFDO

Authors Khelifa Saber, Karim Nour

Publication date 2 October 2013

Full work available at URL https://arxiv.org/abs/0905.1555

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05)

Abstract: 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.

Recommendations

• A semantical proof of the strong normalization theorem for full propositional classical natural deduction
• scientific article; zbMATH DE number 1104448
• A Survey of Classical Realizability
• scientific article; zbMATH DE number 1337625
• On semantics of a term calculus for classical logic

Cited in

(5)

• Strong normalization of classical natural deduction with disjunctions
• scientific article; zbMATH DE number 5851813 (Why is no real title available?)
• A completeness result for the simply typed \(\lambda \mu \)-calculus
• Towards a Canonical Classical Natural Deduction System
• A Classical Realizability Model for a Semantical Value Restriction

This page was built for publication: A semantics of realisability for the classical propositional natural deduction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2851691)