Pages that link to "Item:Q5756495"
From MaRDI portal
The following pages link to Abstract Predicates and Mutable ADTs in Hoare Type Theory (Q5756495):
Displaying 5 items.
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits (Q670699) (← links)
- Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq (Q3087993) (← links)
- Safety Guarantees from Explicit Resource Management (Q3602994) (← links)
- Higher-Order Separation Logic in Isabelle/HOLCF (Q5415649) (← links)
- Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language (Q6151555) (← links)
