Polymorphism and separation in hoare type theory

DOI10.1145/1159803.1159812zbMath1321.68351OpenAlexW2109772966MaRDI QIDQ5501458

Aleksandar Nanevski, Greg Morrisett, Lars Birkedal

Publication date: 3 August 2015

Published in: Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL: http://nrs.harvard.edu/urn-3:HUL.InstRepos:24947964

zbMATH Keywords

type theoryHoare logicseparation logic

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

A Kripke logical relation for effect-based program transformations ⋮ Dependently typed array programs don't go wrong ⋮ A Hoare Logic for the State Monad ⋮ Trace-based verification of imperative programs with I/O ⋮ Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control ⋮ Imperative Functional Programming with Isabelle/HOL ⋮ Extended Static Checking by Calculation Using the Pointfree Transform ⋮ Parameterised notions of computation ⋮ Reverse Hoare Logic