Focusing and polarization in linear, intuitionistic, and classical logics
From MaRDI portal
Publication:1035706
DOI10.1016/j.tcs.2009.07.041zbMath1187.68528OpenAlexW2141978322MaRDI QIDQ1035706
Publication date: 4 November 2009
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2009.07.041
Related Items
From axioms to synthetic inference rules via focusing, A linear logic framework for multimodal logics, Proof checking and logic programming, Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations, The Proof Certifier Checkers, Proof-Search in Natural Deduction Calculus for Classical Propositional Logic, Intuitionistic games: determinacy, completeness, and normalization, On subexponentials, focusing and modalities in concurrent systems, Proofs, Upside Down, Structural Focalization, A Survey of the Proof-Theoretic Foundations of Logic Programming, Towards substructural property-based testing, Unnamed Item, Maximally multi-focused proofs for skew non-commutative \texttt{MILL}, A semantic framework for proof evidence, A focused approach to combining logics, Unnamed Item, Unnamed Item, From QBFs to \textsf{MALL} and back via focussing, Unnamed Item, Goal-oriented proof-search in natural deduction for intuitionistic propositional logic, A coinductive approach to proof search through typed lambda-calculi, Focused proof-search in the logic of bunched implications, Multi-focused cut elimination, Expressing additives using multiplicatives and subexponentials, Imaginary groups: lazy monoids and reversible computation, Proof nets for classical logic, Proof certificates for equality reasoning, Multi-focused proofs with different polarity assignments, The polarized \(\lambda\)-calculus, Kripke semantics for higher-order type theory applied to constraint logic programming languages, Proving concurrent constraint programming correct, revisited, Proof Checking and Logic Programming, Specifying Proof Systems in Linear Logic with Subexponentials, A framework for proof systems, On geometry of interaction for polarized linear logic, Focused and Synthetic Nested Sequents, COCHIS: Stable and coherent implicits, Subformula linking for intuitionistic logic with application to type theory, Proof search and certificates for evidential transactions, A Proposal for Broad Spectrum Proof Certificates, Inhabitation in simply typed lambda-calculus through a lambda-calculus for proof search, A general proof certification framework for modal logic, A proof theory for model checking, A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems, A focused linear logical framework and its application to metatheory of object logics, Connecting Sequent Calculi with Lorenzen-Style Dialogue Games, Resourceful program synthesis from graded linear types
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Polarized and focalized linear and classical proofs
- Linear logic
- Forum: A multiple-conclusion specification logic
- On the unity of logic
- A logical characterization of forward and backward chaining in the inverse method
- Logic programming in a fragment of intuitionistic linear logic
- On structuring proof search for first order linear logic
- Uniform proofs as a foundation for logic programming
- The duality of computation
- Jumbo λ-Calculus
- From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
- Focusing and Polarization in Intuitionistic Logic
- Incorporating Tables into Proofs
- A new constructive logic: classic logic
- Logic Programming with Focusing Proofs in Linear Logic
- Contraction-free sequent calculi for intuitionistic logic
- A new deconstructive logic: linear logic
- FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science
- Logical Approaches to Computational Barriers
