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. © 2011 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Svendsen, K., Birkedal, L., & Nanevski, A. (2011). Partiality, state and dependent types. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6690 LNCS, pp. 198–212). https://doi.org/10.1007/978-3-642-21691-6_17
Mendeley helps you to discover research relevant for your work.