A semantics of realisability for the classical propositional natural deduction

zbMATH Open1272.03152arXiv0905.1555MaRDI QIDQ2851691FDOQ2851691

Authors: Khelifa Saber, Karim Nour 

Publication date: 2 October 2013

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.

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

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

Mathematics Subject Classification ID

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

Cited In (5)

• Title not available (Why is that?)
• Strong normalization of classical natural deduction with disjunctions
• Towards a Canonical Classical Natural Deduction System
• A Classical Realizability Model for a Semantical Value Restriction
• A completeness result for the simply typed \(\lambda \mu \)-calculus

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)