Abstract Predicates and Mutable ADTs in Hoare Type Theory

DOI10.1007/978-3-540-71316-6_14zbMath1187.68158OpenAlexW1677332761MaRDI QIDQ5756495

Amal Ahmed, Aleksandar Nanevski, Greg Morrisett, Lars Birkedal

Publication date: 4 September 2007

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-71316-6_14

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (5)

Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language ⋮ Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits ⋮ Higher-Order Separation Logic in Isabelle/HOLCF ⋮ Safety Guarantees from Explicit Resource Management ⋮ Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq

Uses Software

• JML
• Spec#

This page was built for publication: Abstract Predicates and Mutable ADTs in Hoare Type Theory