Unification in matching logic

DOI10.1007/978-3-030-30942-8_30MaRDI QIDQ6535966zbMATH OpenFDO

Authors Andrei Arusoaie, Dorel Lucanu

Publication date 14 March 2024

Full work available at URL https://doi.org/10.1007/978-3-030-30942-8_30

zbMATH Keywords

certificationmatching logicsemantic unificationsyntactic term unification

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of programming languages (68N15) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42)

Recommendations

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

Cites work

• An Efficient Unification Algorithm
• Coming to terms with quantified reasoning
• From hoare logic to matching logic reachability
• scientific article; zbMATH DE number 3045411 (Why is no real title available?)
• K-Java: a complete semantics of Java
• Matching logic
• One-path reachability logic
• Program verification by coinduction
• Proving reachability-logic formulas incrementally
• Symbolic execution based on language transformation
• Unification theory
• Verifying Reachability-Logic Properties on Rewriting-Logic Specifications

Cited in

(1)

• Unification and anti-unification in applicative matching logic

This page was built for publication: Unification in matching logic

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