ICFP 2021
Sun 22 - Sat 28 August 2021
Mon 23 Aug 2021 19:10 - 19:16 at Student Research Competition - SRC Poster Session

It is known that abstract machines can be derived from calculi with explicit substitutions through well-understood program transformations. Formalising them in dependently-typed programming languages allows for obtaining machines proven to be correct. This work introduces the Agda formalisation of an executable and terminating CEK machine, obtained from simply typed call-by-value λp̂-calculus. The novel contributions have been the successful extension of Swierstra’s previous research on the Krivine machine to a broader case, as well as providing elegant Tait-style proof of Strong Normalisation of call-by-value λp̂-calculus.

Graduate of BSc Computer Science at the University of Southampton, interested in Programming Language Theory and Verification. From September, I will be a PhD student at UCL supervised by Prof. Alexandra Silva. Currently interning at Goldman Sachs in London and previously worked at Software and Large Scale Systems Research Group at ARM in Cambridge.

Mon 23 Aug

Displayed time zone: Seoul change

18:30 - 19:30
18:30
6m
Poster
A Linear Temporal Logic with Heartbeat
Student Research Competition
18:36
6m
Poster
An Interactive Stepper for Expression with Holes
Student Research Competition
Yanjun Chen University of Michigan
18:43
6m
Poster
Automatic concurrency with free applicatives/monads, side effects supported
Student Research Competition
18:50
6m
Poster
Compilation of a functional shading language to a SPIR-V intermediate representation
Student Research Competition
Andrzej Swatowski University of Warsaw
18:56
6m
Poster
Composable, Modular Probabilistic Models
Student Research Competition
Minh Nguyen University of Bristol
19:03
6m
Poster
Distilling Sparse Linear Algebra
Student Research Competition
19:10
6m
Poster
Formally verified derivation of an executable and terminating CEK machine from call-by-value λp̂-calculus
Student Research Competition
Wojciech Różowski University of Southampton
19:16
6m
Poster
Mechanizing an elaboration algorithm for the Hindley-Damas-Milner system
Student Research Competition
19:23
6m
Poster
Ungenerators
Student Research Competition
Harrison Goldstein University of Pennsylvania