CPSTranslatingInductiveandCoinductiveTypes
[ExtendedAbstract]
INRIASophia-Antipolis2004routedesLucioles,BP93
F-06902Sophia-AntipolisCedex,France
GillesBarthe
Dep.deInform´atica,UniversidadedoMinho
CampusdeGualtarP-4710-057Braga,Portugal
TarmoUustalu
Gilles.Barthe@inria.fr
ABSTRACT
tarmo@di.uminho.pt
CategoriesandSubjectDescriptors
GeneralTerms
Keywords
1.INTRODUCTION
Background
Organizationofthepaper
2.
SIMPLYTYPEDLAMBDA-CALCULUS
WITHSUMANDPRODUCTTYPES
3.NATURALNUMBERSANDSTREAMS
4.
GENERALPOSITIVEINDUCTIVEAND
COINDUCTIVETYPES
7.CALCULUSOFINDUCTIVECONSTRUC-TIONS
7.1CalculusofConstructions
7.2Sigma-types
7.3Sumtypes
7.4Summary
8.
CONCLUSION
Acknowledgments
9.
REFERENCES