Non-wellfounded proof theory for (Kleene+action)(algebras+lattices)
From MaRDI portal
Publication:5079743
DOI10.4230/LIPICS.CSL.2018.19MaRDI QIDQ5079743FDOQ5079743
Authors: Anupam Das, Damien Pous 
Publication date: 28 May 2022
Recommendations
Cites Work
- Netkat, semantic foundations for networks
- A calculational approach to mathematical induction
- Title not available (Why is that?)
- Linear logic
- Residuated lattices. An algebraic glimpse at substructural logics
- Complete systems of \(\mathcal B\)-rational identities
- A completeness theorem for Kleene algebras and the algebra of regular events
- Title not available (Why is that?)
- Concurrent Kleene Algebra
- The Mathematics of Sentence Structure
- Title not available (Why is that?)
- Une condition impliquant toutes les identités rationnelles
- Kleene algebra with tests and Coq tools for while programs
- Title not available (Why is that?)
- On Hoare logic and Kleene algebra with tests
- Least and Greatest Fixpoints in Game Semantics
- Logic Programming with Focusing Proofs in Linear Logic
- Proof Pearl: regular expression equivalence and relation algebra
- Title not available (Why is that?)
- An efficient Coq tactic for deciding Kleene algebras
- Regular expression containment, coinductive axiomatization and computational interpretation
- Automata, Languages and Programming
- From semirings to residuated Kleene lattices
- On Action Logic: Equational Theories of Action Algebras
- An infinitary sequent system for the equational theory of *-continuous action lattices
- A cut-free cyclic proof system for Kleene algebra
- Title not available (Why is that?)
- Infinitary proof theory: the multiplicative additive case
- Title not available (Why is that?)
Cited In (12)
- Uniform interpolation from cyclic proofs: the case of modal mu-calculus
- NON-WELL-FOUNDED PROOFS FOR THE GRZEGORCZYK MODAL LOGIC
- Circular proofs as session-typed processes: a local validity condition
- Contributed papers. Restriction on cut in cyclic proof system for symbolic heaps
- Non-well-founded deduction for induction and coinduction
- Integrating induction and coinduction via closure operators and proof cycles
- Cyclic implicit complexity
- Complexity of a fragment of infinitary action logic with exponential via non-well-founded proofs
- Kleene star, subexponentials without contraction, and infinite computations
- A restricted fragment of the Lambek calculus with iteration and intersection operations
- A linear perspective on cut-elimination for non-wellfounded sequent calculi with least and greatest fixed-points
- Canonicity of proofs in constructive modal logic
Uses Software
This page was built for publication: Non-wellfounded proof theory for (Kleene+action)(algebras+lattices)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5079743)
