A Diamond Machine for Strong Evaluation
Abstract machines for strong evaluation of the λ-calculus enter into arguments and have a set of transitions for backtracking out of an evaluated argument. We study a new abstract machine which avoids backtracking by splitting the run of the machine in smaller jobs, one for argument, and that jumps directly to the next job once one is finished.
Usually, machines are also deterministic and implement deterministic strategies. Here we weaken this aspect and consider a light form of non-determinism, namely the diamond property, for both the machine and the strategy. For the machine, this introduces a modular management of jobs, parametric in a scheduling policy. We then show how to obtain various strategies, among which leftmost-outermost evaluation.
Mon 27 NovDisplayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change
13:30 - 15:00 | |||
13:30 30mTalk | A Diamond Machine for Strong Evaluation APLAS 2023 Beniamino Accattoli Inria & Ecole Polytechnique, Pablo Barenbaum Universidad Nacional de Quilmes (CONICET) & Universidad de Buenos Aires | ||
14:00 30mTalk | Proofs as Terms, Terms as Graphs APLAS 2023 Jui-Hsuan Wu Institut Polytechnique de Paris | ||
14:30 30mTalk | Typed Non-determinism in Functional and Concurrent Calculi APLAS 2023 Bas van den Heuvel University of Groningen, Joseph Paulus , Daniele Nantes-Sobrinho Imperial College London, Jorge A. Pérez University of Groningen |