Partiality, State and Dependent Types

摘要

Partial type theories allow reasoning about recursively-defined computations using fixed-point induction. However, fixed-point induction is only sound for admissible types and not all types are admissible in sufficiently expressive dependent type theories. Previous solutions have either introduced explicit admissibility conditions on the use of fixed points, or limited the underlying type theory. In this paper we propose a third approach, which supports Hoare-style partial correctness reasoning, without admissibility conditions, but at a tradeoff that one cannot reason equationally about effectful computations. The resulting system is still quite expressive and useful in practice, which we confirm by an implementation as an extension of Coq.