Focalisation and Classical Realisability

DOI10.1007/978-3-642-04027-6_30zbMath1257.03055MaRDI 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

68N15: Theory of programming languages

03B70: Logic in computer science

03F52: Proof-theoretic aspects of linear logic and other substructural logics

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

03B40: Combinatory logic and lambda calculus

Related Items

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

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