%0 Report %1 nanevski-deptt-hof %A Nanevski, Aleks %A Morrisett, Greg %C Cambridge, MA, USA %D 2005 %I Harvard University %K imported %N TR-24-05 %T Dependent Type Theory of Stateful Higher-Order Functions %X 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 Px:AQ 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 Turingcomplete imperative language with conditionals, loops, recursion and commands for stateful operations like allocation, lookup and mutation of location content.

@techreport{nanevski-deptt-hof, abstract = {{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 Px:AQ 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 Turingcomplete imperative language with conditionals, loops, recursion and commands for stateful operations like allocation, lookup and mutation of location content. }}, added-at = {2010-08-25T08:47:38.000+0200}, address = {{Cambridge, MA, USA}}, author = {Nanevski, Aleks and Morrisett, Greg}, biburl = {https://www.bibsonomy.org/bibtex/2e8abafe2df3812d89f4b3ffbe8021ede/miguel.pagano}, institution = {{Harvard University}}, interhash = {e4996e1c70950ba28566584a282cd988}, intrahash = {e8abafe2df3812d89f4b3ffbe8021ede}, keywords = {imported}, month = {{January}}, number = {{TR-24-05}}, pdf = {{ftp://ftp.deas.harvard.edu/techreports/tr-24-05.pdf}}, printed = {{TT}}, publisher = {{Harvard University}}, timestamp = {2010-08-25T08:47:44.000+0200}, title = {{Dependent Type Theory of Stateful Higher-Order Functions}}, year = {{2005}} }