Thomas Ehrhard
ABSTRACT
We introduce and study the Bang Calculus, an untyped functional calculus in which the promotion operation of Linear Logic is made explicit and where application is a bilinear operation. This calculus, which can be understood as an untyped version of Call-By-Push-Value, subsumes both Call-By-Name and Call-By-Value lambda-calculi, factorizing the Girard's translations of these calculi in Linear Logic. We build a denotational model of the Bang Calculus based on the relational interpretation of Linear Logic and prove an adequacy theorem by means of a resource Bang Calculus whose design is based on Differential Linear Logic.
- S. Abramsky. Computational Interpretations of Linear Logic. Theor. Comput. Sci., 111(1&2):3--57, 1993. Google Scholar
Digital Library
- B. Accattoli. Proof nets and the call-by-value λ-calculus. Theoretical Computer Science, 606:2--24, 2015. Google ScholarDigital Library
- B. Accattoli, P. Barenbaum, and D. Mazza. Distilling abstract machines. In J. Jeuring and M. M. T. Chakravarty, editors, Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, pages 363--376. ACM, 2014. Google ScholarDigital Library
- B. Accattoli and D. Kesner. Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus. Logical Methods in Computer Science, 8(1), 2012.Google Scholar
- B. Accattoli and L. Paolini. Call-by-Value Solvability, Revisited. In FLOPS, pages 4--16, 2012. Google ScholarDigital Library
- Z. M. Ariola, J. Maraist, M. Odersky, M. Felleisen, and P. Wadler. A Call-by-need Lambda Calculus. In Proceedings of the 22Nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '95, pages 233--246, New York, NY, USA, 1995. ACM. Google ScholarDigital Library
- H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundation of Mathematics. North-Holland, Amsterdam, 1984.Google Scholar
- P. N. Benton and P. Wadler. Linear Logic, Monads and the Lambda Calculus. In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, pages 420--431. IEEE Computer Society, 1996. Google ScholarDigital Library
- A. Bucciarelli and T. Ehrhard. On phase semantics and denotational semantics: the exponentials. Annals of Pure and Applied Logic, 109(3):205--241, 2001.Google ScholarCross Ref
- A. Carraro and G. Guerrieri. A semantical and operational account of call-by-value solvability. In A. Muscholl, editor, Foundations of Software Science and Computation Structures - FOSSACS 2014, volume 8412 of Lecture Notes in Computer Science, pages 103--118. Springer, 2014.Google Scholar
- P.-L. Curien and H. Herbelin. The duality of computation. In M. Odersky and P. Wadler, editors, Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), pages 233--243. ACM, 2000. Google ScholarDigital Library
- V. Danos. La Logique Linéaire appliqué à l'étude de divers processus de normalisation (principalement du λ-calcul). PhD thesis, Université Paris 7.Google Scholar
- V. Danos and T. Ehrhard. Probabilistic coherence spaces as a model of higher-order probabilistic computation. Information and Computation, 152(1):111--137, 2011. Google ScholarDigital Library
- D. de Carvalho. Execution Time of lambda-Terms via Denotational Semantics and Intersection Types. Mathematical Structures in Computer Science, 2009. To appear.Google Scholar
- D. de Carvalho. The relational model is injective for Multiplicative Exponential Linear Logic. CoRR, abs/1502.02404, 2015.Google Scholar
- D. de Carvalho and L. Tortora de Falco. The relational model is injective for multiplicative exponential linear logic (without weakenings). Ann. Pure Appl. Logic, 163(9):1210--1236, 2012.Google ScholarCross Ref
- T. Ehrhard. Collapsing non-idempotent intersection types. In CSL, pages 259--273, 2012.Google Scholar
- T. Ehrhard. An introduction to Differential Linear Logic: proof-nets, models and antiderivatives. Mathematical Structures in Computer Science, 2015. To appear.Google Scholar
- T. Ehrhard. Call-By-Push-Value from a Linear Logic point of view. In Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Proceedings, volume 9632 of Lecture Notes in Computer Science, pages 202--228. Springer, 2016.Google Scholar
- T. Ehrhard and L. Regnier. Böhm Trees, Krivine's Machine and the Taylor Expansion of Lambda-Terms. In CiE, volume 3988 of LNCS, pages 186--197. Springer, 2006. Google ScholarDigital Library
- T. Ehrhard and L. Regnier. Differential interaction nets. Theoretical Computer Science, 364(2):166--195, 2006. Google ScholarDigital Library
- T. Ehrhard and L. Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. Theoretical Computer Science, 403(2-3):347--372, 2008. Google ScholarDigital Library
- J.-Y. Girard. Linear Logic. Theoretical Computer Science, 50(1):1--102, 1987. Google ScholarDigital Library
- G. Guerrieri. Head reduction and normalization in a call-by-value lambda-calculus. In N. Nishida et al., editors, Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015, volume 46 of OASICS, pages 3--17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015.Google Scholar
- G. Guerrieri, L. Paolini, and S. Ronchi Della Rocca. Standardization of a Call-By-Value Lambda-Calculus. In T. Altenkirch, editor, Typed Lambda Calculi and Applications, TLCA 2015, volume 38 of LIPIcs, pages 211--225. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015.Google Scholar
- G. Guerrieri, L. Pellissier, and L. Tortora de Falco. Computing Connected Proof(-Structure)s From Their Taylor Expansion. In D. Kesner and B. Pientka, editors, 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, volume 52 of LIPIcs, pages 20:1--20:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.Google Scholar
- D. Kesner. Reasoning About Call-by-need by Means of Types. In B. Jacobs and C. Löding, editors, Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Proceedings, volume 9634 of Lecture Notes in Computer Science, pages 424--441. Springer, 2016.Google Scholar
- O. Laurent. Polarized proof-nets and λμ-calculus. Theoretical Computer Science, 290(1):161--188, 2003. Google ScholarDigital Library
- O. Laurent and L. Regnier. About Translations of Classical Logic into Polarized Linear Logic. In 18th IEEE Symposium on Logic in Computer Science (LICS 2003), Proceedings, pages 11--20. IEEE Computer Society, 2003. Google ScholarDigital Library
- P. B. Levy. Call-by-Push-Value: A Subsuming Paradigm. In J.-Y. Girard, editor, Typed Lambda Calculi and Applications, TLCA'99, Proceedings, volume 1581 of Lecture Notes in Computer Science, pages 228--242. Springer, 1999. Google ScholarDigital Library
- P. B. Levy. Call-by-push-value: Decomposing call-by-value and call-by-name. Higher-Order and Symbolic Computation, 19(4):377--414, 2006. Google ScholarDigital Library
- P. Lincoln and J. C. Mitchell. Operational aspects of linear lambda calculus. In Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), pages 235--246. IEEE Computer Society, 1992.Google ScholarCross Ref
- G. Manzonetto and M. Pagani. Böhm's Theorem for Resource Lambda Calculus through Taylor Expansion. In TLCA 2011, pages 153--168, 2011. Google ScholarDigital Library
- J. Maraist, M. Odersky, D. N. Turner, and P. Wadler. Call-by-name, Call-by-value, Call-by-need and the Linear lambda Calculus. Theoretical Computer Science, 228(1-2):175--210, 1999. Google ScholarDigital Library
- P.-A. Melliès. Categorical semantics of linear logic. In Interactive models of computation and program behaviour, volume 27 of Panoramas et Synthèses. Société Mathématique de France, 2009.Google Scholar
- E. Moggi. Computational Lambda-Calculus and Monads. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), pages 14--23. IEEE Computer Society, 1989. Google ScholarDigital Library
- E. Moggi. Notions of Computation and Monads. Inf. Comput., 93(1):55--92, 1991. Google ScholarDigital Library
- L. Paolini, M. Piccolo, and S. Ronchi Della Rocca. Essential and relational models. Mathematical Structures in Computer Science, FirstView:1--25, 2015.Google Scholar
- L. Paolini and S. Ronchi Della Rocca. Call-by-value Solvability. ITA, 33(6):507--534, 1999.Google Scholar
- G. D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1(2):125--159, 1975.Google ScholarCross Ref
- L. Regnier. Lambda calcul et réseaux. PhD thesis, Université Paris 7, 1992.Google Scholar
- L. Regnier. Une équivalence sur les lambda-termes. Theor. Comput. Sci., 126(2):281--292, 1994. Google ScholarDigital Library
- S. Ronchi della Rocca and L. Paolini. The Parametric λ-calculus: a Metamodel for Computation. Texts in Theoretical Computer Science. Springer, Berlin, 2004. Google ScholarDigital Library
- M. Takahashi. Parallel Reductions in lambda-Calculus. Inf. Comput., 118(1):120--127, 1995. Google ScholarDigital Library
Index Terms
- The Bang Calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value
Recommendations
Call-by-push-value: Decomposing call-by-value and call-by-name
We present the call-by-push-value (CBPV) calculus, which decomposes the typed call-by-value (CBV) and typed call-by-name (CBN) paradigms into fine-grain primitives. On the operational side, we give big-step semantics and a stack machine for CBPV, which ...
Proofs, tests and continuation passing style
The concept of syntactical duality is central in logic. In particular, the duality defined by classical negation, or more syntactically by left and right in sequents, has been widely used to relate logic and computations. We study the proof/test duality ...
Call-by-push-value in Coq: operational, equational, and denotational theory
CPP 2019: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and ProofsCall-by-push-value (CBPV) is an idealised calculus for functional and imperative programming, introduced as a subsuming paradigm for both call-by-value (CBV) and call-by-name (CBN). We formalise weak and strong operational semantics for (effect-free) ...
Comments