Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020
Tue 25 Aug 2020 11:41 - 11:52 at ICFP NY 3 - New York 3 (JFP talks) Chair(s): Jeremy Gibbons
Tue 25 Aug 2020 22:41 - 22:52 at ICFP Asia 3 - Asia 3 (JFP talks) Chair(s): Jeremy Gibbons

We exploit the idea of proving properties of an abstract machine by using a corresponding semantic artefact better suited to their proof. The abstract machine is an improved version of Pierre Crégut’s full-reducing Krivine machine KN. The original version works with closed terms of the pure lambda calculus with de Bruijn indices. The improved version reduces in similar fashion but works on closures where terms may be open. The corresponding semantic artefact is a structural operational semantics of a calculus of closures whose reduction relation is purposely a reduction strategy. As shown in previous work, improved KN and the structural operational semantics ‘correspond’, i.e. both artefacts realise the same reduction strategy. In this paper, we prove in the calculus of closures that the reduction strategy simulates in lockstep (at every reduction step) the complete and standard normal-order strategy (i.e. leftmost reduction to normal form) of the pure lambda calculus. The simulation is witnessed by a substitution function from closures of the closure calculus to pure terms of the pure lambda calculus. Thus, KN also simulates normal-order in lockstep by the correspondence. This result is stronger than the known proof that KN is complete, for in the pure lambda calculus there are complete but non-standard strategies. The lockstep simulation proof consists of straightforward structural inductions, thanks to three properties of the closure calculus we call ‘index alignment’, ‘parameters-as-levels’ and ‘balanced derivations’. The first two come from KN. Thanks to these properties, a proof in a calculus of closures involving de Bruijn indices and de Bruijn levels is unproblematic. There is no lexical adjustment at binding lookup, on-the-fly alpha-conversion or recursive traversals of the term to deal with bound and free variables as in other calculi. This paper contributes to the framework for environment machines of Biernacka and Danvy a full-reducing open-terms closure calculus, its corresponding abstract machine, and a lockstep simulation proof via a substitution function.

Tue 25 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change

11:30 - 13:00: New York 3 (JFP talks)ICFP Program at ICFP NY 3
Chair(s): Jeremy GibbonsDepartment of Computer Science, University of Oxford

Public livestreams: YouTube, Bilibili (China)

11:30 - 11:41
Talk
A theory of RPC calculi for client–server modelJFP
ICFP Program
DOI Media Attached
11:41 - 11:52
Talk
The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculusJFP
ICFP Program
Álvaro García PerezIMDEA Software Institute, Pablo NogueiraESNE University School of Design, Innovation and Technology
DOI Media Attached
11:52 - 12:03
Talk
Local algebraic effect theoriesJFP
ICFP Program
Žiga Lukšič, Matija PretnarUniversity of Ljubljana, Slovenia
DOI Media Attached
12:03 - 12:15
Talk
Heterogeneous binary random-access listsJFP
ICFP Program
Wouter SwierstraUtrecht University, Netherlands
DOI Media Attached
12:15 - 12:26
Talk
POPLMark reloaded: Mechanizing proofs by logical relationsJFP
ICFP Program
Andreas AbelGothenburg University, Guillaume AllaisUniversity of St Andrews, Aliya HameerMcGill University, Brigitte PientkaMcGill University, Alberto Momigliano Università degli Studi di Milano, Steven SchäferGoogle, Aarhus, Kathrin StarkPrinceton University, USA
DOI Media Attached
12:26 - 12:37
Talk
Perturbation confusion in forward automatic differentiation of higher-order functionsJFP
ICFP Program
Oleksandr Manzyuk, Barak A. PearlmutterMaynooth University, Alexey Radul, David Rush, Jeffrey Mark SiskindSchool of Electrical and Computer Engineering, Purdue University
DOI Media Attached
12:37 - 12:48
Talk
Elastic Sheet-Defined Functions: Generalising Spreadsheet Functions to Variable-Size Input ArraysJFP
ICFP Program
Matt McCutchen, Judith Borghouts, Andrew D. GordonMicrosoft Research and University of Edinburgh, Simon Peyton JonesMicrosoft, UK, Advait SarkarMicrosoft Research and University of Cambridge
DOI Pre-print Media Attached
12:48 - 13:00
Talk
Emerging languages: An alternative approach to teaching programming languagesJFP
ICFP Program
Saverio PeruginiUniversity of Dayton
DOI Media Attached
22:30 - 00:00: Asia 3 (JFP talks)ICFP Program at ICFP Asia 3
Chair(s): Jeremy GibbonsDepartment of Computer Science, University of Oxford

Public livestreams: YouTube, Bilibili (China)

22:30 - 22:41
Talk
A theory of RPC calculi for client–server modelJFP
ICFP Program
DOI Media Attached
22:41 - 22:52
Talk
The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculusJFP
ICFP Program
Álvaro García PerezIMDEA Software Institute, Pablo NogueiraESNE University School of Design, Innovation and Technology
DOI Media Attached
22:52 - 23:03
Talk
Local algebraic effect theoriesJFP
ICFP Program
Žiga Lukšič, Matija PretnarUniversity of Ljubljana, Slovenia
DOI Media Attached
23:03 - 23:15
Talk
Heterogeneous binary random-access listsJFP
ICFP Program
Wouter SwierstraUtrecht University, Netherlands
DOI Media Attached
23:15 - 23:26
Talk
POPLMark reloaded: Mechanizing proofs by logical relationsJFP
ICFP Program
Andreas AbelGothenburg University, Guillaume AllaisUniversity of St Andrews, Aliya HameerMcGill University, Brigitte PientkaMcGill University, Alberto Momigliano Università degli Studi di Milano, Steven SchäferGoogle, Aarhus, Kathrin StarkPrinceton University, USA
DOI Media Attached
23:26 - 23:37
Talk
Perturbation confusion in forward automatic differentiation of higher-order functionsJFP
ICFP Program
Oleksandr Manzyuk, Barak A. PearlmutterMaynooth University, Alexey Radul, David Rush, Jeffrey Mark SiskindSchool of Electrical and Computer Engineering, Purdue University
DOI Media Attached
23:37 - 23:48
Talk
Elastic Sheet-Defined Functions: Generalising Spreadsheet Functions to Variable-Size Input ArraysJFP
ICFP Program
Matt McCutchen, Judith Borghouts, Andrew D. GordonMicrosoft Research and University of Edinburgh, Simon Peyton JonesMicrosoft, UK, Advait SarkarMicrosoft Research and University of Cambridge
DOI Pre-print Media Attached
23:48 - 00:00
Talk
Emerging languages: An alternative approach to teaching programming languagesJFP
ICFP Program
Saverio PeruginiUniversity of Dayton
DOI Media Attached