Dependent type theory of stateful higher-order functions
Aleksandar Nanevski, Greg Morrisett · Digital Access to Scholarship at Harvard (DASH) (Harvard University) · 2005
In this paper we investigate a logic for reasoning about programs with higher-order functions and effectful features like non-termination and state with aliasing. We propose a dependent type theory HTT (short for Hoare Type Theory), where types serve as program specifications. In case of effectful programs, the type of Hoare triples {P}x:A{Q} specifies the precondition P, the type of the return result A, and the postcondition Q. By Curry-Howard isomorphism, a dependent type theory may be viewed as a functional programming language. From this perspective, the type of Hoare triples is a monad, and HTT is a monadic language, whose pure fragment consists of higher-order functions, while the effectful fragment is a full Turing-complete imperative language with conditionals, loops, recursion and commands for stateful operations like allocation, lookup and mutation of location content.