Concept
Hoare type theory
Books
Journey Statuslearning Tags
A type theory that integrates Hoare-style specifications into types, allowing pre/postconditions and invariants to be expressed and checked within a dependently typed language.
A Type theory that integrates Hoare logic-style specifications into types, allowing pre/postconditions and invariants to be expressed and checked within a dependently typed language.