Matching logic explained

DOI10.1016/J.JLAMP.2021.100638MaRDI QIDQ2035650zbMATH OpenOpenAlexFDO

Authors Yanyan Li

Publication date 25 June 2021

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/2142/107794

zbMATH Keywords

(co)inductive data types(co)monad specificationdependent typesmatching logicprogram logicsspecification of transition systems

Mathematics Subject Classification ID

Computer science (68-XX)

Recommendations

• Matching logic -- extended abstract (invited talk)
• Matching logic
• Matching logic: an alternative to Hoare/Floyd logic
• Connecting Constrained Constructor Patterns and Matching Logic
• From hoare logic to matching logic reachability

Cites work

• A calculus of communicating systems
• A lattice-theoretical fixpoint theorem and its applications
• Circular coinduction: a proof theoretical foundation
• Comonadic notions of computation
• Handbook of modal logic
• scientific article; zbMATH DE number 4039251 (Why is no real title available?)
• scientific article; zbMATH DE number 1296290 (Why is no real title available?)
• scientific article; zbMATH DE number 1412988 (Why is no real title available?)
• Matching logic
• Nominal logic, a first order theory of names and binding
• Process Algebra

Cited in

(15)

• Capturing constrained constructor patterns in matching logic
• Matching logic: an alternative to Hoare/Floyd logic
• Matching logic
• Matching logic -- extended abstract (invited talk)
• A matching logic foundation for Alk
• Towards a unifying logical framework for neural networks
• Connecting Constrained Constructor Patterns and Matching Logic
• Unification in matching logic
• Interactive matching logic proofs in Coq
• Cartesian reachability logic: a language-parametric logic for verifying k-safety properties
• A unifying logical foundation for initial algebra semantics and induction
• Unification and anti-unification in applicative matching logic
• \( \mathbb{K}\) definitions as matching logic theories, formally
• Toward model-theoretic consistency verification in a dependently typed encoding of matching logic
• A matching logic theory of multi-hole contexts

Describes a project that uses

Uses Software

• CIRC

This page was built for publication: Matching logic explained

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2035650)