Write a Blog >>
ICFP 2020
Thu 20 - Fri 28 August 2020

Dates
Rooms
Tracks
Badges
Your Program
You're viewing the program in a time zone which is different from your device's time zone - change time zone

Thu 20 Aug

Displayed time zone: Eastern Time (US & Canada) change

21:00 - 22:00
Clowdr TrainingClowdr Training at ICFP Social
21:00
60m
Other
Clowdr Training Sessions
Clowdr Training
Benjamin C. Pierce University of Pennsylvania

Fri 21 Aug

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:00
Clowdr TrainingClowdr Training at ICFP Social
09:00
60m
Other
Clowdr Training Sessions
Clowdr Training
Benjamin C. Pierce University of Pennsylvania

Sun 23 Aug

Displayed time zone: Eastern Time (US & Canada) change

07:50 - 09:30
Session 1Erlang at Erlang
Chair(s): Viktória Fördős Cisco Systems
07:50
10m
Day opening
Opening
Erlang
Annette Bieniusa Technische Universität Kaiserslautern, Viktória Fördős Cisco Systems
08:00
30m
Short-paper
Transformations towards Clean Functional Code
Erlang
Boldizsár Poór Eötvös Loránd University, Melinda Tóth Eötvös Loránd University, Faculty of Informatics, Department of Programming Languages and Compilers & ELTE-Soft Nonprofit Ltd., István Bozó Eötvös Loránd University
DOI
08:30
30m
Talk
Supporting Secure Coding with RefactorErl
Erlang
Brigitta Baranyai ELTE Eötvös Loránd University, István Bozó Eötvös Loránd University, Melinda Tóth Eötvös Loránd University, Faculty of Informatics, Department of Programming Languages and Compilers & ELTE-Soft Nonprofit Ltd.
09:00
30m
Full-paper
Teaching Practical Realistic Verification of Distributed Algorithms in Erlang with TLA+
Erlang
Peter Zeller TU Kaiserslautern, Annette Bieniusa Technische Universität Kaiserslautern, Carla Ferreira Universidade Nova Lisboa
DOI
08:00 - 11:30
Keynote and Session 1HOPE at HOPE
08:00
60m
Keynote
Variants of call-by-push-value
HOPE
Paul Blain Levy University of Birmingham
09:15
45m
Talk
Kripke open relations and operational game semantics
HOPE
Guilhem Jaber Université de Nantes, Andrzej Murawski University of Oxford
10:00
45m
Talk
Merging coeffect production into effect handling
HOPE
Tarmo Uustalu Reykjavik University, Tallinn University of Technology, Niels Voorneveld Tallinn University of Technology
10:45
45m
Talk
Simply RaTT: A Fitch-style Modal Calculus for Reactive Programming
HOPE
Patrick Bahr IT University of Copenhagen, Christian Uldal Graulund IT University of Copenhagen, Rasmus Ejlers Møgelberg IT University of Copenhagen
09:00 - 10:00
09:00
15m
Day opening
Welcome
PLMW @ ICFP
Lindsey Kuper University of California, Santa Cruz, Talia Ringer University of Washington, Nate Foster Cornell University
09:15
45m
Talk
How To Write Papers So People Can Read Them
PLMW @ ICFP
Derek Dreyer MPI-SWS
09:00 - 12:30
Teaching Functional ProgrammingTutorials at Tutorials 1
09:00
3h30m
Tutorial
Teaching Functional Programming
Tutorials
Michael Sperber Active Group GmbH
09:00 - 12:30
Audio, Video & Web Live Coding in HaskellTutorials at Tutorials 2
09:00
3h30m
Tutorial
Audio, Video & Web Live Coding in Haskell
Tutorials
Manuel Bärenz sonnen eServices GmbH
Pre-print
10:00 - 10:30
Social 1Erlang at Erlang
10:00
30m
Social Event
Social 1
Erlang

10:00 - 11:30
Session 1TyDe at TyDe
10:00
30m
Talk
Practical Dependent Type Checking Using Twin Types
TyDe
Víctor López Juan Chalmers University of Technology, Nils Anders Danielsson University of Gothenburg, Chalmers University of Technology
Media Attached
10:30
30m
Talk
Shallowly Embedding Type Theories as Presheaf Models in Agda (Extended Abstract)
TyDe
Joris Ceulemans Vrije Universiteit Brussel, Dominique Devriese Vrije Universiteit Brussel
File Attached
11:00
30m
Talk
Generalization of Meta-Programs with Dependent Types in Mtac2 with Mtac2 (Extended Abstract)
TyDe
Ignacio Tiraboschi None, Jan-Oliver Kaiser MPI-SWS, Beta Ziliani FAMAF, UNC and CONICET
10:30 - 12:00
Session 2Erlang at Erlang
Chair(s): Annette Bieniusa Technische Universität Kaiserslautern
10:30
30m
Full-paper
Machine-Checked Natural Semantics for Core Erlang: Exceptions and Side Effects
Erlang
Simon Thompson University of Kent, Dániel Horpácsi Eötvös Loránd University, Péter Bereczky Eötvös Loránd University
DOI
11:00
30m
Full-paper
Secure Design and Verification of Erlang Systems
Erlang
Viktória Fördős Cisco Systems
DOI
11:30
30m
Full-paper
Clojerl: The Expressive Power of Clojure on the BEAM
Erlang
Juan Facorro , Natalia Chechina Bournemouth University
DOI
10:30 - 12:30
10:30
40m
Talk
Constraint Solvers for the Working PL Researcher
PLMW @ ICFP
Nadia Polikarpova University of California, San Diego
11:10
40m
Talk
Managing your Research, your Advisor, your PhD
PLMW @ ICFP
Amal Ahmed Northeastern University, USA
11:50
40m
Talk
Basic Mechanics of Operational Semantics
PLMW @ ICFP
David Van Horn University of Maryland, USA
12:00 - 14:00
Session 2HOPE at HOPE
12:00
45m
Talk
Higher-order Programming with Effects and Handlers — without First-Class Functions
HOPE
Jonathan Immanuel Brachthäuser University of Tübingen, Germany, Philipp Schuster University of Tübingen, Germany
12:45
45m
Talk
Towards Highly Symmetric Effects and Coeffects and a Systematic Separation between the Extra- and Intra-Logical
HOPE
Ingo Skupin University of Tübingen, Julian Jabs University of Tübingen, David Binder University of Tübingen
File Attached
12:30 - 13:30
Session 3Erlang at Erlang
Chair(s): Annette Bieniusa Technische Universität Kaiserslautern, Viktória Fördős Cisco Systems
12:30
60m
Keynote
Living on the Edge with Erlang
Erlang
Peter Van Roy Université catholique de Louvain
12:30 - 14:00
Session 2TyDe at TyDe
12:30
30m
Talk
Graded Modal Dependent Type Theory (Extended Abstract)
TyDe
Benjamin Moon School of Computing, University of Kent, Harley D. Eades III Augusta University, Dominic Orchard University of Kent, UK
File Attached
13:00
30m
Talk
Frex: indexing modulo equations with free extensions (Extended Abstract)
TyDe
Guillaume Allais University of St Andrews, Edwin Brady University of St. Andrews, UK, Ohad Kammar University of Edinburgh, Jeremy Yallop University of Cambridge
13:30
30m
Talk
Retrofitting Symbolic Holes to LLVM IR (Extended Abstract)
TyDe
Bruce Collie University of Edinburgh, Michael F. P. O'Boyle University of Edinburgh
Pre-print
13:30 - 14:00
Social 2Erlang at Erlang
13:30
30m
Social Event
Social 2
Erlang

13:30 - 14:00
Social SessionPLMW @ ICFP at PLMW
13:30
30m
Social Event
Optional Social Activity
PLMW @ ICFP

14:00 - 15:00
Session 4Erlang at Erlang
14:00
60m
Industry talk
Panel - Erlang fuelled inventions
Erlang

14:00 - 17:30
14:00
3h30m
Tutorial
Best Practices in Code Generation
Tutorials
Michal J. Gajda Migamake Pte Ltd
14:00 - 17:30
Designing Hardware Systems and Accelerators with Open-Source Bluespec HaskellTutorials at Tutorials 2

https://www.youtube.com/watch?v=JCxE3JQAXY0

14:00
3h30m
Tutorial
Designing Hardware Systems and Accelerators with Open-Source Bluespec Haskell
Tutorials
Rishiyur Nikhil Bluespec, Inc.
14:30 - 16:00
Session 3HOPE at HOPE
14:30
45m
Talk
Effectful Improvement Theory
HOPE
Martin Ceresa UNR - CIFASIS - CONICET
15:15
45m
Talk
Alef: A bidirectional effect system for algebraic effects.
HOPE
Antonio Locascio Universidad Nacional de Rosario
15:30 - 17:00
Session 3TyDe at TyDe
15:30
30m
Talk
Predictable Macros for Hindley-Milner (Extended Abstract)
TyDe
16:00
30m
Talk
Strongly Bounded Termination with Applications to Security and Hardware Synthesis
TyDe
Thomas Reynolds University of Missouri, William Harrison Oak Ridge National Laboratory, Rohit Chadha University of Missouri, Gerard Allwein U.S. Naval Research Laboratory
16:30
30m
Talk
Developing a Dependently Typed Language with Runtime Proof Search (Extended Abstract)
TyDe
Mark Lemay Boston University, Cheng Zhang Boston University, William Blair Boston University
16:00 - 17:00
16:00
60m
Talk
Panel discussion: Making a career in PL (even in uncertain times)
PLMW @ ICFP
P: Simon Peyton Jones Microsoft, UK, P: Kathleen Fisher Tufts University, USA, P: Jose Calderon Galois, Inc., P: Benjamin C. Pierce University of Pennsylvania, P: Sarah E. Chasins University of California, Berkeley, P: Jeff Vaughan Google
18:00 - 19:30
TyDe SocialTyDe at TyDe

Join the Zoom via Clowdr

Mon 24 Aug

Displayed time zone: Eastern Time (US & Canada) change

05:00 - 18:00
05:00
60m
Live Q&A
Jane Street 1
ICFP Sponsors

13:30
60m
Live Q&A
Jane Street 3
ICFP Sponsors

09:00 - 18:00
09:00 - 18:00
09:00 - 18:00
09:00 - 10:00
KeynoteICFP Program at ICFP Keynote 1
Chair(s): Chung-chieh Shan Indiana University, USA

Public livestreams: YouTube, iQIYI (China)

09:00
60m
Talk
Referential transparency for pandemic resilience
ICFP Program
09:00 - 18:00
10:00 - 11:30
10:00
90m
Social Event
ICFP Social Time
Social Events

10:00 - 10:30
10:00
30m
Other
Information Desk
Social Events
Stephanie Weirich University of Pennsylvania
10:30 - 11:30
10:30
60m
Meeting
How to Use Clowdr at ICFP
Social Events
Benjamin C. Pierce University of Pennsylvania
10:30 - 11:30
10:30
8m
Poster
A GHC-Plugin to Compile Effectful Languages
Student Research Competition
10:38
8m
Poster
Certified double sided auction mechanisms
Student Research Competition
10:47
8m
Poster
Certified Optimisation of Stream Operations Using Heterogeneous Staging
Student Research Competition
James Lowenthal University of Cambridge
10:55
8m
Poster
Pattern Matching with Typed Holes
Student Research Competition
Yongwei Yuan University of Michigan
11:04
8m
Poster
Type Hole Inference
Student Research Competition
Zhiyi Pan University of Michigan
11:12
8m
Poster
Semantics for a Simple Differentiable Language Using Distribution Theory
Student Research Competition
Christopher Lam Cornell University
11:21
8m
Poster
Gradual Enforcement of IO Trace Properties
Student Research Competition
Cezar-Constantin Andrici Alexandru Ioan Cuza University of Iasi
11:30 - 13:00
New York 1ICFP Program at ICFP NY 1
Chair(s): Adam Chlipala Massachusetts Institute of Technology

Public livestreams: YouTube, Bilibili (China)

11:30
15m
Talk
Stable Relations and Abstract Interpretation of Higher-Order Programs
ICFP Program
Benoît Montagu Inria, Thomas P. Jensen INRIA Rennes
DOI Media Attached File Attached
11:45
15m
Talk
Higher-Order Demand-Driven Symbolic Evaluation
ICFP Program
Zachary Palmer Swarthmore College, Theodore Park Swarthmore and Hopkins, Scott F. Smith The Johns Hopkins University, Shiwei Weng The Johns Hopkins University
DOI Media Attached
12:00
15m
Talk
Sparcl: A Language for Partially-Invertible Computation
ICFP Program
Kazutaka Matsuda Tohoku University, Japan, Meng Wang University of Bristol, UK
DOI Media Attached
12:15
15m
Talk
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
ICFP Program
Nikhil Swamy Microsoft Research, Aseem Rastogi Microsoft Research, Aymeric Fromherz Carnegie Mellon University, Denis Merigoux INRIA, Danel Ahman University of Ljubljana, Guido Martínez CIFASIS-CONICET, Argentina
DOI Media Attached
12:30
15m
Talk
TLC: Temporal Logic of Distributed Components
ICFP Program
Jeremiah Griffin University of California, Riverside, Mohsen Lesani University of California, Riverside, Narges Shadab University of California, Riverside, Xizhe Yin Univsersity of California, Riverside
DOI Media Attached
12:45
15m
Talk
Effect Handlers, Evidently
ICFP Program
Ningning Xie Microsoft Research, USA, Jonathan Immanuel Brachthäuser University of Tübingen, Germany, Daniel Hillerström The University of Edinburgh, Philipp Schuster University of Tübingen, Germany, Daan Leijen Microsoft Research, USA
DOI Media Attached
13:00 - 14:30
13:00
90m
Social Event
ICFP Social Time
Social Events

13:00 - 13:30
13:00
30m
Other
Information Desk
Social Events
Stephanie Weirich University of Pennsylvania
13:30 - 14:30
13:30
60m
Social Event
W@ICFP
Social Events
14:30 - 16:30
New York 2ICFP Program at ICFP NY 2
Chair(s): Alan Jeffrey Mozilla Research

Public livestreams: YouTube, Bilibili (China)

14:30
15m
Talk
Achieving High-Performance the Functional Way - A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies
ICFP Program
Bastian Hagedorn University of Münster, Germany, Johannes Lenfers University of Münster, Thomas Koehler University of Glasgow, United Kingdom, Xueying Qin University of Glasgow, United Kingdom, Sergei Gorlatch University of Münster, Germany, Michel Steuwer The University of Edinburgh
DOI Media Attached
14:45
15m
Talk
Staged Selective Parser Combinators
ICFP Program
Jamie Willis Imperial College London, Nicolas Wu Imperial College London, UK, Matthew Pickering University of Bristol, UK
DOI Media Attached
15:00
15m
Talk
Kindly Bent to Free Us
ICFP Program
Gabriel Radanne Inria, Hannes Saffrich University of Freiburg, Peter Thiemann University of Freiburg, Germany
DOI Pre-print Media Attached File Attached
15:15
15m
Talk
Sealing Pointer-Based Optimizations Behind Pure Functions
ICFP Program
Daniel Selsam Microsoft Research, Simon Hudon Carnegie Mellon University, Leonardo de Moura Microsoft Research, n.n.
DOI Media Attached
15:30
15m
Talk
Effects for Efficiency: Asymptotic Speedup with First-Class Control
ICFP Program
Daniel Hillerström The University of Edinburgh, Sam Lindley Heriot-Watt University, UK / The University of Edinburgh, UK, John Longley The University of Edinburgh
DOI Media Attached
15:45
15m
Talk
Computation Focusing
ICFP Program
Nick Rioux University of Pennsylvania, Steve Zdancewic University of Pennsylvania
DOI Media Attached
16:00
15m
Talk
Retrofitting Parallelism onto OCamlDistinguished Paper
ICFP Program
KC Sivaramakrishnan IIT Madras, Stephen Dolan University of Cambridge, UK, Leo White Jane Street, Sadiq Jaffer Opsian and OCaml Labs, Tom Kelly OCaml Labs, Anmol Sahoo IIT Madras, Sudha Parimala IIT Madras, Atul Dhiman IIT Madras, Anil Madhavapeddy OCaml Labs
DOI Media Attached
16:15
15m
Talk
Liquid Information Flow ControlDistinguished Paper
ICFP Program
Nadia Polikarpova University of California, San Diego, Deian Stefan University of California at San Diego, USA, Jean Yang Carnegie Mellon University, Shachar Itzhaky Technion, Israel, Travis Hance Carnegie Mellon University, Armando Solar-Lezama Massachusetts Institute of Technology, USA
DOI Media Attached
14:45 - 16:45
ICFP Q&A New York 2-2ICFP Q&A at ICFP Q&A 2
15:00
30m
Live Q&A
Staged Selective Parser Combinators
ICFP Q&A

15:30
30m
Live Q&A
Sealing Pointer-Based Optimizations Behind Pure Functions
ICFP Q&A

16:00
30m
Live Q&A
Computation Focusing
ICFP Q&A

16:30
30m
Live Q&A
Liquid Information Flow Control
ICFP Q&A

16:30 - 17:30
16:30
60m
Social Event
ICFP Social Time
Social Events

16:30 - 17:30
Untitled PL Card GameSocial Events at ICFP Social 2
16:30
60m
Social Event
Untitled PL Card Game
Social Events
Jasper Van der Jeugt Fugue, Niki Vazou IMDEA Software Institute, Leonidas Lampropoulos University of Maryland, College Park
Media Attached
21:00 - 22:00
21:00
60m
Social Event
ICFP Social Time
Social Events

21:00 - 22:00
Women in CS PanelSocial Events at ICFP Social
Chair(s): Cristina Cifuentes Oracle Labs

YouTube recording of event: https://youtu.be/uHdtXFEwVCs

21:00
60m
Social Event
Women in CS Panel
Social Events
P: Cristina Cifuentes Oracle Labs, P: Sukyoung Ryu KAIST, P: Alena Griffiths RGB Assurance, P: Behnaz Hassanshahi Oracle Labs, Australia
22:00 - 23:00
22:00
60m
Meeting
How to Use Clowdr at ICFP
Social Events
Benjamin C. Pierce University of Pennsylvania
22:30 - 00:00
Asia 1ICFP Program at ICFP Asia 1
Chair(s): Adam Chlipala Massachusetts Institute of Technology

Public livestreams: YouTube, Bilibili (China)

22:30
15m
Talk
Stable Relations and Abstract Interpretation of Higher-Order Programs
ICFP Program
Benoît Montagu Inria, Thomas P. Jensen INRIA Rennes
DOI Media Attached File Attached
22:45
15m
Talk
Higher-Order Demand-Driven Symbolic Evaluation
ICFP Program
Zachary Palmer Swarthmore College, Theodore Park Swarthmore and Hopkins, Scott F. Smith The Johns Hopkins University, Shiwei Weng The Johns Hopkins University
DOI Media Attached
23:00
15m
Talk
Sparcl: A Language for Partially-Invertible Computation
ICFP Program
Kazutaka Matsuda Tohoku University, Japan, Meng Wang University of Bristol, UK
DOI Media Attached
23:15
15m
Talk
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
ICFP Program
Nikhil Swamy Microsoft Research, Aseem Rastogi Microsoft Research, Aymeric Fromherz Carnegie Mellon University, Denis Merigoux INRIA, Danel Ahman University of Ljubljana, Guido Martínez CIFASIS-CONICET, Argentina
DOI Media Attached
23:30
15m
Talk
TLC: Temporal Logic of Distributed Components
ICFP Program
Jeremiah Griffin University of California, Riverside, Mohsen Lesani University of California, Riverside, Narges Shadab University of California, Riverside, Xizhe Yin Univsersity of California, Riverside
DOI Media Attached
23:45
15m
Talk
Effect Handlers, Evidently
ICFP Program
Ningning Xie Microsoft Research, USA, Jonathan Immanuel Brachthäuser University of Tübingen, Germany, Daniel Hillerström The University of Edinburgh, Philipp Schuster University of Tübingen, Germany, Daan Leijen Microsoft Research, USA
DOI Media Attached
22:45 - 00:15
ICFP Q&A Asia 1-1ICFP Q&A at ICFP Q&A 1
23:15
30m
Live Q&A
Sparcl: A Language for Partially-Invertible Computation
ICFP Q&A

23:45
30m
Live Q&A
TLC: Temporal Logic of Distributed Components
ICFP Q&A

Tue 25 Aug

Displayed time zone: Eastern Time (US & Canada) change

01:00 - 02:00
01:00
60m
Social Event
ICFP Social Time
Social Events

01:00 - 02:00
01:00
60m
Talk
Mentoring with Ranjit Jhala
Social Events
Ranjit Jhala University of California at San Diego, USA
02:30 - 04:30
Asia 2ICFP Program at ICFP Asia 2
Chair(s): Alan Jeffrey Mozilla Research

Public livestreams: YouTube, Bilibili (China)

02:30
15m
Talk
Achieving High-Performance the Functional Way - A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies
ICFP Program
Bastian Hagedorn University of Münster, Germany, Johannes Lenfers University of Münster, Thomas Koehler University of Glasgow, United Kingdom, Xueying Qin University of Glasgow, United Kingdom, Sergei Gorlatch University of Münster, Germany, Michel Steuwer The University of Edinburgh
DOI Media Attached
02:45
15m
Talk
Staged Selective Parser Combinators
ICFP Program
Jamie Willis Imperial College London, Nicolas Wu Imperial College London, UK, Matthew Pickering University of Bristol, UK
DOI Media Attached
03:00
15m
Talk
Kindly Bent to Free Us
ICFP Program
Gabriel Radanne Inria, Hannes Saffrich University of Freiburg, Peter Thiemann University of Freiburg, Germany
DOI Pre-print Media Attached File Attached
03:15
15m
Talk
Sealing Pointer-Based Optimizations Behind Pure Functions
ICFP Program
Daniel Selsam Microsoft Research, Simon Hudon Carnegie Mellon University, Leonardo de Moura Microsoft Research, n.n.
DOI Media Attached
03:30
15m
Talk
Effects for Efficiency: Asymptotic Speedup with First-Class Control
ICFP Program
Daniel Hillerström The University of Edinburgh, Sam Lindley Heriot-Watt University, UK / The University of Edinburgh, UK, John Longley The University of Edinburgh
DOI Media Attached
03:45
15m
Talk
Computation Focusing
ICFP Program
Nick Rioux University of Pennsylvania, Steve Zdancewic University of Pennsylvania
DOI Media Attached
04:00
15m
Talk
Retrofitting Parallelism onto OCamlDistinguished Paper
ICFP Program
KC Sivaramakrishnan IIT Madras, Stephen Dolan University of Cambridge, UK, Leo White Jane Street, Sadiq Jaffer Opsian and OCaml Labs, Tom Kelly OCaml Labs, Anmol Sahoo IIT Madras, Sudha Parimala IIT Madras, Atul Dhiman IIT Madras, Anil Madhavapeddy OCaml Labs
DOI Media Attached
04:15
15m
Talk
Liquid Information Flow ControlDistinguished Paper
ICFP Program
Nadia Polikarpova University of California, San Diego, Deian Stefan University of California at San Diego, USA, Jean Yang Carnegie Mellon University, Shachar Itzhaky Technion, Israel, Travis Hance Carnegie Mellon University, Armando Solar-Lezama Massachusetts Institute of Technology, USA
DOI Media Attached
02:45 - 04:45
ICFP Q&A Asia 2-2ICFP Q&A at ICFP Q&A 2
04:30 - 05:30
04:30
60m
Social Event
ICFP Social Time
Social Events

04:30 - 05:30
04:30
60m
Meeting
Online Lecture Panel
Social Events
Atsushi Igarashi Kyoto University, Japan, Sukyoung Ryu KAIST, Ilya Sergey Yale-NUS College and National University of Singapore, Alex Potanin Victoria University of Wellington
05:00 - 18:00
05:00
60m
Live Q&A
Jane Street 1
ICFP Sponsors

10:00
60m
Live Q&A
Jane Street 2
ICFP Sponsors

13:30
60m
Live Q&A
Jane Street 3
ICFP Sponsors

09:00 - 18:00
09:00 - 18:00
09:00 - 18:00
09:00 - 10:00
KeynoteICFP Program at ICFP Keynote 2
Chair(s): Adam Chlipala Massachusetts Institute of Technology

Public livestreams: YouTube, iQIYI (China)

09:00
60m
Talk
On Language Adoption
ICFP Program
09:00 - 18:00
10:00 - 10:30
10:00
30m
Other
Information Desk
Social Events
Stephanie Weirich University of Pennsylvania
10:30 - 11:30
10:30
60m
Social Event
Virtual Art Gallery
Social Events
Alan Jeffrey Mozilla Research
10:30 - 11:30
10:30
30m
Meeting
SIGPLAN CARES
Social Events
David Walker Princeton University, USA, Simon Peyton Jones Microsoft, UK, Alexandra Silva University College London, Shriram Krishnamurthi Brown University, United States
11:30 - 13:00
New York 3 (JFP talks)ICFP Program at ICFP NY 3
Chair(s): Jeremy Gibbons Department of Computer Science, University of Oxford

Public livestreams: YouTube, Bilibili (China)

11:30
11m
Talk
A theory of RPC calculi for client–server modelJFP
ICFP Program
DOI Media Attached
11:41
11m
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 Perez IMDEA Software Institute, Pablo Nogueira ESNE University School of Design, Innovation and Technology
DOI Media Attached
11:52
11m
Talk
Local algebraic effect theoriesJFP
ICFP Program
Žiga Lukšič , Matija Pretnar University of Ljubljana, Slovenia
DOI Media Attached
12:03
11m
Talk
Heterogeneous binary random-access listsJFP
ICFP Program
Wouter Swierstra Utrecht University, Netherlands
DOI Media Attached
12:15
11m
Talk
POPLMark reloaded: Mechanizing proofs by logical relationsJFP
ICFP Program
Andreas Abel Gothenburg University, Guillaume Allais University of St Andrews, Aliya Hameer McGill University, Brigitte Pientka McGill University, Alberto Momigliano Università degli Studi di Milano, Steven Schäfer Google, Aarhus, Kathrin Stark Princeton University, USA
DOI Media Attached
12:26
11m
Talk
Perturbation confusion in forward automatic differentiation of higher-order functionsJFP
ICFP Program
Oleksandr Manzyuk , Barak A. Pearlmutter Maynooth University, Alexey Radul , David Rush , Jeffrey Mark Siskind School of Electrical and Computer Engineering, Purdue University
DOI Media Attached
12:37
11m
Talk
Elastic Sheet-Defined Functions: Generalising Spreadsheet Functions to Variable-Size Input ArraysJFP
ICFP Program
Matt McCutchen , Judith Borghouts , Andrew D. Gordon Microsoft Research and University of Edinburgh, Simon Peyton Jones Microsoft, UK, Advait Sarkar Microsoft Research and University of Cambridge
DOI Pre-print Media Attached
12:48
11m
Talk
Emerging languages: An alternative approach to teaching programming languagesJFP
ICFP Program
Saverio Perugini University of Dayton
DOI Media Attached
11:30 - 12:15
11:30
45m
Talk
SRC Finalist Presentation 1
Student Research Competition

13:00 - 14:30
13:00
90m
Social Event
ICFP Social Time
Social Events

13:00 - 13:30
13:00
30m
Other
Information Desk
Social Events
Stephanie Weirich University of Pennsylvania
13:30 - 14:30
LGBTQ MeetupSocial Events at ICFP Social
13:30
60m
Talk
LGBTQ Meetup
Social Events
David Walker Princeton University, USA, Matthew Weaver Princeton University
14:30 - 16:30
New York 4ICFP Program at ICFP NY 4
Chair(s): Stephanie Weirich University of Pennsylvania

Public livestreams: YouTube, Bilibili (China)

14:30
15m
Talk
The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy (Functional Pearl)
ICFP Program
DOI Pre-print Media Attached
14:45
15m
Talk
Liquid Resource Types
ICFP Program
Tristan Knoth University of California at San Diego, USA, Di Wang Carnegie Mellon University, Adam Reynolds University of California, San Diego, Nadia Polikarpova University of California, San Diego, Jan Hoffmann Carnegie Mellon University
DOI Media Attached
15:00
15m
Talk
Cosmo: A Concurrent Separation Logic for Multicore OCaml
ICFP Program
Glen Mével Inria, Université Paris-Saclay, CNRS, Laboratoire de recherche en informatique, Jacques-Henri Jourdan Universersité Paris Saclay, CNRS, LRI, François Pottier Inria, France
DOI Media Attached
15:15
15m
Talk
Composing and Decomposing Op-Based CRDTs with Semidirect Products
ICFP Program
Matthew Weidner Carnegie Mellon University, Christopher Meiklejohn Carnegie Mellon University, Heather Miller Carnegie Mellon University
DOI Media Attached
15:30
15m
Talk
A Quick Look at ImpredicativityDistinguished Paper
ICFP Program
Alejandro Serrano 47 Degrees, Spain, Jurriaan Hage Utrecht University, Netherlands, Simon Peyton Jones Microsoft, UK, Dimitrios Vytiniotis DeepMind
DOI Pre-print Media Attached
15:45
15m
Talk
A Unified View of Modalities in Type Systems
ICFP Program
Andreas Abel Gothenburg University, Jean-Philippe Bernardy University of Gothenburg, Sweden
DOI Media Attached
16:00
15m
Talk
Lower Your Guards: A Compositional Pattern-Match Coverage Checker
ICFP Program
Sebastian Graf Karlsruhe Institute of Technology, Simon Peyton Jones Microsoft, UK, Ryan Scott Galois, Inc.
Link to publication DOI Media Attached
16:15
15m
Talk
Signature restriction for polymorphic algebraic effects
ICFP Program
Taro Sekiyama National Institute of Informatics, Takeshi Tsukada Chiba University, Japan, Atsushi Igarashi Kyoto University, Japan
DOI Media Attached
14:45 - 16:45
ICFP Q&A New York 4-2ICFP Q&A at ICFP Q&A 2
15:00
30m
Live Q&A
Liquid Resource Types
ICFP Q&A

15:30
30m
Live Q&A
Composing and Decomposing Op-Based CRDTs with Semidirect Products
ICFP Q&A

16:00
30m
Live Q&A
A Unified View of Modalities in Type Systems
ICFP Q&A

16:30 - 17:30
16:30
60m
Social Event
ICFP Social Time
Social Events

16:30 - 17:30
16:30
60m
Social Event
ICFP Triva
Social Events
Jose Calderon Galois, Inc., Paulette Koronkevich University of British Columbia
21:00 - 22:30
21:00
90m
Social Event
ICFP Social Time
Social Events

21:00 - 22:00
21:00
30m
Meeting
SIGPLAN CARES
Social Events
David Walker Princeton University, USA, Simon Peyton Jones Microsoft, UK, Alexandra Silva University College London, Shriram Krishnamurthi Brown University, United States
21:30 - 22:30
Mind the TitleSocial Events at ICFP Social 3
21:30
60m
Meeting
Mind the Title
Social Events
Olivier Danvy Yale-NUS College and School of Computing, Singapore
22:30 - 00:00
Asia 3 (JFP talks)ICFP Program at ICFP Asia 3
Chair(s): Jeremy Gibbons Department of Computer Science, University of Oxford

Public livestreams: YouTube, Bilibili (China)

22:30
11m
Talk
A theory of RPC calculi for client–server modelJFP
ICFP Program
DOI Media Attached
22:41
11m
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 Perez IMDEA Software Institute, Pablo Nogueira ESNE University School of Design, Innovation and Technology
DOI Media Attached
22:52
11m
Talk
Local algebraic effect theoriesJFP
ICFP Program
Žiga Lukšič , Matija Pretnar University of Ljubljana, Slovenia
DOI Media Attached
23:03
11m
Talk
Heterogeneous binary random-access listsJFP
ICFP Program
Wouter Swierstra Utrecht University, Netherlands
DOI Media Attached
23:15
11m
Talk
POPLMark reloaded: Mechanizing proofs by logical relationsJFP
ICFP Program
Andreas Abel Gothenburg University, Guillaume Allais University of St Andrews, Aliya Hameer McGill University, Brigitte Pientka McGill University, Alberto Momigliano Università degli Studi di Milano, Steven Schäfer Google, Aarhus, Kathrin Stark Princeton University, USA
DOI Media Attached
23:26
11m
Talk
Perturbation confusion in forward automatic differentiation of higher-order functionsJFP
ICFP Program
Oleksandr Manzyuk , Barak A. Pearlmutter Maynooth University, Alexey Radul , David Rush , Jeffrey Mark Siskind School of Electrical and Computer Engineering, Purdue University
DOI Media Attached
23:37
11m
Talk
Elastic Sheet-Defined Functions: Generalising Spreadsheet Functions to Variable-Size Input ArraysJFP
ICFP Program
Matt McCutchen , Judith Borghouts , Andrew D. Gordon Microsoft Research and University of Edinburgh, Simon Peyton Jones Microsoft, UK, Advait Sarkar Microsoft Research and University of Cambridge
DOI Pre-print Media Attached
23:48
11m
Talk
Emerging languages: An alternative approach to teaching programming languagesJFP
ICFP Program
Saverio Perugini University of Dayton
DOI Media Attached
22:40 - 00:10
ICFP Q&A Asia 3-1ICFP Q&A at ICFP Q&A 1
22:40 - 00:10
ICFP Q&A Asia 3-2ICFP Q&A at ICFP Q&A 2
23:30 - 00:15
23:30
45m
Talk
SRC Finalist Presentation 2
Student Research Competition

Wed 26 Aug

Displayed time zone: Eastern Time (US & Canada) change

00:00 - 01:00
00:00
60m
Social Event
ICFP Social Time
Social Events

00:00 - 01:00
00:00
60m
Talk
Mentoring with Guy Steele
Social Events
Guy L. Steele Jr. Oracle Labs
02:30 - 04:30
Asia 4ICFP Program at ICFP Asia 4
Chair(s): Stephanie Weirich University of Pennsylvania

Public livestreams: YouTube, Bilibili (China)

02:30
15m
Talk
The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy (Functional Pearl)
ICFP Program
DOI Pre-print Media Attached
02:45
15m
Talk
Liquid Resource Types
ICFP Program
Tristan Knoth University of California at San Diego, USA, Di Wang Carnegie Mellon University, Adam Reynolds University of California, San Diego, Nadia Polikarpova University of California, San Diego, Jan Hoffmann Carnegie Mellon University
DOI Media Attached
03:00
15m
Talk
Cosmo: A Concurrent Separation Logic for Multicore OCaml
ICFP Program
Glen Mével Inria, Université Paris-Saclay, CNRS, Laboratoire de recherche en informatique, Jacques-Henri Jourdan Universersité Paris Saclay, CNRS, LRI, François Pottier Inria, France
DOI Media Attached
03:15
15m
Talk
Composing and Decomposing Op-Based CRDTs with Semidirect Products
ICFP Program
Matthew Weidner Carnegie Mellon University, Christopher Meiklejohn Carnegie Mellon University, Heather Miller Carnegie Mellon University
DOI Media Attached
03:30
15m
Talk
A Quick Look at ImpredicativityDistinguished Paper
ICFP Program
Alejandro Serrano 47 Degrees, Spain, Jurriaan Hage Utrecht University, Netherlands, Simon Peyton Jones Microsoft, UK, Dimitrios Vytiniotis DeepMind
DOI Pre-print Media Attached
03:45
15m
Talk
A Unified View of Modalities in Type Systems
ICFP Program
Andreas Abel Gothenburg University, Jean-Philippe Bernardy University of Gothenburg, Sweden
DOI Media Attached
04:00
15m
Talk
Lower Your Guards: A Compositional Pattern-Match Coverage Checker
ICFP Program
Sebastian Graf Karlsruhe Institute of Technology, Simon Peyton Jones Microsoft, UK, Ryan Scott Galois, Inc.
Link to publication DOI Media Attached
04:15
15m
Talk
Signature restriction for polymorphic algebraic effects
ICFP Program
Taro Sekiyama National Institute of Informatics, Takeshi Tsukada Chiba University, Japan, Atsushi Igarashi Kyoto University, Japan
DOI Media Attached
02:45 - 04:45
ICFP Q&A Asia 4-2ICFP Q&A at ICFP Q&A 2
04:00
30m
Live Q&A
A Unified View of Modalities in Type Systems
ICFP Q&A

04:30
30m
Live Q&A
Signature restriction for polymorphic algebraic effects
ICFP Q&A

04:30 - 05:30
04:30
60m
Social Event
ICFP Social Time
Social Events

04:30 - 05:30
04:30
60m
Talk
Some Proverbs in Type Theory
Social Events
Neel Krishnaswami Computer Laboratory, University of Cambridge
05:00 - 18:00
05:00
60m
Live Q&A
Jane Street 1
ICFP Sponsors

10:00
60m
Live Q&A
Jane Street 2
ICFP Sponsors

13:30
60m
Live Q&A
Jane Street 3
ICFP Sponsors

16:30
60m
Social Event
Jane Street at Industrial Reception
ICFP Sponsors

09:00 - 18:00
16:30
60m
Social Event
Ahrefs at Industrial Reception
ICFP Sponsors

09:00 - 18:00
16:30
60m
Social Event
Facebook at Industrial Reception
ICFP Sponsors

09:00 - 18:00
16:30
60m
Social Event
Galois at Industrial Reception
ICFP Sponsors

09:00 - 09:45
ICFP Programming ContestICFP Program at ICFP Awards
Chair(s): Stephanie Weirich University of Pennsylvania

Public livestreams: YouTube, iQIYI (China)

09:00
45m
Keynote
Programming Contest Report
ICFP Program
09:00 - 18:00
16:30
60m
Social Event
Standard Chartered at Industrial Reception
ICFP Sponsors

09:45 - 10:30
Awards & ReportsICFP Program at ICFP Awards
Chair(s): Stephanie Weirich University of Pennsylvania

Public livestreams: YouTube, iQIYI (China)

09:45
45m
Talk
Award Presentations & Chair Report
ICFP Program
Stephanie Weirich University of Pennsylvania, Adam Chlipala Massachusetts Institute of Technology, Mira Mezini Technische Universität Darmstadt, Sukyoung Ryu KAIST, Jens Palsberg University of California, Los Angeles, Youyou Cong Tokyo Institute of Technology
10:30 - 11:00
10:30
30m
Other
Information Desk
Social Events
Stephanie Weirich University of Pennsylvania
11:00 - 13:00
New York 5ICFP Program at ICFP NY 5
Chair(s): Richard A. Eisenberg Tweag I/O

Public livestreams: YouTube, Bilibili (China)

11:00
15m
Talk
Denotational Recurrence Extraction for Amortized Analysis
ICFP Program
Joseph W. Cutler Wesleyan University, Dan Licata Wesleyan University, Norman Danner Wesleyan University
DOI Media Attached
11:15
15m
Talk
Separation Logic for Sequential Programs (Functional Pearl)
ICFP Program
DOI Media Attached
11:30
15m
Talk
Strong Functional Pearl: Harper's Regular-Expression Matcher in Cedille
ICFP Program
Aaron Stump The University of Iowa, USA, Chris Jenkins The University of Iowa, Stephan Spahn The University of Iowa, Colin McDonald University of Notre Dame
DOI Media Attached
11:45
15m
Talk
Duplo: A Framework for OCaml Post-Link Optimisation
ICFP Program
Nandor Licker University of Cambridge, Timothy M. Jones University of Cambridge, UK
DOI Media Attached
12:00
15m
Talk
Recovering Purity with Comonads and Capabilities
ICFP Program
Vikraman Choudhury Indiana University & University of Cambridge, Neel Krishnaswami Computer Laboratory, University of Cambridge
DOI Media Attached
12:15
15m
Talk
A General Approach to Define Binders Using Matching Logic
ICFP Program
Xiaohong Chen University of Illinois at Urbana-Champaign, Grigore Roşu University of Illinois at Urbana-Champaign
DOI Media Attached
12:30
15m
Talk
Parsing with Zippers (Functional Pearl)
ICFP Program
Pierce Darragh University of Utah, Michael D. Adams University of Michigan
DOI Media Attached
12:45
15m
Talk
Regular Language Type Inference with Term Rewriting
ICFP Program
Timothée Haudebourg Univ Rennes, Inria, CNRS, IRISA, Thomas Genet IRISA, Univ Rennes, Thomas P. Jensen INRIA Rennes
DOI Media Attached
13:00 - 14:30
13:00
90m
Social Event
ICFP Social Time
Social Events

13:00 - 13:30
13:00
30m
Other
Information Desk
Social Events
Stephanie Weirich University of Pennsylvania
13:30 - 14:30
Virtualization Feedback 1Social Events at ICFP Social 2
13:30
60m
Meeting
Virtualization Feedback
Social Events
Benjamin C. Pierce University of Pennsylvania, Jonathan Bell Northeastern University, Crista Lopes University of California, Irvine
14:30 - 16:25
New York 6ICFP Program at ICFP NY 6
Chair(s): Sukyoung Ryu KAIST

Public livestreams: YouTube, Bilibili (China)

14:30
15m
Talk
Compiling Effect Handlers in Capability-Passing Style
ICFP Program
Philipp Schuster University of Tübingen, Germany, Jonathan Immanuel Brachthäuser University of Tübingen, Germany, Klaus Ostermann University of Tübingen, Germany
DOI Media Attached
14:45
15m
Talk
Scala Step-by-Step — Soundness for DOT with Step-Indexed Logical Relations in Iris
ICFP Program
Paolo G. Giarrusso BedRock Systems, Leo Stefanesco IRIF, University Paris Diderot & CNRS, Amin Timany Aarhus University, Lars Birkedal Aarhus University, Robbert Krebbers Delft University of Technology
DOI Media Attached
15:00
15m
Talk
A dependently typed calculus with pattern matching and erasure inferenceDistinguished Paper
ICFP Program
Matúš Tejiščák University of St Andrews
DOI Media Attached
15:15
15m
Talk
Raising Expectations: Automating Expected Cost Analysis with Types
ICFP Program
Di Wang Carnegie Mellon University, David M. Kahn Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University
DOI Media Attached
15:30
15m
Talk
Program Sketching with Live Bidirectional Evaluation
ICFP Program
Justin Lubin University of Chicago, Nick Collins University of Chicago, Cyrus Omar University of Michigan, Ravi Chugh University of Chicago
DOI Media Attached
15:45
15m
Talk
Elaboration with First-Class Implicit Function Types
ICFP Program
András Kovács Eötvös Loránd University
DOI Pre-print Media Attached
16:00
15m
Talk
Kinds are Calling Conventions
ICFP Program
Paul Downen University of Oregon, USA, Zena M. Ariola University of Oregon, USA, Simon Peyton Jones Microsoft, UK, Richard A. Eisenberg Tweag I/O
DOI Media Attached
16:15
10m
Day closing
Conference closing
ICFP Program
Stephanie Weirich University of Pennsylvania
16:30 - 17:30
Industrial ReceptionSocial Events at ICFP Social
16:30
60m
Social Event
Industrial Reception
Social Events

16:30 - 17:30
16:30
60m
Social Event
Tweag at Industrial Reception
ICFP Sponsors

16:30 - 17:30
16:30
60m
Social Event
Bloomberg at Industrial Reception
ICFP Sponsors

16:30 - 17:30
16:30
60m
Social Event
Microsoft at Industrial Reception
ICFP Sponsors

16:30 - 17:30
16:30
60m
Social Event
Oracle at Industrial Reception
ICFP Sponsors

21:00 - 22:00
21:00
60m
Social Event
ICFP Social Time
Social Events

21:00 - 22:00
Virtualization Feedback 2Social Events at ICFP Social 2
21:00
60m
Meeting
Virtualization Feedback
Social Events
Benjamin C. Pierce University of Pennsylvania, Jonathan Bell Northeastern University, Crista Lopes University of California, Irvine
22:30 - 00:00
Asia 5ICFP Program at ICFP Asia 5
Chair(s): Richard A. Eisenberg Tweag I/O

Public livestreams: YouTube, Bilibili (China)

22:00
30m
Talk
Denotational Recurrence Extraction for Amortized Analysis
ICFP Program
Joseph W. Cutler Wesleyan University, Dan Licata Wesleyan University, Norman Danner Wesleyan University
DOI Media Attached
22:15
15m
Talk
Separation Logic for Sequential Programs (Functional Pearl)
ICFP Program
DOI Media Attached
22:30
15m
Talk
Strong Functional Pearl: Harper's Regular-Expression Matcher in Cedille
ICFP Program
Aaron Stump The University of Iowa, USA, Chris Jenkins The University of Iowa, Stephan Spahn The University of Iowa, Colin McDonald University of Notre Dame
DOI Media Attached
22:45
15m
Talk
Duplo: A Framework for OCaml Post-Link Optimisation
ICFP Program
Nandor Licker University of Cambridge, Timothy M. Jones University of Cambridge, UK
DOI Media Attached
23:00
15m
Talk
Recovering Purity with Comonads and Capabilities
ICFP Program
Vikraman Choudhury Indiana University & University of Cambridge, Neel Krishnaswami Computer Laboratory, University of Cambridge
DOI Media Attached
23:15
15m
Talk
A General Approach to Define Binders Using Matching Logic
ICFP Program
Xiaohong Chen University of Illinois at Urbana-Champaign, Grigore Roşu University of Illinois at Urbana-Champaign
DOI Media Attached
23:30
15m
Talk
Parsing with Zippers (Functional Pearl)
ICFP Program
Pierce Darragh University of Utah, Michael D. Adams University of Michigan
DOI Media Attached
23:45
15m
Talk
Regular Language Type Inference with Term Rewriting
ICFP Program
Timothée Haudebourg Univ Rennes, Inria, CNRS, IRISA, Thomas Genet IRISA, Univ Rennes, Thomas P. Jensen INRIA Rennes
DOI Media Attached
22:45 - 00:15
ICFP Q&A Asia 5-2ICFP Q&A at ICFP Q&A 2
23:30
30m
Live Q&A
A General Approach to Define Binders Using Matching Logic
ICFP Q&A

Thu 27 Aug

Displayed time zone: Eastern Time (US & Canada) change

00:30 - 01:30
00:30
60m
Social Event
ICFP Social Time
Social Events

00:30 - 01:30
00:30
60m
Talk
Mentoring with Matthias Felleisen
Social Events
Matthias Felleisen PLT @ Northeastern University
02:30 - 04:25
Asia 6ICFP Program at ICFP Asia 6
Chair(s): Sukyoung Ryu KAIST

Public livestreams: YouTube, Bilibili (China)

02:30
15m
Talk
Compiling Effect Handlers in Capability-Passing Style
ICFP Program
Philipp Schuster University of Tübingen, Germany, Jonathan Immanuel Brachthäuser University of Tübingen, Germany, Klaus Ostermann University of Tübingen, Germany
DOI Media Attached
02:45
15m
Talk
Scala Step-by-Step — Soundness for DOT with Step-Indexed Logical Relations in Iris
ICFP Program
Paolo G. Giarrusso BedRock Systems, Leo Stefanesco IRIF, University Paris Diderot & CNRS, Amin Timany Aarhus University, Lars Birkedal Aarhus University, Robbert Krebbers Delft University of Technology
DOI Media Attached
03:00
15m
Talk
A dependently typed calculus with pattern matching and erasure inferenceDistinguished Paper
ICFP Program
Matúš Tejiščák University of St Andrews
DOI Media Attached
03:15
15m
Talk
Raising Expectations: Automating Expected Cost Analysis with Types
ICFP Program
Di Wang Carnegie Mellon University, David M. Kahn Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University
DOI Media Attached
03:30
15m
Talk
Program Sketching with Live Bidirectional Evaluation
ICFP Program
Justin Lubin University of Chicago, Nick Collins University of Chicago, Cyrus Omar University of Michigan, Ravi Chugh University of Chicago
DOI Media Attached
03:45
15m
Talk
Elaboration with First-Class Implicit Function Types
ICFP Program
András Kovács Eötvös Loránd University
DOI Pre-print Media Attached
04:00
15m
Talk
Kinds are Calling Conventions
ICFP Program
Paul Downen University of Oregon, USA, Zena M. Ariola University of Oregon, USA, Simon Peyton Jones Microsoft, UK, Richard A. Eisenberg Tweag I/O
DOI Media Attached
04:15
10m
Day closing
Conference closing
ICFP Program
Stephanie Weirich University of Pennsylvania
04:30 - 05:30
04:30
60m
Social Event
ICFP Social Time
Social Events

09:00 - 10:00
Designated Social Interaction TimeHaskell at Haskell
09:00 - 10:00
Career PlanningSocial Events at ICFP Social
09:00
60m
Meeting
Academic Career Planning During a Crisis
Social Events
Neel Krishnaswami Computer Laboratory, University of Cambridge
09:00 - 12:30
09:00
3h30m
Tutorial
Functional Software Architecture
Tutorials
Michael Sperber Active Group GmbH
09:00 - 12:30
Integrating User Centered Methods into Programming Language DesignTutorials at Tutorials 2

https://www.youtube.com/watch?v=-m34gNVVpFQ

09:00
3h30m
Tutorial
Integrating User-Centered Methods into Programming Language Design
Tutorials
Michael Coblenz Carnegie Mellon University, Jonathan Aldrich Carnegie Mellon University
09:00 - 11:00
Morning KeynoteminiKanren at miniKanren
Chair(s): Dmitri Boulytchev St. Petersburg State University, St. Petersburg, Russia
10:00
60m
Keynote
Executing Declarative Language Definitions
miniKanren
K: Eelco Visser Delft University of Technology
11:30 - 13:00
Paper Session 1 - Software EngineeringHaskell at Haskell
Chair(s): José Pedro Magalhães
11:30
30m
Talk
Assessing the Quality of Evolving Haskell Systems by Measuring Structural Inequality
Haskell
Sander Kamps Open University of the Netherlands, Netherlands, Bastiaan Heeren Open University of the Netherlands, Netherlands, Johan Jeuring Open University of the Netherlands, Netherlands
DOI
12:00
30m
Talk
Describing Microservices using Modern Haskell (Experience Report)
Haskell
Alejandro Serrano 47 Degrees, Spain, Flavio Corpa 47 Degrees, Spain
DOI
12:30
30m
Talk
Towards Secure IoT Programming in Haskell
Haskell
Nachiappan Valliappan Chalmers University of Technology, Sweden, Robert Krook Chalmers University of Technology, Sweden, Alejandro Russo Chalmers University of Technology, Sweden, Koen Claessen Chalmers University of Technology, Sweden
DOI
11:30 - 13:30
Morning SessionminiKanren at miniKanren
Chair(s): Joseph P. Near University of Vermont, Gregory Rosenblatt University of Alabama at Birmingham, USA
11:30
20m
Talk
On Fair Relational Conjunction
miniKanren
Petr Lozov Sain Petersburg State University, SPbGU, Dmitri Boulytchev St. Petersburg State University, St. Petersburg, Russia
Link to publication
11:50
20m
Talk
An Empirical Study of Partial Deduction for miniKanren
miniKanren
Ekaterina Verbitskaia JetBrains, Daniil Berezun JetBrains, Russia, Dmitri Boulytchev St. Petersburg State University, St. Petersburg, Russia
Link to publication
12:10
20m
Talk
MicroKanren in J: an Embedding of the Relational Paradigm in an Array Language with Rank-Polymorphic Unification
miniKanren
Raoul Schorer Geneva University Hospitals
Link to publication
12:30
20m
Talk
λKanren: Higher-order Logic Programming with Shallow Embedding
miniKanren
Weixi Ma Indiana University, Kuang-Chen Lu Indiana University Bloomington, Daniel P. Friedman Indiana University, USA
Link to publication
12:50
20m
Talk
Kanren Light: A Dynamically Semi-Certified Interactive Logic Programming System
miniKanren
Marco Maggesi Università di Firenze, Massimo Nocentini Università di Firenze
Link to publication
13:10
20m
Talk
Certified Semantics for Disequality
miniKanren
Dmitry Rozplokhas Higher School of Economics, Dmitri Boulytchev St. Petersburg State University, St. Petersburg, Russia
Link to publication
14:00 - 18:00
ShutdownPL 1Social Events at ICFP Social
14:00
4h
Social Event
ShutdownPL: Keynote and Getting Started With Anti-racist Action
Social Events
Kenny Foner Galois, Niki Carroll George Mason University, Priya Srikumar Cornell University, David Justo University of California, San Diego, Justin Lubin University of Chicago, Akash Gaonkar , Alan Jeffrey Mozilla Research
14:00 - 17:30
Using the K Framework to Formalize Functional LanguagesTutorials at Tutorials 1

https://www.youtube.com/watch?v=VlQMi_N42B8&feature=youtu.be

14:00
3h30m
Tutorial
Using the K Framework to Formalize Functional Languages
Tutorials
Xiaohong Chen University of Illinois at Urbana-Champaign, Grigore Roşu University of Illinois at Urbana-Champaign
14:30 - 16:10
Paper Session 2 - Animations and DemonstrationsHaskell at Haskell
Chair(s): Exequiel Rivas Inria Paris
14:30
30m
Talk
A Low-Latency Garbage Collector for GHC (Demo)
Haskell
Ben Gamari Well-Typed LLP, Laura Dietz University of New Hampshire
15:00
30m
Talk
Relational Lenses as a Library (Demo)
Haskell
Rudi Horn University of Edinburgh
File Attached
15:30
30m
Talk
Scripted Signal Functions
Haskell
DOI
16:00
10m
Other
PC Chair Report
Haskell
Tom Schrijvers KU Leuven
14:30 - 15:30
Afternoon KeynoteminiKanren at miniKanren
Chair(s): Jason Hemann Northeastern University, United States
14:30
60m
Keynote
The Pill is in The Proof: Saving Lives with Logic
miniKanren
Matthew Might University of Alabama at Birmingham | Harvard Medical School
15:20 - 17:40
15:20
2h20m
Social Event
ShutdownPL: Accountability
Social Events

15:20 - 17:40
15:20
2h20m
Social Event
ShutdownPL: Pedagogy
Social Events

15:20 - 17:40
15:20
2h20m
Social Event
ShutdownPL: Mentorship
Social Events

15:30 - 17:10
Afternoon SessionminiKanren at miniKanren
Chair(s): Nada Amin Harvard University, Weixi Ma Indiana University
15:30
20m
Talk
mediKanren: A System for Bio-medical Reasoning
miniKanren
Michael Patton University of Alabama at Birmingham, Gregory Rosenblatt University of Alabama at Birmingham, USA, William E. Byrd University of Alabama at Birmingham, USA, Matthew Might University of Alabama at Birmingham | Harvard Medical School
Link to publication
15:50
20m
Talk
Relational Synthesis for Pattern Matching
miniKanren
Dmitrii Kosarev JetBrains Research, Saint Petersburg State University, Dmitri Boulytchev St. Petersburg State University, St. Petersburg, Russia
Link to publication
16:10
20m
Talk
Some Novel miniKanren Synthesis Tasks
miniKanren
Jason Hemann Northeastern University, United States, Daniel P. Friedman Indiana University, USA
Link to publication
16:30
20m
Talk
A Relational Interpreter for Synthesizing JavaScript
miniKanren
Artem Chirkov University of Toronto Mississauga, Gregory Rosenblatt University of Alabama at Birmingham, USA, Matthew Might University of Alabama at Birmingham | Harvard Medical School, Lisa Zhang University of Toronto Mississauga
Link to publication
16:50
20m
Talk
dxo: A System for Relational Algebra and Differentiation
miniKanren
Julie Steele Georgetown Day School, William E. Byrd University of Alabama at Birmingham, USA
Link to publication
16:10 - 17:30
Designated Social Interaction TimeHaskell at Haskell

Fri 28 Aug

Displayed time zone: Eastern Time (US & Canada) change

05:30 - 08:30
EcosystemOCaml at OCaml
Chair(s): Florian Angeletti Inria

Infrastructure, tooling, and ecosystem in general.

05:30
60m
Keynote
The OCaml Platform
OCaml
06:30
30m
Talk
OCaml-CI : A Zero-Configuration CI
OCaml
Thomas Leonard OCaml Labs, Craig Ferguson Tarides, Kate Deplaix OCaml Labs, Magnus Skjegstad Tarides and OCaml Labs, Anil Madhavapeddy OCaml Labs
07:00
30m
Talk
The final pieces of the OCaml documentation puzzle
OCaml
Jonathan Ludlam University of Cambridge, Gabriel Radanne Inria, Leo White Jane Street
07:30
30m
Talk
API migration: compare transformed
OCaml
Joseph Harrison University of Kent, UK, Steven Varoumas University of Kent, Simon Thompson University of Kent, Reuben Rowe University College London
08:00
30m
Talk
Parallelising your OCaml Code with Multicore OCaml
OCaml
Sadiq Jaffer Opsian and OCaml Labs, Sudha Parimala IIT Madras, KC Sivaramakrishnan IIT Madras, Tom Kelly OCaml Labs, Anil Madhavapeddy OCaml Labs
Pre-print
09:00 - 12:00
Sessions 1 and 2HIW at HIW
09:00
22m
Talk
Asterius: bringing Haskell to WebAssembly
HIW
Cheng Shao Tweag I/O, Georgios Karachalias Tweag I/O, Hans Hoeglund Tweag I/O
09:22
22m
Talk
Multiple Home Units
HIW
10:00
35m
Talk
Lightning Talks 1
HIW

10:35
22m
Talk
Sweet Egison: a Haskell Library for Non-Deterministic Pattern Matching
HIW
Satoshi Egi Rakuten Institute of Technology, Rakuten, Inc. / The University of Tokyo, Akira Kawata Kyoto University, Mayuko Kori The University of Tokyo, Hiromi Ogawa University of Tsukuba
10:57
22m
Talk
Updating Immutable Code
HIW
Philipp Schuster University of Tübingen, Germany, David Binder University of Tübingen
11:19
12m
Talk
GHC Status Update
HIW
Simon Peyton Jones Microsoft, UK, Ben Gamari Well-Typed LLP
11:31
29m
Break
Social break
HIW

09:00 - 10:00
Designated Social Interaction TimeHaskell at Haskell
09:00 - 11:00
ApplicationsOCaml at OCaml
Chair(s): Marcello Seri Bernoulli Institute for Mathematics, Computer Science and Artificial Intelligence, University of Groningen

Talks about new and existing OCaml applications and libraries.

09:00
30m
Talk
A Simple State-Machine Framework for Property-Based Testing in OCaml
OCaml
Jan Midtgaard University of Southern Denmark
09:30
30m
Talk
The ImpFS filesystem
OCaml
Tom Ridge University of Leicester, UK
10:00
30m
Talk
Irmin v2
OCaml
Clément Pascutto Tarides, Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, Ioana Cristescu INRIA, France, Craig Ferguson Tarides, Thomas Gazagnaire Tarides, Romain Liautaud Tarides
10:30
30m
Talk
AD-OCaml: Algorithmic Differentiation for OCaml
OCaml
Markus Mottl Unaffiliated
09:00 - 12:30
Library-Oriented Dynamic Analysis with LyaTutorials at Tutorials 1
09:00
3h30m
Tutorial
Library-Oriented Dynamic Analysis with Lya
Tutorials
Nikos Vasilakis MIT CSAIL, USA, Grigoris Ntousakis TU Crete
10:00 - 11:00
Paper Session 3 - DatastructuresHaskell at Haskell
Chair(s): Andrey Mokhov Jane Street
10:00
30m
Talk
Finger Trees Explained Anew, and Slightly Simplified (Functional Pearl)
Haskell
Koen Claessen Chalmers University of Technology, Sweden
DOI
10:30
30m
Talk
Type Your Matrices for Great Good: A Haskell Library of Typed Matrices and Applications (Functional Pearl)
Haskell
Armando João Isaías Ferreira dos Santos University of Minho, Portugal / INESC TEC, Portugal, Jose Nuno Oliveira University of Minho, Portugal / INESC TEC, Portugal
DOI
10:00 - 11:00
Morning KeynoteScheme at Scheme
10:00
60m
Keynote
SICP JS: Ketchup on Caviar?
Scheme
Martin Henz National University of Singapore, Tobias Wrigstad Uppsala University, Sweden
11:30 - 13:00
Paper Session 4 - EffectsHaskell at Haskell
Chair(s): Pierre-Evariste Dagand LIP6/CNRS
11:30
30m
Talk
A Graded Monad for Deadlock-Free Concurrency (Functional Pearl)
Haskell
Andrej Ivašković University of Cambridge, UK, Alan Mycroft University of Cambridge, UK
DOI
12:00
30m
Talk
Composing Effects into Tasks and Workflows
Haskell
Yves Parès Tweag I/O, France, Jean-Philippe Bernardy University of Gothenburg, Sweden, Richard A. Eisenberg Tweag I/O
DOI
12:30
30m
Talk
Effect Handlers in Haskell, Evidently
Haskell
Ningning Xie Microsoft Research, USA, Daan Leijen Microsoft Research, USA
DOI
11:30 - 13:30
ExperienceOCaml at OCaml
Chair(s): Greta Yorsh Jane Street

Sharing experience about using OCaml in various scenarios.

11:30
30m
Talk
OCaml Under The Hood: SmartPy
OCaml
12:00
30m
Talk
A Declarative Syntax Definition for OCaml
OCaml
Luis Eduardo de Souza Amorim Delft University of Technology, Netherlands, Eelco Visser Delft University of Technology
Pre-print
12:30
30m
Talk
LexiFi Runtime Types
OCaml
Patrik Keller University of Innsbruck, Marc Lasson LexiFi
13:00
30m
Talk
Types in amber
OCaml
Paul Steckler O(1) Labs, Matthew Ryan O(1) Labs
11:30 - 13:00
Research Session 1Scheme at Scheme
11:30
30m
Talk
Clotho: A Racket Library for Parametric Randomness
Scheme
Pierce Darragh University of Utah, William G Hatch University of Utah, Eric Eide University of Utah
File Attached
12:00
30m
Talk
Scheme for scientific computing
Scheme
Francesco Montanari Universidad Autónoma de Madrid
File Attached
12:30
10m
Talk
Designing a Programming Environment Based on the Program Design Recipe (Lightning Talk)
Scheme
Junya Nose Tokyo Institute of Technology, Youyou Cong Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology
File Attached
12:40
10m
Talk
On Teaching Type Systems as Macros (Lightning Talk)
Scheme
Youyou Cong Tokyo Institute of Technology, Naoya Furudono Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology
File Attached
12:50
10m
Talk
Programming with Petri Nets to Reason about Concurrency (Lightning Talk)
Scheme
Julien Lepiller Yale University
File Attached
12:30 - 13:30
Session 3HIW at HIW
12:30
22m
Talk
Exactprint in GHC
HIW
12:52
22m
Talk
Liquid Haskell as a GHC Plugin
HIW
Alfredo Di Napoli Well-Typed LLP, Ranjit Jhala University of California at San Diego, USA, Andres Löh Well-Typed LLP, Niki Vazou IMDEA Software Institute
13:14
22m
Talk
Stan — Haskell Static Analyser
HIW
Dmitrii Kovanikov Standard Chartered, Veronika Romashkina None
14:00 - 17:30
Sessions 4 and 5HIW at HIW
14:00
22m
Talk
Implementation of linear types
HIW
14:22
22m
Talk
Circuit Notation Source Plugin
HIW
15:00
45m
Talk
Lightning Talks 2
HIW

15:45
12m
Talk
Embracing a Mechanized Formalization Gap: Interactive reasoning for Haskell at scale
HIW
Antal Spector-Zabusky University of Pennsylvania, Joachim Breitner DFINITY Foundation, Stephanie Weirich University of Pennsylvania, Yao Li University of Pennsylvania
16:00
20m
Talk
Closing
HIW
Ben Gamari Well-Typed LLP
14:00 - 15:00
Keynote IIOCaml at OCaml
Chair(s): Chris Casinghino Draper Laboratory

The recitation of the Keynote speech for those who weren’t able to attend the first one.

14:00
60m
Keynote
The OCaml Platform
OCaml
14:00 - 17:30
Building Multi-Language Tools with CubixTutorials at Tutorials 1
14:00
3h30m
Tutorial
Building Multi-Language Tools with Cubix
Tutorials
James Koppel Massachusetts Institute of Technology, USA
14:30 - 16:00
Paper Session 5 - TypesHaskell at Haskell
Chair(s): Jurriaan Hage Utrecht University, Netherlands
14:30
30m
Talk
Staged Sums of Products
Haskell
Matthew Pickering University of Bristol, UK, Andres Löh Well-Typed LLP, Nicolas Wu Imperial College London, UK
DOI
15:00
30m
Talk
Eliminating Bugs with Dependent Haskell (Experience Report)
Haskell
Noam Zilberstein Facebook, USA
DOI
15:30
30m
Talk
Stitch: The Sound Type-Indexed Type Checker (Functional Pearl)
Haskell
DOI File Attached
15:30 - 17:30
RecitationOCaml at OCaml
Chair(s): Chris Casinghino Draper Laboratory

Repeats Session I for those who weren’t able to attend the earlier time slot.

15:30
30m
Talk
API migration: compare transformed
OCaml
Joseph Harrison University of Kent, UK, Steven Varoumas University of Kent, Simon Thompson University of Kent, Reuben Rowe University College London
16:00
30m
Talk
OCaml-CI : A Zero-Configuration CI
OCaml
Thomas Leonard OCaml Labs, Craig Ferguson Tarides, Kate Deplaix OCaml Labs, Magnus Skjegstad Tarides and OCaml Labs, Anil Madhavapeddy OCaml Labs
16:30
30m
Talk
The final pieces of the OCaml documentation puzzle
OCaml
Jonathan Ludlam University of Cambridge, Gabriel Radanne Inria, Leo White Jane Street
17:00
30m
Talk
Parallelising your OCaml Code with Multicore OCaml
OCaml
Sadiq Jaffer Opsian and OCaml Labs, Sudha Parimala IIT Madras, KC Sivaramakrishnan IIT Madras, Tom Kelly OCaml Labs, Anil Madhavapeddy OCaml Labs
Pre-print
16:00 - 17:30
Designated Social Interaction TimeHaskell at Haskell
16:00 - 17:00
Afternoon KeynoteScheme at Scheme
16:00
60m
Keynote
21st Century Lisp in Academic Research and Pedagogy
Scheme
Bohdan Khomtchouk University of Chicago, Jonah Fleishhacker University of Chicago
17:30 - 19:30
FARM PerformanceSocial Events at FARM Performance
17:30
2h
Social Event
FARM Performance
Social Events
C: Donya Quick Stevens Institute of Technology