Sciweavers

ICFP
2010
ACM
14 years 4 months ago
The gentle art of levitation
We present a closed dependent type theory whose inductive types are given not by a scheme for generative declarations, but by encoding in a universe. Each inductive datatype arise...
James Chapman, Pierre-Évariste Dagand, Cono...