Nanevski, AleksandarMorrisett, Greg Gregory2016-04-082005Nanevski, Aleksandar and Greg Morrisett. 2005. Dependent type theory of stateful higher-order functions. Harvard Computer Science Group Technical Report TR-24-05.http://nrs.harvard.edu/urn-3:HUL.InstRepos:26506436In 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.en-USResearch Paper or Report2016-04-08