Skip to content
scrambled
Programming Language Theory Concept

Hoare type theory

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.