Abstract
We explore the duality of construction and deconstruction in the presence of different evaluation strategies. We characterize an evaluation strategy by the notion of substitutability, given by defining what is a value and a co-value, and we present an equational theory that takes the strategy as a parameter. The theory may be extended with new logical connectives, in the form of user-defined data and co-data types, which are duals of one another. Finally, we explore a calculus with composite evaluation strategies that allow for more flexibility over evaluation order by mingling multiple primitive strategies within a single program.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abel, A., Pientka, B., Thibodeau, D., Setzer, A.: Copatterns: programming infinite structures by observations. In: POPL 2013 (2013)
Ariola, Z.M., Herbelin, H., Saurin, A.: Classical call-by-need and duality. In: Ong, L. (ed.) TLCA 2011. LNCS, vol. 6690, pp. 27–44. Springer, Heidelberg (2011)
Curien, P.-L., Herbelin, H.: The duality of computation. In: International Conference on Functional Programming, pp. 233–243 (2000)
Curien, P.-L., Munch-Maccagnoni, G.: The duality of computation under focus. In: Calude, C.S., Sassone, V. (eds.) TCS 2010. IFIP AICT, vol. 323, pp. 165–181. Springer, Heidelberg (2010)
Filinski, A.: Declarative Continuations and Categorical Duality. Master thesis, DIKU, Danmark (August 1989)
Girard, J.-Y.: Linear logic. Theoretical Computer Science 50, 1–102 (1987)
Herbelin, H.: Duality of computation and sequent calculus: a few more remarks (2012), http://pauillac.inria.fr/~herbelin/publis/full-dual-lk.pdf
Munch-Maccagnoni, G.: Focalisation and classical realisability. In: Grädel, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 409–423. Springer, Heidelberg (2009)
Ronchi Della Rocca, S., Paolini, L.: The Parametric λ-Calculus: a Metamodel for Computation. Springer (2004)
Selinger, P.: Control categories and duality: on the categorical semantics of the lambda-mu calculus. MSCS 11(2), 207–260 (2001)
Wadler, P.: Call-by-value is dual to call-by-name. In: Proceedings of ICFP, pp. 189–201. ACM (2003)
Wadler, P.: Call-by-value is dual to call-by-name – reloaded. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 185–203. Springer, Heidelberg (2005)
Zeilberger, N.: On the unity of duality. Annals of Pure Applied Logic 153(1-3), 66–96 (2008)
Zeilberger, N.: The Logical Basis of Evaluation Order and Pattern-Matching. PhD thesis, Carnegie Mellon University (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Downen, P., Ariola, Z.M. (2014). The Duality of Construction. In: Shao, Z. (eds) Programming Languages and Systems. ESOP 2014. Lecture Notes in Computer Science, vol 8410. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54833-8_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-54833-8_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54832-1
Online ISBN: 978-3-642-54833-8
eBook Packages: Computer ScienceComputer Science (R0)