JFP
2008
14 years 3 months 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 5 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
15 years 10 days 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 3 months 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 3 months 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...