Conference proceeding
The recursive polarized dual calculus
Proceedings of the ACM SIGPLAN 2014 Workshop on programming languages meets program verification, pp.3-14
PLPV '14
01/11/2014
DOI: 10.1145/2541568.2541575
Abstract
This paper introduces the Recursive Polarized Dual Calculus (RP-DC), based on Wadler's Dual Calculus. RP-DC features a polarized form of reduction, which enables several simplifications over previous related systems. It also adds inductive types with recursion, from which coinductive types with corecursion can be defined. Typing and reduction relations are defined for RP-DC, and we consider several examples of practical programming. Logical consistency is proved, as well as a canonicity theorem showing that all closed values of a certain family of types are canonical. This shows how RP-DC can be used for practical programming, where canonical final results are required.
Details
- Title: Subtitle
- The recursive polarized dual calculus
- Creators
- Aaron Stump - University of Iowa
- Resource Type
- Conference proceeding
- Publication Details
- Proceedings of the ACM SIGPLAN 2014 Workshop on programming languages meets program verification, pp.3-14
- Series
- PLPV '14
- DOI
- 10.1145/2541568.2541575
- Publisher
- ACM
- Language
- English
- Date published
- 01/11/2014
- Academic Unit
- Computer Science
- Record Identifier
- 9984259496702771
Metrics
66 Record Views