Content deleted Content added
Citation bot (talk | contribs) Added doi-access. | Use this bot. Report bugs. | Suggested by Headbomb | Linked from Wikipedia:WikiProject_Academic_Journals/Journals_cited_by_Wikipedia/Sandbox2 | #UCB_webform_linked 336/1051 |
→Award: m capitalization |
||
| (2 intermediate revisions by 2 users not shown) | |||
Line 31:
== Modifications ==
Some authors have noted that CBPV can be simplified, by removing either the U type constructor (thunks)<ref name="Egger2014">{{cite journal |last1=Egger |first1=J. |last2=Mogelberg |first2=R. E. |last3=Simpson |first3=A. |title=The enriched effect calculus: syntax and semantics |journal=Journal of Logic and Computation |date=1 June 2014 |volume=24 |issue=3 |pages=615–654 |doi=10.1093/logcom/exs025 |url=https://www.pure.ed.ac.uk/ws/portalfiles/portal/12289301/eec.pdf}}</ref> or the F type constructor (computations returning values).<ref name="Ehrhard2016">{{cite book |last1=Ehrhard |first1=Thomas |chapter=Call-By-Push-Value from a Linear Logic Point of View |title=Programming Languages and Systems |series=Lecture Notes in Computer Science |date=2016 |volume=9632 |pages=202–228 |doi=10.1007/978-3-662-49498-1_9|doi-access=free|isbn=978-3-662-49497-4 }}</ref> Egger and Mogelberg justify omitting U on the grounds of streamlined syntax and avoiding the clutter of inferable conversions from computations to values. This choice makes computation types a subset of value types, and it is then natural to expand function types to a full function space between values. They term their calculus the "Enriched Effects Calculus". This modified calculus is equivalent to a superset of CBPV via a bidirectional semantics-preserving translation.<ref name="Egger2014"/> Ehrhard in contrast omits the F type constructor, making values a subset of computations. Ehrhard renames computations to "general types" to better reflect their semantics. This modified calculus, the "half-polarized lambda calculus", has close connections to linear logic.<ref name="Ehrhard2016"/><ref>{{cite book |last1=Chouquet |first1=Jules |last2=Tasson |first2=Christine |title=Taylor expansion for Call-By-Push-Value |date=2020 |publisher=Schloss Dagstuhl – Leibniz-Zentrum für Informatik |series=Leibniz International Proceedings in Informatics |volume=152 |pages=16:1–16:16 |doi=10.4230/LIPIcs.CSL.2020.16 |doi-access=free |isbn=978-3-95977-132-0 |url=https://hal.science/hal-02318600/document}}</ref> It can be translated bidirectionally to a subset of a fully-polarized variant of CBPV.<ref>{{citation |last1=Ehrhard |first1=Thomas |title=A Call-By-Push-Value FPC and its interpretation in Linear Logic |date=July 2015 |url=https://hal.science/hal-01176033/document}}</ref>
== Award ==
Paul Blain Levy received the 2025 [[Alonzo Church Award]] for his work on CBPV.<ref>https://siglog.org/winner-of-the-2025-alonzo-church-award/</ref>
== See also ==
| |||