Loading...
Please wait, while we are loading the content...
Similar Documents
Dependent type theory of stateful higher-order functions (2006)
| Content Provider | CiteSeerX |
|---|---|
| Author | Nanevski, Aleksandar Morrisett, Greg |
| 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 {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 Turingcomplete imperative language with conditionals, loops, recursion and commands for stateful operations like allocation, lookup and mutation of location content. |
| File Format | |
| Language | English |
| Publisher Date | 2006-01-01 |
| Access Restriction | Open |
| Subject Keyword | Dependent Type Theory Stateful Higher-order Function Hoare Triple Higher-order Function Dependent Type Theory Htt Full Turingcomplete Imperative Language Effectful Fragment Location Content Effectful Program Monadic Language Hoare Type Theory Return Result Program Specification Curry-howard Isomorphism Stateful Operation Pure Fragment Functional Programming Language Effectful Feature |
| Content Type | Text |
| Resource Type | Technical Report |
