Name
Abstract | ||
|---|---|---|
It is natural to present subtyping for recursive types coinductively. However, Gapeyev, Levin and Pierce have noted that there
is a problem with coinductive definitions of non-trivial transitive inference systems: they cannot be “declarative”—as opposed
to “algorithmic” or syntax-directed—because coinductive inference systems with an explicit rule of transitivity are trivial.
We propose a solution to this problem. By using mixed induction and coinduction we define an inference system for subtyping
which combines the advantages of coinduction with the convenience of an explicit rule of transitivity. The definition uses
coinduction for the structural rules, and induction for the rule of transitivity. We also discuss under what conditions this
technique can be used when defining other inference systems.
The developments presented in the paper have been mechanised using Agda, a dependently typed programming language and proof
assistant.
|
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-13321-3_8 | MPC |
DocType | Citations | PageRank |
Conference | 2 | 0.38 |
References | Authors | |
1 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Nils Anders Danielsson | 1 | 100 | 8.26 |
| Thorsten Altenkirch | 2 | 668 | 56.85 |