Polymorphism and separation in Hoare type theory
From MaRDI portal
Publication:5501458
Recommendations
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)