Least and Greatest Fixed Points in Linear Logic

DOI10.1145/2071368.2071370zbMath1352.03072arXiv0910.3383OpenAlexW2088881461MaRDI QIDQ5892168

David Baelde, Dale A. Miller

Publication date: 17 September 2015

Published in: Logic for Programming, Artificial Intelligence, and Reasoning, ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/0910.3383

zbMATH Keywords

fixed pointscut eliminationlinear logicnormalizationfocusingproof searchrecursive definitions(co)induction

Mathematics Subject Classification ID

Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items

On concurrent behaviors and focusing in linear logic, The undecidability of proof search when equality is a logical connective, Proof checking and logic programming, Complexity of a fragment of infinitary action logic with exponential via non-well-founded proofs, Substructural Proofs as Automata, Transport of finiteness structures and applications, A semantic framework for proof evidence, Cut elimination for a logic with induction and co-induction, Totality in arena games, A focused approach to combining logics, A rewriting framework and logic for activities subject to regulations, Unnamed Item, Focused linear logic and the \(\lambda\)-calculus, Observed Communication Semantics for Classical Processes, The Abella Interactive Theorem Prover (System Description), Multi-focused cut elimination, Kleene star, subexponentials without contraction, and infinite computations, Hybrid and subexponential linear logics, Proving concurrent constraint programming correct, revisited, Unnamed Item, Focused Inductive Theorem Proving, Syntactic cut-elimination for a fragment of the modal mu-calculus, Unnamed Item, Least and Greatest Fixpoints in Game Semantics, On the Expressivity of Minimal Generic Quantification, Corecursion and Non-divergence in Session-Typed Processes, Non-well-founded deduction for induction and coinduction, A Proposal for Broad Spectrum Proof Certificates, Hybrid linear logic, revisited, Mechanized metatheory revisited, A proof theory for model checking, Integrating induction and coinduction via closure operators and proof cycles

Uses Software

• Automath
• Tac
• Bedwyr

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Forum: A multiple-conclusion specification logic
• On the unity of logic
• Logic programming in a fragment of intuitionistic linear logic
• Cut-elimination for a logic with definitions and induction
• Soft linear logic and polynomial time
• Uniform proofs as a foundation for logic programming
• Locus Solum: From the rules of logic to the logic of rules
• From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
• Focusing and Polarization in Intuitionistic Logic
• Contributions to the Theory of Logic Programming
• Logic Programming with Focusing Proofs in Linear Logic
• On the Specification of Sequent Systems
• Types for Proofs and Programs
• CONCUR 2005 – Concurrency Theory