Abstract Predicates and Mutable ADTs in Hoare Type Theory

DOI10.1007/978-3-540-71316-6_14MaRDI QIDQ5756495zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

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

Cited in

(7)

• Verifying object-oriented programs with higher-order separation logic in Coq
• Safety Guarantees from Explicit Resource Management
• Higher-order separation logic in Isabelle/HOLCF
• A Realizability Model for Impredicative Hoare Type Theory
• Polymorphism and separation in Hoare type theory
• 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

Describes a project that uses

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)