Name
Abstract | ||
|---|---|---|
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. |
Year | Venue | Keywords |
|---|---|---|
2011 | TLCA | fixed point,admissibility condition,underlying type theory,hoare-style partial correctness reasoning,expressive dependent type theory,explicit admissibility condition,partial type theory,fixed-point induction,effectful computation,admissible type |
Field | DocType | Volume |
Separation logic,Inductive type,Algebra,Computer science,Correctness,Algorithm,Type theory,Fixed point,Dependent type,Computation | Conference | 6690 |
ISSN | Citations | PageRank |
0302-9743 | 4 | 0.42 |
References | Authors | |
16 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Kasper Svendsen | 1 | 127 | 6.84 |
| Lars Birkedal | 2 | 1481 | 96.84 |
| Aleksandar Nanevski | 3 | 583 | 27.01 |