Refinement to imperative HOL (Q1739909): Difference between revisions

@@ Property / describes a project that uses @@
+Refinement Monadic
@@ Property / describes a project that uses: Refinement Monadic / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle
@@ Property / describes a project that uses: Isabelle / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Imperative Refinement
@@ Property / describes a project that uses: Imperative Refinement / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Ynot
@@ Property / describes a project that uses: Ynot / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Autoref
@@ Property / describes a project that uses: Autoref / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Collections
@@ Property / describes a project that uses: Collections / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CAVA LTL Modelchecker
@@ Property / describes a project that uses: CAVA LTL Modelchecker / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W2762980364
@@ Property / OpenAlex ID: W2762980364 / rank @@
+Normal rank
@@ Property / cites work @@
+A theory of timed automata
@@ Property / cites work: A theory of timed automata / rank @@
+Normal rank
@@ Property / cites work @@
+Refinement Calculus
@@ Property / cites work: Refinement Calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Permission accounting in separation logic
@@ Property / cites work: Permission accounting in separation logic / rank @@
+Normal rank
@@ Property / cites work @@
+Imperative Functional Programming with Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Characteristic formulae for the verification of imperative programs
+Normal rank
@@ Property / cites work @@
+Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation
+Normal rank
@@ Property / cites work @@
+Fiat
@@ Property / cites work: Fiat / rank @@
+Normal rank
@@ Property / cites work @@
+Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems
+Normal rank
@@ Property / cites work @@
+Q4356435
@@ Property / cites work: Q4356435 / rank @@
+Normal rank
@@ Property / cites work @@
+Mechanised Separation Algebra
@@ Property / cites work: Mechanised Separation Algebra / rank @@
+Normal rank
@@ Property / cites work @@
+Partial and nested recursive function definitions in higher-order logic
+Normal rank
@@ Property / cites work @@
+Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
+Normal rank
@@ Property / cites work @@
+Automatic Data Refinement
@@ Property / cites work: Automatic Data Refinement / rank @@
+Normal rank
@@ Property / cites work @@
+Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm
+Normal rank
@@ Property / cites work @@
+Formalizing the Edmonds-Karp Algorithm
@@ Property / cites work: Formalizing the Edmonds-Karp Algorithm / rank @@
+Normal rank
@@ Property / cites work @@
+Ynot
@@ Property / cites work: Ynot / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+Program development by stepwise refinement
@@ Property / cites work: Program development by stepwise refinement / rank @@
+Normal rank