Logic Programming with Focusing Proofs in Linear Logic
From MaRDI portal
Publication:4018167
Recommendations
Cited in
(only showing first 100 items - show all)- A fresh view of linear logic as a logical framework
- From QBFs to \textsf{MALL} and back via focussing
- From axioms to synthetic inference rules via focusing
- Resource-distribution via Boolean constraints (extended abstract)
- Kripke semantics for higher-order type theory applied to constraint logic programming languages
- Focused linear logic and the \(\lambda\)-calculus
- Proving concurrent constraint programming correct, revisited
- An Isbell duality theorem for type refinement systems
- A categorical semantics for polarized MALL
- A rewriting framework and logic for activities subject to regulations
- Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
- On geometry of interaction for polarized linear logic
- A linear logic programming language for concurrent programming over graph structures
- A framework for proof systems
- A linear logic framework for multimodal logics
- Subformula linking for intuitionistic logic with application to type theory
- On the meaning of focalization
- Subexponentials in non-commutative linear logic
- Structural focalization
- Focused proof-search in the logic of bunched implications
- Figures of dialogue: a view from ludics
- Parsing/theorem-proving for logical grammar \textit{CatLog3}
- A proof theory of right-linear ( -)grammars via cyclic proofs
- Cut elimination for the unified logic
- A sequent calculus for a semi-associative law
- A focused linear logical framework and its application to metatheory of object logics
- An interpretation of CCS into ludics
- Formal meta-level analysis framework for quantum programming languages
- scientific article; zbMATH DE number 7533344 (Why is no real title available?)
- Implicational relevance logic is 2-\textsc{ExpTime}-complete
- Proofs as computations in linear logic
- Resource modalities in tensor logic
- On subexponentials, focusing and modalities in concurrent systems
- scientific article; zbMATH DE number 7243672 (Why is no real title available?)
- Jump from parallel to sequential proofs: exponentials
- Syntactic Completeness of Proper Display Calculi
- Entailment-based actions for coordination
- Algebraic proof theory for substructural logics: cut-elimination and completions
- Differential Linear Logic and Polarization
- Axiom Directed Focusing
- Resourceful program synthesis from graded linear types
- Non-commutative proof construction: a constraint-based approach
- Linearizing intuitionistic implication
- An intuitionistic formula hierarchy based on high‐school identities
- Specifying properties of concurrent computations in CLF
- MacNeille completions of FL-algebras
- From cut-free calculi to automated deduction: the case of bounded contraction
- Hybrid and subexponential linear logics
- Multi-focused proofs with different polarity assignments
- The polarized \(\lambda\)-calculus
- Focused and Synthetic Nested Sequents
- A logical characterization of forward and backward chaining in the inverse method
- Algebraic proof theory: hypersequents and hypercompletions
- A proposal for broad spectrum proof certificates
- Focused Inductive Theorem Proving
- Foundations for reliable and flexible interactive multimedia scores
- Expressing additives using multiplicatives and subexponentials
- Representing scope in intuitionistic deductions
- scientific article; zbMATH DE number 2134912 (Why is no real title available?)
- A general proof certification framework for modal logic
- Bracket induction for Lambek calculus with bracket modalities
- Focussing and proof construction
- Proof strategies in linear logic
- Non-commutative logic. III: Focusing proofs.
- Proof checking and logic programming
- Linear logic in a refutational setting
- Cut elimination in multifocused linear logic
- Multimodal linguistic inference
- Correct answers for first order logic
- On the relations between disjunctive and linear logic programming
- A tableau method for the Lambek calculus based on a matrix characterization
- Proof checking and logic programming
- scientific article; zbMATH DE number 7243675 (Why is no real title available?)
- Logic programming with sequent systems: a linear logic approach
- A concurrent constraint programming interpretation of access permissions
- Hybrid linear logic, revisited
- Forum: A multiple-conclusion specification logic
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Weak units, universal cells, and coherence via universality for bicategories
- On concurrent behaviors and focusing in linear logic
- Computer Science Logic
- Focused proof search for linear logic in the calculus of structures
- Reasoning about group polarization: from semantic games to sequent systems
- Automatic verification of secrecy properties for linear logic specifications of cryptographic protocols
- Modularity of proof-nets. Generating the type of a module.
- Formalized meta-theory of sequent calculi for linear logics
- Logic programming in a fragment of intuitionistic linear logic
- Linearity, control effects, and behavioral types
- Soft subexponentials and multiplexing
- From focalization of logic to the logic of focalization
- Softness of MALL proof-structures and a correctness criterion with Mix
- Sequent systems on undirected graphs
- Skolemisation for intuitionistic linear logic
- On Lambek's restriction in the presence of exponential modalities
- Adjoint logic with a 2-category of modes
- Safe session-based concurrency with shared linear state
- Structure of proofs and the complexity of cut elimination
- A proof theoretic view of spatial and temporal dependencies in biochemical systems
- Coherence via focusing for symmetric skew monoidal categories
- The multiplicative-additive Lambek calculus with subexponential and bracket modalities
This page was built for publication: Logic Programming with Focusing Proofs in Linear Logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4018167)
