Write a Blog >>
APLAS 2020
Mon 30 November - Wed 2 December 2020
Wed 2 Dec 2020 18:00 - 18:30 at online - Semantics Chair(s): Florian Rabe

We present an abstract machine that implements a full-reducing (a.k.a. strong) call-by-value strategy for pure $\lambda$-calculus. It is derived using Danvy et al.’s functional correspondence from Crégut’s KN by: (1) deconstructing KN to a call-by-name normalization-by-evaluation function akin to Filinski and Rohde’s, (2) modifying the resulting normalizer so that it implements the right-to-left call-by-value function application, and (3) constructing the functionally corresponding abstract machine.

This new machine implements a reduction strategy that subsumes the fireball-calculus variant of call by value studied by Accattoli et al. We describe the strong strategy of the machine in terms of a reduction semantics and prove the correctness of the machine using a method based on Biernacka et al’s generalized refocusing. As a byproduct, we present an example application of the machine to efficiently checking term convertibility by discriminating on the basis of their partially normalized forms.

Wed 2 Dec

Displayed time zone: Osaka, Sapporo, Tokyo change

17:30 - 19:00
SemanticsResearch Papers at online
Chair(s): Florian Rabe University of Erlangen
Certified Semantics for Relational Programming
Research Papers
Dmitry Rozplokhas Higher School of Economics and JetBrains Research, Russia, Andrey Vyatkin Saint Petersburg State University, Russia, Dmitri Boulytchev Saint Petersburg State University / JetBrains Research
An Abstract Machine for Strong Call by Value
Research Papers
Malgorzata Biernacka University of Wroclaw, Dariusz Biernacki University of Wrocław, Witold Charatonik Institute of Computer Science, University of Wroclaw, Tomasz Drab Institute of Computer Science, University of Wroclaw
Link to publication
Algebraic and coalgebraic perspectives on interaction laws
Research Papers
Tarmo Uustalu Reykjavik University, Niels Voorneveld Tallinn University of Technology