Name
Abstract | ||
|---|---|---|
This paper gives an extension of Dual Calculus by introducing inductive types and coinductive types. The same duality as Dual Calculus is shown to hold in the new system, that is, this paper presents its involution for the new system and proves that it preserves both typing and reduction. The duality between inductive types and coinductive types is shown by the existence of the involution that maps an inductive type and a coinductive type to each other. The strong normalization in this system is also proved. First, strong normalization in second-order Dual Calculus is shown by translating it into second-order symmetric lambda calculus. Next, strong normalization in Dual Calculus with inductive and coinductive types is proved by translating it into second-order Dual Calculus. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-02348-4_16 | RTA |
Keywords | Field | DocType |
dual calculus,coinductive type,inductive type,coinductive types,new system,strong normalization,second-order dual calculus,second order,lambda calculus | Discrete mathematics,Inductive type,Lambda calculus,Simply typed lambda calculus,Typed lambda calculus,Algorithm,Sequent calculus,Time-scale calculus,Church encoding,Duality (optimization),Mathematics,Calculus | Conference |
Volume | ISSN | Citations |
5595 | 0302-9743 | 3 |
PageRank | References | Authors |
0.44 | 19 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Daisuke Kimura | 1 | 3 | 0.44 |
| Makoto Tatsuta | 2 | 111 | 22.36 |