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

@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-642-22863-6_5
+Normal rank
@@ Property / OpenAlex ID @@
+W1848615987
@@ Property / OpenAlex ID: W1848615987 / rank @@
+Normal rank
@@ 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