Content deleted Content added
Nowhere man (talk | contribs) mNo edit summary |
restore redirect notice Tag: Disambiguation links added |
||
Line 1:
{{Short description|Intermediate language}}
{{Short description|Intermediate language}}In [[programming language theory]], '''call-by-push-value''' (CBPV) is an [[intermediate language]] that embeds the [[call-by-value]] (CBV) and [[call-by-name]] (CBV) [[evaluation strategy|evaluation strategies]]. CBPV is structured as a polarized [[λ-calculus]] with two main types, "values" (+) and "computations" (-).<ref name="Kavvos2020">{{cite journal |last1=Kavvos |first1=G. A. |last2=Morehouse |first2=Edward |last3=Licata |first3=Daniel R. |last4=Danner |first4=Norman |title=Recurrence extraction for functional programs through call-by-push-value |journal=Proceedings of the ACM on Programming Languages |date=January 2020 |volume=4 |issue=POPL |pages=1–31 |doi=10.1145/3371083 |url=https://dl.acm.org/doi/pdf/10.1145/3371083 |language=en |issn=2475-1421}}</ref> Restrictions on interactions between the two types enforce a controlled order of evaluation, similar to [[Monad (functional programming)|monad]]s or [[continuation passing style|CPS]]. The calculus can embed computational effects, such as nontermination, mutable state, or nondeterminism. There are natural semantics-preserving translations from CBV and CBN into CBPV. This means that giving a CBPV semantics and proving its properties implicitly establishes CBV and CBN semantics and properties as well. Paul Blain Levy formulated and developed CBPV in several papers and his doctoral thesis.<ref name="Levy99">{{Cite conference |last=Blain Levy |first=Paul |date=April 1999 |title=Call-by-Push-Value: A Subsuming Paradigm |conference=Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy |series=Lecture Notes in Computer Science |volume=1581 |pages=228–242|url=https://www.cs.bham.ac.uk/~pbl/papers/tlca99.pdf}}</ref><ref name="Levy2003">{{cite book |last1=Levy |first1=Paul Blain |title=Call-by-push-value: a functional/imperative synthesis |date=2003 |publisher=Kluwer Academic Publishers |___location=Dordrecht ; Boston |isbn=978-1-4020-1730-8|url=https://www.cs.bham.ac.uk/~pbl/papers/thesisqmwphd.pdf}}</ref><ref name="Levy2022">{{cite journal |last1=Levy |first1=Paul Blain |title=Call-by-push-value |journal=ACM SIGLOG News |date=April 2022 |volume=9 |issue=2 |pages=7–29 |doi=10.1145/3537668.3537670}}</ref>▼
{{Redirects here|CBPV|the virus that affects bees|Chronic bee paralysis virus}}
▲
== Definition ==
| |||