Focalisation and Classical Realisability

DOI10.1007/978-3-642-04027-6_30MaRDI QIDQ3644763zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• The duality of computation under focus
• The polarized \(\lambda\)-calculus
• Polarized and focalized linear and classical proofs
• Structural focalization
• Focused linear logic and the \(\lambda\)-calculus

Cites work

• A new constructive logic: classic logic
• A new deconstructive logic: linear logic
• Call-by-value is dual to call-by-name
• Classical \(F_{\omega}\), orthogonality and symmetric candidates
• Computational ludics
• Disjunctive normal forms and local exceptions
• scientific article; zbMATH DE number 482822 (Why is no real title available?)
• Linear logic
• Locus solum: From the rules of logic to the logic of rules.
• Logic Programming with Focusing Proofs in Linear Logic
• Logical Approaches to Computational Barriers
• The blind spot. Course on logic. II. On the imperfection
• The duality of computation
• The duality of computation under focus

Cited in

(14)

• Classical realizability in the CPS target language
• 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
• The duality of computation under focus
• From focalization of logic to the logic of focalization
• Linear is CP (more or less)
• Compiling with classical connectives
• Preface to the special volume
• No value restriction is needed for algebraic effects and handlers
• Focused linear logic and the \(\lambda\)-calculus
• Meaningfulness and genericity in a subsuming framework (invited talk)
• A contextual formalization of structural coinduction

This page was built for publication: Focalisation and Classical Realisability

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