Search

• < Previous
• 1
• Next >

---

Probabilistic call by push value

Thomas Ehrhard ; Christine Tasson.

We introduce a probabilistic extension of Levy's Call-By-Push-Value. This extension consists simply in adding a " flipping coin " boolean closed atomic expression. This language can be understood as a major generalization of Scott's PCF encompassing both call-by-name and call-by-value and featuring&nbsp;[&hellip;]

---

A coherent differential PCF

Thomas Ehrhard.

The categorical models of the differential lambda-calculus are additive categories because of the Leibniz rule which requires the summation of two expressions. This means that, as far as the differential lambda-calculus and differential linear logic are concerned, these models feature finite&nbsp;[&hellip;]

---