Least and Greatest Fixed Points in Linear Logic

DOI10.1145/2071368.2071370zbMath1352.03072arXiv0910.3383OpenAlexW2088881461WikidataQ130863236 ScholiaQ130863236MaRDI 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 (32)

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

This page was built for publication: Least and Greatest Fixed Points in Linear Logic