-
Notifications
You must be signed in to change notification settings - Fork 6
Abstracts.2019.CBPV
Fabian edited this page Mar 5, 2020
·
28 revisions
A value is, a computation does.
CBPV decomposes the monad of Moggi and Filinski into an adjunction.
The belief that the categorical semantics of functionspace in call-by-name are easy is a consequence of a longstanding bias (going back to Church) towards functionspace, at the expense of other connectives. Try formulating a categorical semantics for sum type in call-by-name.
- Paul Blain Levy. 2001. "Call-By-Push-Value". FAQ, course notes, book.
- Andreas Abel and Christian Sattler. 2019. "Normalization by Evaluation for Call-by-Push-Value and Polarized Lambda-Calculus".