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 DecDisplayed time zone: Osaka, Sapporo, Tokyo change

 17:30 - 19:00 SemanticsResearch Papers at online Chair(s): Florian Rabe University of Erlangen 17:3030mTalk Certified Semantics for Relational ProgrammingResearch PapersDmitry Rozplokhas Higher School of Economics and JetBrains Research, Russia, Andrey Vyatkin Saint Petersburg State University, Russia, Dmitri Boulytchev Saint Petersburg State University / JetBrains Research 18:0030mTalk An Abstract Machine for Strong Call by ValueResearch PapersMalgorzata 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 18:3030mTalk Algebraic and coalgebraic perspectives on interaction lawsResearch PapersTarmo Uustalu Reykjavik University, Niels Voorneveld Tallinn University of Technology