Mechanised DPO theory: uniqueness of derivations and Church-Rosser theorem
From MaRDI portal
Publication:6535510
Recommendations
Cites work
- scientific article; zbMATH DE number 3548465 (Why is no real title available?)
- scientific article; zbMATH DE number 7649899 (Why is no real title available?)
- A formal proof of the Kepler conjecture
- A formally verified proof of the prime number theorem
- A graph library for Isabelle
- Concrete semantics. With Isabelle/HOL
- Deriving graphs from graphs by applying a production
- Double-pushout graph transformation revisited
- Elements of finite model theory.
- Foundations of Software Science and Computation Structures
- From LCF to Isabelle/HOL
- Fundamentals of algebraic graph transformation
- Interactive and automated proofs for graph transformations
- Logic in Computer Science
- Pushout-Properties: An analysis of gluing constructions for graphs
- Reasoning about graph programs
- The Four Colour Theorem: Engineering of a Formal Proof
- Theorem proving graph grammars with attributes and negative application conditions
- Towards mechanised proofs in double-pushout graph transformation
- Tutorial to locales and locale interpretation
- Verifying graph programs with monadic second-order logic
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)
