Positive Sharing and Abstract MachinesRemote Talk
This program is tentative and subject to change.
Wu’s positive $\lambda$-calculus is a recent call-by-value $\lambda$-calculus with sharing coming from Miller and Wu’s study of the proof theoretical concept of focalization. Accattoli and Wu showed that it simplifies a technical aspect of the study of sharing; namely it rules out the recurrent issue of renaming chains, that often causes a quadratic time slowdown.
In this paper, we define the natural abstract machine for the positive $\lambda$-calculus and show that it suffers from an inefficiency: the quadratic slowdown somehow reappears when analyzing the cost of the machine. We then design an optimized machine for the positive $\lambda$-calculus, which we prove efficient. The optimization is based on a new slicing technique which is dual to the standard structure of machine environments.
This program is tentative and subject to change.
Tue 28 OctDisplayed time zone: Chennai, Kolkata, Mumbai, New Delhi change
14:00 - 15:30 | Control, Effects, and DecidabilityResearch Papers at R104 Chair(s): Sanjiva Prasad Indian Institute of Technology Delhi | ||
14:00 30mTalk | Reachability is Decidable for ATM-Typable Finitary PCF with Effect Handlers Research Papers | ||
14:30 30mTalk | Expressive Power of One-Shot Control Operators and CoroutinesIn Person Talk Research Papers | ||
15:00 30mTalk | Positive Sharing and Abstract MachinesRemote Talk Research Papers Beniamino Accattoli Inria & Ecole Polytechnique, Claudio Sacerdoti Coen University of Bologna, Jui-Hsuan Wu CNRS - ENS Lyon - Université Claude Bernard Lyon 1 - LIP - UMR 5668 | ||