Hoare type theory, polymorphism and separation

DOI10.1017/S0956796808006953zbMath1155.68354OpenAlexW1990409169WikidataQ56504617 ScholiaQ56504617MaRDI QIDQ3546051

Greg Morrisett, Aleksandar Nanevski, Lars Birkedal

Publication date: 18 December 2008

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796808006953

zbMATH Keywords

Hoare-style specifications

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (15)

Crowfoot: A Verifier for Higher-Order Store Programs ⋮ Symbolic execution proofs for higher order store programs ⋮ Towards patterns for heaps and imperative lambdas ⋮ Compositional System Security with Interface-Confined Adversaries ⋮ Specification patterns for reasoning about recursion through the store ⋮ When programs have to watch paint dry ⋮ Mtac: A monad for typed tactic programming in Coq ⋮ Unnamed Item ⋮ Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits ⋮ An Isbell duality theorem for type refinement systems ⋮ Partiality, State and Dependent Types ⋮ Syntactic soundness proof of a type-and-capability system with hidden state ⋮ Building program construction and verification tools from algebraic principles ⋮ Dependent Types and Fibred Computational Effects ⋮ Relational cost analysis in a functional-imperative setting

Uses Software

• SPARK
• Haskell
• JML
• Spec#

Cites Work

• Unnamed Item
• Unnamed Item
• Notions of computation and monads
• Inductive families
• Indexed induction-recursion
• A judgmental reconstruction of modal logic
• Combining programming with theorem proving
• A step-indexed model of substructural state
• A language-based approach to functionally correct imperative programming
• Local reasoning about a copying garbage collector
• Separation and information hiding
• A critique of the foundations of Hoare style programming logics
• Guarded commands, nondeterminacy and formal derivation of programs
• Soundness and Completeness of an Axiom System for Program Verification
• The view from the left
• An effective theory of type refinements
• The marriage of effects and monads
• Cayenne—a language with dependent types
• An axiomatic basis for computer programming
• A formulation of the simple theory of types

This page was built for publication: Hoare type theory, polymorphism and separation