Exploring an Abstract Machine for Strong Call-by-Value Evaluation 🔍
Discover the innovative abstract machine designed for strong call-by-value evaluation, presented at APLAS 2020. Learn how this approach advances programming language semantics and implementation techniques.
Tomasz Drab Academic
69 views • Mar 4, 2022
About this video
18th Asian Symposium on Programming Languages and Systems (https://conf.researchr.org/home/aplas-2020)
2nd of December 2020 (day of the talk), held online (originally planned in Fukuoka City, Japan)
Paper: An Abstract Machine for Strong Call by Value (https://doi.org/10.1007/978-3-030-64437-6_8)
Authors' websites:
Małgorzata Biernacka: https://ii.uni.wroc.pl/~mabi/
Dariusz Biernacki: https://ii.uni.wroc.pl/~dabi/
Witold Charatonik: https://ii.uni.wroc.pl/~wch/
Tomasz Drab (presenter): https://ii.uni.wroc.pl/~tdr/
Institute of Computer Science, University of Wrocław (https://ii.uni.wroc.pl)
00:00 Introduction
00:44 Motivation of Strong CbV
02:16 Motivation of abstract machines
05:06 Functional Correspondence as a tool (with an example)
07:44 Overview of the derived machine
10:17 Its formal connection with Strong CbV
14:10 Summary
Abstract:
We present an abstract machine that implements a full-reducing (a.k.a. strong) call-by-value strategy for pure λ-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.
2nd of December 2020 (day of the talk), held online (originally planned in Fukuoka City, Japan)
Paper: An Abstract Machine for Strong Call by Value (https://doi.org/10.1007/978-3-030-64437-6_8)
Authors' websites:
Małgorzata Biernacka: https://ii.uni.wroc.pl/~mabi/
Dariusz Biernacki: https://ii.uni.wroc.pl/~dabi/
Witold Charatonik: https://ii.uni.wroc.pl/~wch/
Tomasz Drab (presenter): https://ii.uni.wroc.pl/~tdr/
Institute of Computer Science, University of Wrocław (https://ii.uni.wroc.pl)
00:00 Introduction
00:44 Motivation of Strong CbV
02:16 Motivation of abstract machines
05:06 Functional Correspondence as a tool (with an example)
07:44 Overview of the derived machine
10:17 Its formal connection with Strong CbV
14:10 Summary
Abstract:
We present an abstract machine that implements a full-reducing (a.k.a. strong) call-by-value strategy for pure λ-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.
Video Information
Views
69
Duration
14:46
Published
Mar 4, 2022