Mechanised DPO theory: uniqueness of derivations and Church-Rosser theorem
From MaRDI portal
Publication:6535510
DOI10.1007/978-3-031-36709-0_7zbMATH Open1545.68065MaRDI QIDQ6535510FDOQ6535510
Authors: Detlef Plump 
Publication date: 12 January 2024
Recommendations
Grammars and rewriting systems (68Q42) Formalization of mathematics in connection with theorem provers (68V20)
Cites Work
- Logic in Computer Science
- Elements of finite model theory.
- Concrete semantics. With Isabelle/HOL
- A formally verified proof of the prime number theorem
- Foundations of Software Science and Computation Structures
- Fundamentals of algebraic graph transformation
- The Four Colour Theorem: Engineering of a Formal Proof
- Double-pushout graph transformation revisited
- Deriving graphs from graphs by applying a production
- Pushout-Properties: An analysis of gluing constructions for graphs
- Reasoning about graph programs
- A graph library for Isabelle
- A formal proof of the Kepler conjecture
- Title not available (Why is that?)
- Title not available (Why is that?)
- Tutorial to locales and locale interpretation
- From LCF to Isabelle/HOL
- Verifying graph programs with monadic second-order logic
- Interactive and automated proofs for graph transformations
- Theorem proving graph grammars with attributes and negative application conditions
- Towards mechanised proofs in double-pushout graph transformation
Cited In (2)
This page was built for publication: Mechanised DPO theory: uniqueness of derivations and Church-Rosser theorem
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6535510)
