Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq (Q3087993): Difference between revisions

@@ Property / cites work @@
+Q4715213
@@ Property / cites work: Q4715213 / rank @@
+Normal rank
@@ Property / cites work @@
+A very modal model of a modern, major, general type system
+Normal rank
@@ Property / cites work @@
+Programming Languages and Systems
@@ Property / cites work: Programming Languages and Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Step-indexed kripke models over recursive worlds
@@ Property / cites work: Step-indexed kripke models over recursive worlds / rank @@
+Normal rank
@@ Property / cites work @@
+Abstract Predicates and Mutable ADTs in Hoare Type Theory
+Normal rank
@@ Property / cites work @@
+Q4783297
@@ Property / cites work: Q4783297 / rank @@
+Normal rank
@@ Property / cites work @@
+Separation logic and abstraction
@@ Property / cites work: Separation logic and abstraction / rank @@
+Normal rank
@@ Property / cites work @@
+Separation logic, abstraction and inheritance
@@ Property / cites work: Separation logic, abstraction and inheritance / rank @@
+Normal rank
@@ Property / cites work @@
+Frame rule for mutually recursive procedures manipulating pointers
+Normal rank
@@ Property / cites work @@
+Nested Hoare Triples and Frame Rules for Higher-Order Store
+Normal rank
@@ Property / cites work @@
+Higher-Order Separation Logic in Isabelle/HOLCF
@@ Property / cites work: Higher-Order Separation Logic in Isabelle/HOLCF / rank @@
+Normal rank