Abstract Predicates and Mutable ADTs in Hoare Type Theory

DOI10.1007/978-3-540-71316-6_14zbMATH Open1187.68158OpenAlexW1677332761MaRDI QIDQ5756495FDOQ5756495

Authors: Aleksandar Nanevski, Amal Ahmed, 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

Recommendations

• Hoare type theory, polymorphism and separation
• Polymorphism and separation in Hoare type theory
• A Realizability Model for Impredicative Hoare Type Theory
• scientific article; zbMATH DE number 1956493
• Taming effects with monadic typing

Mathematics Subject Classification ID

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

Cited In (7)

• A Realizability Model for Impredicative Hoare Type Theory
• Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
• Higher-order separation logic in Isabelle/HOLCF
• Polymorphism and separation in Hoare type theory
• Verifying object-oriented programs with higher-order separation logic in Coq
• Safety Guarantees from Explicit Resource Management
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits

Uses Software

• JML
• Spec#

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5756495)