scrambled
Concept

Hoare type theory

Modified just now
Books JourneyProgramming Language Theory Statuslearning Tags
  • formal system
  • logic
  • program analysis
  • proof-reason-technique
  • semantics

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.