Focalisation and Classical Realisability

DOI10.1007/978-3-642-04027-6_30zbMath1257.03055OpenAlexW1738264400MaRDI QIDQ3644763

Guillaume Munch-MacCagnoni

Publication date: 12 November 2009

Published in: Computer Science Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-04027-6_30

Mathematics Subject Classification ID

Theory of programming languages (68N15) Logic in computer science (03B70) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40)

Related Items

From Focalization of Logic to the Logic of Focalization, Linear $$ \lambda \mu $$ is $$ \textsc {CP} $$ (more or less), No value restriction is needed for algebraic effects and handlers, Focused linear logic and the \(\lambda\)-calculus, Preface to the special volume, A Classical Realizability Model for a Semantical Value Restriction, Abstracting models of strong normalization for classical calculi, On the Meaning of Focalization, Unnamed Item, Quantitative classical realizability

Cites Work

• Unnamed Item
• Unnamed Item
• Computational ludics
• Linear logic
• Classical \(F_{\omega}\), orthogonality and symmetric candidates
• Locus Solum: From the rules of logic to the logic of rules
• The duality of computation
• The Duality of Computation under Focus
• A new constructive logic: classic logic
• Logic Programming with Focusing Proofs in Linear Logic
• A new deconstructive logic: linear logic
• Call-by-value is dual to call-by-name
• Disjunctive normal forms and local exceptions
• Logical Approaches to Computational Barriers