JFP
2008
14 years 13 days ago
2008
We consider the problem of reconciling a dependently typed functional language with imperative features such as mutable higher-order state, pointer aliasing, and non-termination. ...
ESOP
2008
Springer
14 years 2 months ago
2008
Springer
We present a denotational model of impredicative Hoare Type Theory, a very expressive dependent type theory in which one can and reason about mutable abstract data types. The model...
TLDI
2009
ACM
14 years 9 months ago
2009
ACM
We propose a dependent type theory that integrates programming, specifications, and reasoning about higher-order concurrent programs with shared transactional memory. The design ...
ICFP
2006
ACM
15 years 13 days ago
2006
ACM
In previous work, we proposed a Hoare Type Theory (HTT) which combines effectful higher-order functions, dependent types and Hoare Logic specifications into a unified framework. H...
ICFP
2008
ACM
15 years 13 days ago
2008
ACM
We describe an axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher-order, dependently-typed programs with side-effects. C...