Polymorphism and separation in Hoare type theory

DOI10.1145/1159803.1159812MaRDI QIDQ5501458zbMATH OpenOpenAlexFDO

Authors 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

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

Recommendations

• Hoare type theory, polymorphism and separation
• Abstract Predicates and Mutable ADTs in Hoare Type Theory
• A Realizability Model for Impredicative Hoare Type Theory
• Effect polymorphism in higher-order logic (proof pearl)
• Effect polymorphism in higher-order logic (proof pearl)

Cited in

(20)

• A Realizability Model for Impredicative Hoare Type Theory
• From Monomorphic to Polymorphic Well-Typings and Beyond
• Imperative Functional Programming with Isabelle/HOL
• Extended Static Checking by Calculation Using the Pointfree Transform
• Foundations of mathematics in polymorphic type theory
• Semantics, specification logic, and Hoare logic of exact real computation
• Typed Lambda Calculi and Applications
• Dependently typed array programs don't go wrong
• On polymorphic types of untyped terms
• A Kripke logical relation for effect-based program transformations
• Parameterised notions of computation
• Trace-based verification of imperative programs with I/O
• Comprehensive Parametric Polymorphism: Categorical Models and Type Theory
• Reverse Hoare logic
• Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
• Polymorphism and apartness
• Effect polymorphism in higher-order logic (proof pearl)
• Abstract Predicates and Mutable ADTs in Hoare Type Theory
• Hoare type theory, polymorphism and separation
• A Hoare Logic for the State Monad

This page was built for publication: Polymorphism and separation in Hoare type theory

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