xOur data center is currently experiencing power issues. Our colleagues are working hard to resolve the issue and keep downtime to a minimum.
ICFP 2021
Sun 22 - Sat 28 August 2021
Wed 25 Aug 2021 19:45 - 20:00 at ICFP Talks - Session 6
Thu 26 Aug 2021 07:45 - 08:00 at ICFP Talks - Session 6

Rigorous reasoning about programs calls for some amount of bureaucracy in managing details like variable binding, but, in guiding students through big ideas in semantics, we might hope to minimize the overhead. We describe our experiment introducing a range of such ideas, using the Coq proof assistant, without any explicit representation of variables, instead using a higher-order syntax encoding that we dub "mixed embedding": it is neither the fully explicit syntax of deep embeddings nor the syntax-free programming of shallow embeddings. Marquee examples include different takes on concurrency reasoning, including in the traditions of model checking (partial-order reduction), program logics (concurrent separation logic), and type checking (session types) – all presented without any side conditions on variables.

Started hacking on compilers & web-development tools in the late 1990s. Finished CS undergrad at Carnegie Mellon in 2003 and CS PhD at Berkeley in 2007, picking up mechanized proof of executable, decently practical systems with Coq as a main focus in between. Postdoc at Harvard through 2011, then faculty at MIT since. Author of Certified Programming with Dependent Types, a popular online & in-print introduction to using Coq at scale. Lately into building practical but clean-slate hardware-software stacks with end-to-end Coq proofs of everything digital, at the same time as developing a startup-company idea to trick ordinary people into using dependent types (with Ur/Web) to generate their business applications.

Wed 25 Aug

Displayed time zone: Seoul change

19:00 - 20:45
19:00
15m
Talk
Newly-Single and Loving It: Improving Higher-Order Must-Alias Analysis with Heap Fragments
Research Papers
Kimball Germane Brigham Young University, Jay McCarthy University of Massachusetts Lowell
DOI Media Attached
19:15
15m
Talk
Grafs: Declarative Graph Analytics
Research Papers
Farzin Houshmand University of California at Riverside, Mohsen Lesani University of California at Riverside, Keval Vora Simon Fraser University
DOI Media Attached
19:30
15m
Talk
Certifying the Synthesis of Heap-Manipulating Programs
Research Papers
Yasunari Watanabe Yale-NUS College; National University of Singapore, Kiran Gopinathan National University of Singapore, George Pîrlea National University of Singapore, Singapore, Nadia Polikarpova University of California at San Diego, Ilya Sergey National University of Singapore
DOI Pre-print Media Attached
19:45
15m
Talk
Skipping the Binder Bureaucracy with Mixed Embeddings in a Semantics Course (Functional Pearl)
Research Papers
Adam Chlipala Massachusetts Institute of Technology
DOI Media Attached
20:00
15m
Talk
GhostCell: Separating Permissions from Data in Rust
Research Papers
Joshua Yanovski MPI-SWS, Hoang-Hai Dang MPI-SWS, Ralf Jung MPI-SWS, Derek Dreyer MPI-SWS
DOI Media Attached
20:15
15m
Talk
Catala: A Programming Language for the Law
Research Papers
Denis Merigoux INRIA, Nicolas Chataing ENS Paris, Jonathan Protzenko Microsoft Research, Redmond
DOI Media Attached
20:30
15m
Talk
Persistent Software Transactional Memory in Haskell
Research Papers
Nicolas Krauter Johannes Gutenberg University Mainz, Patrick Raaf Johannes Gutenberg University Mainz, Peter Braam University of Oxford, Reza Salkordeh Johannes Gutenberg-Universität Mainz, Sebastian Erdweg JGU Mainz, André Brinkmann Johannes Gutenberg U Mainz
DOI Media Attached

Thu 26 Aug

Displayed time zone: Seoul change

07:00 - 08:45
Session 6Research Papers at ICFP Talks
07:00
15m
Talk
Newly-Single and Loving It: Improving Higher-Order Must-Alias Analysis with Heap Fragments
Research Papers
Kimball Germane Brigham Young University, Jay McCarthy University of Massachusetts Lowell
DOI Media Attached
07:15
15m
Talk
Grafs: Declarative Graph Analytics
Research Papers
Farzin Houshmand University of California at Riverside, Mohsen Lesani University of California at Riverside, Keval Vora Simon Fraser University
DOI Media Attached
07:30
15m
Talk
Certifying the Synthesis of Heap-Manipulating Programs
Research Papers
Yasunari Watanabe Yale-NUS College; National University of Singapore, Kiran Gopinathan National University of Singapore, George Pîrlea National University of Singapore, Singapore, Nadia Polikarpova University of California at San Diego, Ilya Sergey National University of Singapore
DOI Pre-print Media Attached
07:45
15m
Talk
Skipping the Binder Bureaucracy with Mixed Embeddings in a Semantics Course (Functional Pearl)
Research Papers
Adam Chlipala Massachusetts Institute of Technology
DOI Media Attached
08:00
15m
Talk
GhostCell: Separating Permissions from Data in Rust
Research Papers
Joshua Yanovski MPI-SWS, Hoang-Hai Dang MPI-SWS, Ralf Jung MPI-SWS, Derek Dreyer MPI-SWS
DOI Media Attached
08:15
15m
Talk
Catala: A Programming Language for the Law
Research Papers
Denis Merigoux INRIA, Nicolas Chataing ENS Paris, Jonathan Protzenko Microsoft Research, Redmond
DOI Media Attached
08:30
15m
Talk
Persistent Software Transactional Memory in Haskell
Research Papers
Nicolas Krauter Johannes Gutenberg University Mainz, Patrick Raaf Johannes Gutenberg University Mainz, Peter Braam University of Oxford, Reza Salkordeh Johannes Gutenberg-Universität Mainz, Sebastian Erdweg JGU Mainz, André Brinkmann Johannes Gutenberg U Mainz
DOI Media Attached