Polymorphism and separation in Hoare type theory
DOI10.1145/1159803.1159812zbMATH Open1321.68351OpenAlexW2109772966MaRDI QIDQ5501458FDOQ5501458
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
Recommendations
Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)
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
- Reverse Hoare logic
- Comprehensive Parametric Polymorphism: Categorical Models and Type Theory
- 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)
