A Realizability Model for Impredicative Hoare Type Theory

DOI10.1007/978-3-540-78739-6_26zbMath1133.68311OpenAlexW2152899988MaRDI QIDQ5458408

Rasmus L. Petersen, Aleksandar Nanevski, Greg Morrisett, Lars Birkedal

Publication date: 11 April 2008

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

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Abstract data types; algebraic specification (68Q65)

Related Items (5)

Specification patterns for reasoning about recursion through the store ⋮ Trace-based verification of imperative programs with I/O ⋮ Partiality, State and Dependent Types ⋮ Realisability semantics of parametric polymorphism, general references and recursive types ⋮ Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types

Uses Software

• JML
• Spec#

This page was built for publication: A Realizability Model for Impredicative Hoare Type Theory