Abstract
We define an extension of Herbelin’s \(\bar\lambda\mu\)-calculus, introducing a product operation on contexts (in the sense of lists of arguments, or stacks in environment machines), similar to the convolution product of distributions. This is the computational couterpart of some new semantical constructions, extending models of Ehrhard-Regnier’s differential interaction nets, along the lines of Laurent’s polarization of linear logic. We demonstrate this correspondence by providing this calculus with a denotational semantics inside a lambda-model in the category of sets and relations.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bucciarelli, A., Ehrhard, T.: An extensional model of the lambda-calculus in the category of sets and relations. Manuscript (2004)
de Carvalho, D.: Execution time of lambda-terms via non uniform semantics and intersection types (2006) Revised version available at http://iml.univ-mrs.fr/c̃arvalho/Pub/computation.pdf
Dougherty, D.J., Ghilezan, S., Lescanne, P.: Intersection and union types in the lambda-bar-mu-mu-tilde-calculus. Electr. Notes Theor. Comput. Sci. 136, 153–172 (2005)
Danos, V., Joinet, J.-B., Schellinx, H.: Sequent calculi for second order logic. In: Girard, J.-Y., Lafont, Y., Regnier, L. (eds.) Advances in Linear Logic, pp. 211–224. Cambridge University Press, Cambridge (1995)
Ehrhard, T.: On Köthe sequence spaces and linear logic. Mathematical Structures in Computer Science 12, 579–623 (2001)
Ehrhard, T.: Finiteness spaces. Mathematical. Structures in Comp. Sci. 15(4), 615–646 (2005)
Ehrhard, T., Regnier, L.: The differential lambda-calculus. Theoretical Computer Science 309, 1–41 (2003)
Ehrhard, T., Regnier, L.: Differential interaction nets. Electr. Notes Theor. Comput. Sci. 123, 35–74 (2005)
Herbelin, H.: Séquents qu’on calcule. Phd thesis, Université Paris 7 (1995)
Lafont, Y.: From proof nets to interaction nets. In: Girard, J.-Y., Lafont, Y., Regnier, L. (eds.) Advances in Linear Logic, pp. 225–247. Cambridge University Press, Cambridge (1995)
Laurent, O.: Etude de la polarisation en logique. Thèse de doctorat, Université Aix-Marseille II (March 2002)
Laurent, O.: Polarized proof-nets and λμ-calculus. Theoretical Computer Science 290(1), 161–188 (2003)
Laurent, O., Regnier, L.: About translations of classical logic into polarized linear logic. In: Proceedings of the 18th annual IEEE symposium on Logic In Comp. Sci., pp. 11–20. IEEE Computer Society Press, Los Alamitos (2003)
Parigot, M.: λμ-calculus: An algorithmic interpretation of classical natural deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190–201. Springer, Heidelberg (1992)
Regnier, L.: Lambda-calcul et réseaux. PhD thesis, Université Paris 7 (1992)
Schwartz, L.: Théorie des distributions. Hermann (1966)
Vaux, L.: λ-calculus in an algebraic setting (2006) Research report, available at http://iml.univ-mrs.fr/Ṽaux/articles/alglam.ps.gz
Vaux, L.: The differential λμ-calculus. Theoretical Computer Science (to appear, 2007) doi:10.1016/j.tcs.2007.02.028
Vaux, L.: Polarized proof nets and differential structures. Unpublished manuscript (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Vaux, L. (2007). Convolution \(\bar\lambda\mu\)-Calculus. In: Della Rocca, S.R. (eds) Typed Lambda Calculi and Applications. TLCA 2007. Lecture Notes in Computer Science, vol 4583. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73228-0_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-73228-0_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73227-3
Online ISBN: 978-3-540-73228-0
eBook Packages: Computer ScienceComputer Science (R0)