DependentTypeTheoryAndImperativeComputation
Dependent type theory and imperative computation
Many efficient algorithms rely on low-level management of memory, such as pointer manipulation. Originally, such low-level management was not available in functional programming languages. However, in modern functional programming languages such as ML and Haskell, it is possible to integrate it with ordinary functional computations. In ML the type system is extended with reference types and new constructs for manipulating references. In Haskell monads are used to encapsulate computation which is impure from the functional point of view. For example, stateful computation is encapsulated using the state monad.
When programming in a functional language with dependent types, such as the Agda languages developed at Chalmers, we would also like to have access to low-level manipulation of memory in a similar way as in Haskell or as in ML. However, the rich types system provided by dependent types provides new possibilities. For example, we an now express logical pre- and post-conditions using types. However, it is not so clear how to keep the resulting logical complexity under control. It is a current hot topic to integrate dependent types and stateful computation. Two of the main research efforts in this direction is the Hoare Type Theory developed by Gregg Morrisette at Harvard, and the Krakatoa System developed by Christine Paulin at Paris Sud.
In this project we would like to investigate how such ideas could be integrate in the Agda language. Libaries for imperative computations using state monads could be developed. New axioms a la those of Hoare Type Theory could be considered.
contact person: Peter Dybjer