Characteristic formulae for liveness properties of non-terminating CakeML programs (Q5875446): Difference between revisions

@@ label / en / label / en @@
+Characteristic formulae for liveness properties of non-terminating CakeML programs
@@ Property / full work available at URL @@
+https://doi.org/10.4230/LIPIcs.ITP.2019.32
+Normal rank
@@ Property / OpenAlex ID @@
+W2977469202
@@ Property / OpenAlex ID: W2977469202 / rank @@
+Normal rank
@@ Property / title @@
+Characteristic formulae for liveness properties of non-terminating CakeML programs (English)
+Normal rank
@@ Property / cites work @@
+A Dynamic Logic with Traces and Coinduction
@@ Property / cites work: A Dynamic Logic with Traces and Coinduction / rank @@
+Normal rank
@@ Property / cites work @@
+Program verification through characteristic formulae
+Normal rank
@@ Property / cites work @@
+Characteristic formulae for the verification of imperative programs
+Normal rank
@@ Property / cites work @@
+Pretty-Big-Step Semantics
@@ Property / cites work: Pretty-Big-Step Semantics / rank @@
+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 @@
+Temporary Read-Only Permissions for Separation Logic
+Normal rank
@@ Property / cites work @@
+Non-standard semantics for program slicing
@@ Property / cites work: Non-standard semantics for program slicing / rank @@
+Normal rank
@@ Property / cites work @@
+A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification
+Normal rank
@@ Property / cites work @@
+Verified Characteristic Formulae for CakeML
@@ Property / cites work: Verified Characteristic Formulae for CakeML / rank @@
+Normal rank
@@ Property / cites work @@
+Q3883467
@@ Property / cites work: Q3883467 / rank @@
+Normal rank
@@ Property / cites work @@
+Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions
+Normal rank
@@ Property / cites work @@
+Q2754051
@@ Property / cites work: Q2754051 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2764132
@@ Property / cites work: Q2764132 / rank @@
+Normal rank
@@ Property / cites work @@
+Transfinite reductions in orthogonal term rewriting systems
+Normal rank
@@ Property / cites work @@
+A formally verified compiler back-end
@@ Property / cites work: A formally verified compiler back-end / rank @@
+Normal rank
@@ Property / cites work @@
+Coinductive big-step operational semantics
@@ Property / cites work: Coinductive big-step operational semantics / rank @@
+Normal rank
@@ Property / cites work @@
+Trace-Based Coinductive Operational Semantics for While
+Normal rank
@@ Property / cites work @@
+A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While
+Normal rank
@@ Property / cites work @@
+Q4963901
@@ Property / cites work: Q4963901 / rank @@
+Normal rank
@@ Property / cites work @@
+Sound, Modular and Compositional Verification of the Input/Output Behavior of Programs
+Normal rank
@@ Property / cites work @@
+Flag-based big-step semantics
@@ Property / cites work: Flag-based big-step semantics / rank @@
+Normal rank
@@ Property / cites work @@
+On the bisimulation proof method
@@ Property / cites work: On the bisimulation proof method / rank @@
+Normal rank
@@ Property / cites work @@
+The verified CakeML compiler backend
@@ Property / cites work: The verified CakeML compiler backend / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:5875446