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

Conference Dates
Conference Dates are in time zone (GMT-04:00) Eastern Time (US & Canada), and may differ from the viewed time zone.
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

Conference Day
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. PierceUniversity of Pennsylvania

Conference Day
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. PierceUniversity of Pennsylvania

Conference Day
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ősCisco Systems
07:50
10m
Day opening
Opening
Erlang
Annette BieniusaTechnische Universität Kaiserslautern, Viktória FördősCisco Systems
08:00
30m
Short-paper
Transformations towards Clean Functional Code
Erlang
Boldizsár PoórEötvös Loránd University, Melinda TóthEö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 BaranyaiELTE Eötvös Loránd University, István BozóEötvös Loránd University, Melinda TóthEö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 ZellerTU Kaiserslautern, Annette BieniusaTechnische Universität Kaiserslautern, Carla FerreiraUniversidade 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 LevyUniversity of Birmingham
09:15
45m
Talk
Kripke open relations and operational game semantics
HOPE
Guilhem JaberUniversité de Nantes, Andrzej MurawskiUniversity of Oxford
10:00
45m
Talk
Merging coeffect production into effect handling
HOPE
Tarmo UustaluReykjavik University, Tallinn University of Technology, Niels VoorneveldTallinn University of Technology
10:45
45m
Talk
Simply RaTT: A Fitch-style Modal Calculus for Reactive Programming
HOPE
Patrick BahrIT University of Copenhagen, Christian Uldal GraulundIT University of Copenhagen, Rasmus Ejlers MøgelbergIT University of Copenhagen
09:00 - 10:00
09:00
15m
Day opening
Welcome
PLMW @ ICFP
Lindsey KuperUniversity of California, Santa Cruz, Talia RingerUniversity of Washington, Nate FosterCornell University
09:15
45m
Talk
How To Write Papers So People Can Read Them
PLMW @ ICFP
09:00 - 12:30
Teaching Functional ProgrammingTutorials at Tutorials 1
09:00
3h30m
Tutorial
Teaching Functional Programming
Tutorials
Michael SperberActive 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ärenzsonnen 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 JuanChalmers University of Technology, Nils Anders DanielssonUniversity 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 CeulemansVrije Universiteit Brussel, Dominique DevrieseVrije Universiteit Brussel
File Attached
11:00
30m
Talk
Generalization of Meta-Programs with Dependent Types in Mtac2 with Mtac2 (Extended Abstract)
TyDe
Ignacio TiraboschiNone, Jan-Oliver KaiserMPI-SWS, Beta ZilianiFAMAF, UNC and CONICET
10:30 - 12:00
Session 2Erlang at Erlang
Chair(s): Annette BieniusaTechnische Universität Kaiserslautern
10:30
30m
Full-paper
Machine-Checked Natural Semantics for Core Erlang: Exceptions and Side Effects
Erlang
Simon ThompsonUniversity of Kent, Dániel HorpácsiEötvös Loránd University, Péter BereczkyEötvös Loránd University
DOI
11:00
30m
Full-paper
Secure Design and Verification of Erlang Systems
Erlang
Viktória FördősCisco Systems
DOI
11:30
30m
Full-paper
Clojerl: The Expressive Power of Clojure on the BEAM
Erlang
Juan Facorro, Natalia ChechinaBournemouth University
DOI
10:30 - 12:30
10:30
40m
Talk
Constraint Solvers for the Working PL Researcher
PLMW @ ICFP
Nadia PolikarpovaUniversity of California, San Diego
11:10
40m
Talk
Managing your Research, your Advisor, your PhD
PLMW @ ICFP
Amal AhmedNortheastern University, USA
11:50
40m
Talk
Basic Mechanics of Operational Semantics
PLMW @ ICFP
David Van HornUniversity of Maryland, USA
12:30 - 13:30
Session 3Erlang at Erlang
Chair(s): Viktória FördősCisco Systems, Annette BieniusaTechnische Universität Kaiserslautern
12:30
60m
Keynote
Living on the Edge with Erlang
Erlang
Peter Van RoyUniversité catholique de Louvain
12:30 - 14:00
Session 2TyDe at TyDe
12:30
30m
Talk
Graded Modal Dependent Type Theory (Extended Abstract)
TyDe
Benjamin MoonSchool of Computing, University of Kent, Harley D. Eades IIIAugusta University, Dominic OrchardUniversity of Kent, UK
File Attached
13:00
30m
Talk
Frex: indexing modulo equations with free extensions (Extended Abstract)
TyDe
Guillaume AllaisUniversity of St Andrews, Edwin BradyUniversity of St. Andrews, UK, Ohad KammarUniversity of Edinburgh, Jeremy YallopUniversity of Cambridge
13:30
30m
Talk
Retrofitting Symbolic Holes to LLVM IR (Extended Abstract)
TyDe
Bruce CollieUniversity of Edinburgh, Michael F. P. O'BoyleUniversity 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. GajdaMigamake 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 NikhilBluespec, Inc.
14:30 - 16:00
Session 3HOPE at HOPE
14:30
45m
Talk
Effectful Improvement Theory
HOPE
Martin CeresaUNR - CIFASIS - CONICET
15:15
45m
Talk
Alef: A bidirectional effect system for algebraic effects.
HOPE
Antonio LocascioUniversidad 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 ReynoldsUniversity of Missouri, William HarrisonOak Ridge National Laboratory, Rohit ChadhaUniversity of Missouri, Gerard AllweinU.S. Naval Research Laboratory
16:30
30m
Talk
Developing a Dependently Typed Language with Runtime Proof Search (Extended Abstract)
TyDe
Mark LemayBoston University, Cheng ZhangBoston University, William BlairBoston 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 JonesMicrosoft, UK, P: Kathleen FisherTufts University, USA, P: Jose CalderonGalois, Inc., P: Benjamin C. PierceUniversity of Pennsylvania, P: Sarah E. ChasinsUniversity of California, Berkeley, P: Jeff VaughanGoogle
18:00 - 19:30
TyDe SocialTyDe at TyDe

Join the Zoom via Clowdr

Conference Day
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 ShanIndiana 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 WeirichUniversity of Pennsylvania
10:30 - 11:30
10:30
60m
Meeting
How to Use Clowdr at ICFP
Social Events
Benjamin C. PierceUniversity 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 LowenthalUniversity of Cambridge
10:55
8m
Poster
Pattern Matching with Typed Holes
Student Research Competition
Yongwei YuanUniversity of Michigan
11:04
8m
Poster
Type Hole Inference
Student Research Competition
Zhiyi PanUniversity of Michigan
11:12
8m
Poster
Semantics for a Simple Differentiable Language Using Distribution Theory
Student Research Competition
Christopher LamCornell University
11:21
8m
Poster
Gradual Enforcement of IO Trace Properties
Student Research Competition
Cezar-Constantin AndriciAlexandru Ioan Cuza University of Iasi
11:30 - 13:00
New York 1ICFP Program at ICFP NY 1
Chair(s): Adam ChlipalaMassachusetts Institute of Technology

Public livestreams: YouTube, Bilibili (China)

11:30
15m
Talk
Stable Relations and Abstract Interpretation of Higher-Order Programs
ICFP Program
DOI Media Attached File Attached
11:45
15m
Talk
Higher-Order Demand-Driven Symbolic Evaluation
ICFP Program
Zachary PalmerSwarthmore College, Theodore ParkSwarthmore and Hopkins, Scott F. SmithThe Johns Hopkins University, Shiwei WengThe Johns Hopkins University
DOI Media Attached
12:00
15m
Talk
Sparcl: A Language for Partially-Invertible Computation
ICFP Program
Kazutaka MatsudaTohoku University, Japan, Meng WangUniversity of Bristol, UK
DOI Media Attached
12:15
15m
Talk
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
ICFP Program
Nikhil SwamyMicrosoft Research, Aseem RastogiMicrosoft Research, Aymeric FromherzCarnegie Mellon University, Denis MerigouxINRIA, Danel AhmanUniversity of Ljubljana, Guido MartínezCIFASIS-CONICET, Argentina
DOI Media Attached
12:30
15m
Talk
TLC: Temporal Logic of Distributed Components
ICFP Program
Jeremiah GriffinUniversity of California, Riverside, Mohsen LesaniUniversity of California, Riverside, Narges ShadabUniversity of California, Riverside, Xizhe YinUnivsersity of California, Riverside
DOI Media Attached
12:45
15m
Talk
Effect Handlers, Evidently
ICFP Program
Ningning XieMicrosoft Research, USA, Jonathan Immanuel BrachthäuserUniversity of Tübingen, Germany, Daniel HillerströmThe University of Edinburgh, Philipp SchusterUniversity of Tübingen, Germany, Daan LeijenMicrosoft 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 WeirichUniversity 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 JeffreyMozilla 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 HagedornUniversity of Münster, Germany, Johannes LenfersUniversity of Münster, Thomas KoehlerUniversity of Glasgow, United Kingdom, Xueying QinUniversity of Glasgow, United Kingdom, Sergei GorlatchUniversity of Münster, Germany, Michel SteuwerThe University of Edinburgh
DOI Media Attached
14:45
15m
Talk
Staged Selective Parser Combinators
ICFP Program
Jamie WillisImperial College London, Nicolas WuImperial College London, UK, Matthew PickeringUniversity of Bristol, UK
DOI Media Attached
15:00
15m
Talk
Kindly Bent to Free Us
ICFP Program
Gabriel RadanneInria, Hannes SaffrichUniversity of Freiburg, Peter ThiemannUniversity of Freiburg, Germany
DOI Pre-print Media Attached File Attached
15:15
15m
Talk
Sealing Pointer-Based Optimizations Behind Pure Functions
ICFP Program
Daniel SelsamMicrosoft Research, Simon HudonCarnegie Mellon University, Leonardo de MouraMicrosoft Research, n.n.
DOI Media Attached
15:30
15m
Talk
Effects for Efficiency: Asymptotic Speedup with First-Class Control
ICFP Program
Daniel HillerströmThe University of Edinburgh, Sam LindleyHeriot-Watt University, UK / The University of Edinburgh, UK, John LongleyThe University of Edinburgh
DOI Media Attached
15:45
15m
Talk
Computation Focusing
ICFP Program
Nick RiouxUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania
DOI Media Attached
16:00
15m
Talk
Retrofitting Parallelism onto OCamlDistinguished Paper
ICFP Program
KC SivaramakrishnanIIT Madras, Stephen DolanUniversity of Cambridge, UK, Leo WhiteJane Street, Sadiq JafferOpsian and OCaml Labs, Tom KellyOCaml Labs, Anmol SahooIIT Madras, Sudha ParimalaIIT Madras, Atul DhimanIIT Madras, Anil MadhavapeddyOCaml Labs
DOI Media Attached
16:15
15m
Talk
Liquid Information Flow ControlDistinguished Paper
ICFP Program
Nadia PolikarpovaUniversity of California, San Diego, Deian StefanUniversity of California at San Diego, USA, Jean YangCarnegie Mellon University, Shachar ItzhakyTechnion, Israel, Travis HanceCarnegie Mellon University, Armando Solar-LezamaMassachusetts 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 JeugtFugue, Niki VazouIMDEA Software Institute, Leonidas LampropoulosUniversity 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 CifuentesOracle Labs

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

21:00
60m
Social Event
Women in CS Panel
Social Events
P: Cristina CifuentesOracle Labs, P: Sukyoung RyuKAIST, P: Alena GriffithsRGB Assurance, P: Behnaz HassanshahiOracle Labs, Australia
22:00 - 23:00
22:00
60m
Meeting
How to Use Clowdr at ICFP
Social Events
Benjamin C. PierceUniversity of Pennsylvania
22:30 - 00:00
Asia 1ICFP Program at ICFP Asia 1
Chair(s): Adam ChlipalaMassachusetts Institute of Technology

Public livestreams: YouTube, Bilibili (China)

22:30
15m
Talk
Stable Relations and Abstract Interpretation of Higher-Order Programs
ICFP Program
DOI Media Attached File Attached
22:45
15m
Talk
Higher-Order Demand-Driven Symbolic Evaluation
ICFP Program
Zachary PalmerSwarthmore College, Theodore ParkSwarthmore and Hopkins, Scott F. SmithThe Johns Hopkins University, Shiwei WengThe Johns Hopkins University
DOI Media Attached
23:00
15m
Talk
Sparcl: A Language for Partially-Invertible Computation
ICFP Program
Kazutaka MatsudaTohoku University, Japan, Meng WangUniversity of Bristol, UK
DOI Media Attached
23:15
15m
Talk
SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs
ICFP Program
Nikhil SwamyMicrosoft Research, Aseem RastogiMicrosoft Research, Aymeric FromherzCarnegie Mellon University, Denis MerigouxINRIA, Danel AhmanUniversity of Ljubljana, Guido MartínezCIFASIS-CONICET, Argentina
DOI Media Attached
23:30
15m
Talk
TLC: Temporal Logic of Distributed Components
ICFP Program
Jeremiah GriffinUniversity of California, Riverside, Mohsen LesaniUniversity of California, Riverside, Narges ShadabUniversity of California, Riverside, Xizhe YinUnivsersity of California, Riverside
DOI Media Attached
23:45
15m
Talk
Effect Handlers, Evidently
ICFP Program
Ningning XieMicrosoft Research, USA, Jonathan Immanuel BrachthäuserUniversity of Tübingen, Germany, Daniel HillerströmThe University of Edinburgh, Philipp SchusterUniversity of Tübingen, Germany, Daan LeijenMicrosoft 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

Conference Day
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 JhalaUniversity of California at San Diego, USA
02:30 - 04:30
Asia 2ICFP Program at ICFP Asia 2
Chair(s): Alan JeffreyMozilla 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 HagedornUniversity of Münster, Germany, Johannes LenfersUniversity of Münster, Thomas KoehlerUniversity of Glasgow, United Kingdom, Xueying QinUniversity of Glasgow, United Kingdom, Sergei GorlatchUniversity of Münster, Germany, Michel SteuwerThe University of Edinburgh
DOI Media Attached
02:45
15m
Talk
Staged Selective Parser Combinators
ICFP Program
Jamie WillisImperial College London, Nicolas WuImperial College London, UK, Matthew PickeringUniversity of Bristol, UK
DOI Media Attached
03:00
15m
Talk
Kindly Bent to Free Us
ICFP Program
Gabriel RadanneInria, Hannes SaffrichUniversity of Freiburg, Peter ThiemannUniversity of Freiburg, Germany
DOI Pre-print Media Attached File Attached
03:15
15m
Talk
Sealing Pointer-Based Optimizations Behind Pure Functions
ICFP Program
Daniel SelsamMicrosoft Research, Simon HudonCarnegie Mellon University, Leonardo de MouraMicrosoft Research, n.n.
DOI Media Attached
03:30
15m
Talk
Effects for Efficiency: Asymptotic Speedup with First-Class Control
ICFP Program
Daniel HillerströmThe University of Edinburgh, Sam LindleyHeriot-Watt University, UK / The University of Edinburgh, UK, John LongleyThe University of Edinburgh
DOI Media Attached
03:45
15m
Talk
Computation Focusing
ICFP Program
Nick RiouxUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania
DOI Media Attached
04:00
15m
Talk
Retrofitting Parallelism onto OCamlDistinguished Paper
ICFP Program
KC SivaramakrishnanIIT Madras, Stephen DolanUniversity of Cambridge, UK, Leo WhiteJane Street, Sadiq JafferOpsian and OCaml Labs, Tom KellyOCaml Labs, Anmol SahooIIT Madras, Sudha ParimalaIIT Madras, Atul DhimanIIT Madras, Anil MadhavapeddyOCaml Labs
DOI Media Attached
04:15
15m
Talk
Liquid Information Flow ControlDistinguished Paper
ICFP Program
Nadia PolikarpovaUniversity of California, San Diego, Deian StefanUniversity of California at San Diego, USA, Jean YangCarnegie Mellon University, Shachar ItzhakyTechnion, Israel, Travis HanceCarnegie Mellon University, Armando Solar-LezamaMassachusetts 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 IgarashiKyoto University, Japan, Sukyoung RyuKAIST, Ilya SergeyYale-NUS College and National University of Singapore, Alex PotaninVictoria 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 ChlipalaMassachusetts 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 WeirichUniversity of Pennsylvania
10:30 - 11:30
10:30
60m
Social Event
Virtual Art Gallery
Social Events
Alan JeffreyMozilla Research
10:30 - 11:30
10:30
30m
Meeting
SIGPLAN CARES
Social Events
David WalkerPrinceton University, USA, Simon Peyton JonesMicrosoft, UK, Alexandra SilvaUniversity College London, Shriram KrishnamurthiBrown University, United States
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
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 PerezIMDEA Software Institute, Pablo NogueiraESNE University School of Design, Innovation and Technology
DOI Media Attached
11:52
11m
Talk
Local algebraic effect theoriesJFP
ICFP Program
Žiga Lukšič, Matija PretnarUniversity of Ljubljana, Slovenia
DOI Media Attached
12:03
11m
Talk
Heterogeneous binary random-access listsJFP
ICFP Program
Wouter SwierstraUtrecht University, Netherlands
DOI Media Attached
12:15
11m
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
11m
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
11m
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
11m
Talk
Emerging languages: An alternative approach to teaching programming languagesJFP
ICFP Program
Saverio PeruginiUniversity 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 WeirichUniversity of Pennsylvania
13:30 - 14:30
LGBTQ MeetupSocial Events at ICFP Social
13:30
60m
Talk
LGBTQ Meetup
Social Events
David WalkerPrinceton University, USA, Matthew WeaverPrinceton University
14:30 - 16:30
New York 4ICFP Program at ICFP NY 4
Chair(s): Stephanie WeirichUniversity 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 KnothUniversity of California at San Diego, USA, Di WangCarnegie Mellon University, Adam ReynoldsUniversity of California, San Diego, Nadia PolikarpovaUniversity of California, San Diego, Jan HoffmannCarnegie Mellon University
DOI Media Attached
15:00
15m
Talk
Cosmo: A Concurrent Separation Logic for Multicore OCaml
ICFP Program
Glen MévelInria, Université Paris-Saclay, CNRS, Laboratoire de recherche en informatique, Jacques-Henri JourdanUniversersité Paris Saclay, CNRS, LRI, François PottierInria, France
DOI Media Attached
15:15
15m
Talk
Composing and Decomposing Op-Based CRDTs with Semidirect Products
ICFP Program
Matthew WeidnerCarnegie Mellon University, Christopher MeiklejohnCarnegie Mellon University, Heather MillerCarnegie Mellon University
DOI Media Attached
15:30
15m
Talk
A Quick Look at ImpredicativityDistinguished Paper
ICFP Program
Alejandro Serrano47 Degrees, Spain, Jurriaan HageUtrecht University, Netherlands, Simon Peyton JonesMicrosoft, UK, Dimitrios VytiniotisDeepMind
DOI Pre-print Media Attached
15:45
15m
Talk
A Unified View of Modalities in Type Systems
ICFP Program
Andreas AbelGothenburg University, Jean-Philippe BernardyUniversity of Gothenburg, Sweden
DOI Media Attached
16:00
15m
Talk
Lower Your Guards: A Compositional Pattern-Match Coverage Checker
ICFP Program
Sebastian GrafKarlsruhe Institute of Technology, Simon Peyton JonesMicrosoft, UK, Ryan ScottGalois, Inc.
Link to publication DOI Media Attached
16:15
15m
Talk
Signature restriction for polymorphic algebraic effects
ICFP Program
Taro SekiyamaNational Institute of Informatics, Takeshi TsukadaChiba University, Japan, Atsushi IgarashiKyoto 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 CalderonGalois, Inc., Paulette KoronkevichUniversity 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 WalkerPrinceton University, USA, Simon Peyton JonesMicrosoft, UK, Alexandra SilvaUniversity College London, Shriram KrishnamurthiBrown 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 DanvyYale-NUS College and School of Computing, Singapore
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
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 PerezIMDEA Software Institute, Pablo NogueiraESNE University School of Design, Innovation and Technology
DOI Media Attached
22:52
11m
Talk
Local algebraic effect theoriesJFP
ICFP Program
Žiga Lukšič, Matija PretnarUniversity of Ljubljana, Slovenia
DOI Media Attached
23:03
11m
Talk
Heterogeneous binary random-access listsJFP
ICFP Program
Wouter SwierstraUtrecht University, Netherlands
DOI Media Attached
23:15
11m
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
11m
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
11m
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
11m
Talk
Emerging languages: An alternative approach to teaching programming languagesJFP
ICFP Program
Saverio PeruginiUniversity 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

Conference Day
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
02:30 - 04:30
Asia 4ICFP Program at ICFP Asia 4
Chair(s): Stephanie WeirichUniversity 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 KnothUniversity of California at San Diego, USA, Di WangCarnegie Mellon University, Adam ReynoldsUniversity of California, San Diego, Nadia PolikarpovaUniversity of California, San Diego, Jan HoffmannCarnegie Mellon University
DOI Media Attached
03:00
15m
Talk
Cosmo: A Concurrent Separation Logic for Multicore OCaml
ICFP Program
Glen MévelInria, Université Paris-Saclay, CNRS, Laboratoire de recherche en informatique, Jacques-Henri JourdanUniversersité Paris Saclay, CNRS, LRI, François PottierInria, France
DOI Media Attached
03:15
15m
Talk
Composing and Decomposing Op-Based CRDTs with Semidirect Products
ICFP Program
Matthew WeidnerCarnegie Mellon University, Christopher MeiklejohnCarnegie Mellon University, Heather MillerCarnegie Mellon University
DOI Media Attached
03:30
15m
Talk
A Quick Look at ImpredicativityDistinguished Paper
ICFP Program
Alejandro Serrano47 Degrees, Spain, Jurriaan HageUtrecht University, Netherlands, Simon Peyton JonesMicrosoft, UK, Dimitrios VytiniotisDeepMind
DOI Pre-print Media Attached
03:45
15m
Talk
A Unified View of Modalities in Type Systems
ICFP Program
Andreas AbelGothenburg University, Jean-Philippe BernardyUniversity of Gothenburg, Sweden
DOI Media Attached
04:00
15m
Talk
Lower Your Guards: A Compositional Pattern-Match Coverage Checker
ICFP Program
Sebastian GrafKarlsruhe Institute of Technology, Simon Peyton JonesMicrosoft, UK, Ryan ScottGalois, Inc.
Link to publication DOI Media Attached
04:15
15m
Talk
Signature restriction for polymorphic algebraic effects
ICFP Program
Taro SekiyamaNational Institute of Informatics, Takeshi TsukadaChiba University, Japan, Atsushi IgarashiKyoto 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 KrishnaswamiComputer 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 WeirichUniversity 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 WeirichUniversity of Pennsylvania

Public livestreams: YouTube, iQIYI (China)

09:45
45m
Talk
Award Presentations & Chair Report
ICFP Program
Stephanie WeirichUniversity of Pennsylvania, Adam ChlipalaMassachusetts Institute of Technology, Mira MeziniTechnische Universität Darmstadt, Sukyoung RyuKAIST, Jens PalsbergUniversity of California, Los Angeles, Youyou CongTokyo Institute of Technology
10:30 - 11:00
10:30
30m
Other
Information Desk
Social Events
Stephanie WeirichUniversity of Pennsylvania
11:00 - 13:00
New York 5ICFP Program at ICFP NY 5
Chair(s): Richard A. EisenbergTweag I/O

Public livestreams: YouTube, Bilibili (China)

11:00
15m
Talk
Denotational Recurrence Extraction for Amortized Analysis
ICFP Program
Joseph W. CutlerWesleyan University, Dan LicataWesleyan University, Norman DannerWesleyan 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 StumpThe University of Iowa, USA, Chris JenkinsThe University of Iowa, Stephan SpahnThe University of Iowa, Colin McDonaldUniversity of Notre Dame
DOI Media Attached
11:45
15m
Talk
Duplo: A Framework for OCaml Post-Link Optimisation
ICFP Program
Nandor LickerUniversity of Cambridge, Timothy M. JonesUniversity of Cambridge, UK
DOI Media Attached
12:00
15m
Talk
Recovering Purity with Comonads and Capabilities
ICFP Program
Vikraman ChoudhuryIndiana University & University of Cambridge, Neel KrishnaswamiComputer Laboratory, University of Cambridge
DOI Media Attached
12:15
15m
Talk
A General Approach to Define Binders Using Matching Logic
ICFP Program
Xiaohong ChenUniversity of Illinois at Urbana-Champaign, Grigore RoşuUniversity of Illinois at Urbana-Champaign
DOI Media Attached
12:30
15m
Talk
Parsing with Zippers (Functional Pearl)
ICFP Program
Pierce DarraghUniversity of Utah, Michael D. AdamsUniversity of Michigan
DOI Media Attached
12:45
15m
Talk
Regular Language Type Inference with Term Rewriting
ICFP Program
Timothée HaudebourgUniv Rennes, Inria, CNRS, IRISA, Thomas GenetIRISA, Univ Rennes, Thomas P. JensenINRIA 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 WeirichUniversity of Pennsylvania
13:30 - 14:30
Virtualization Feedback 1Social Events at ICFP Social 2
13:30
60m
Meeting
Virtualization Feedback
Social Events
Benjamin C. PierceUniversity of Pennsylvania, Jonathan BellNortheastern University, Crista LopesUniversity of California, Irvine
14:30 - 16:25
New York 6ICFP Program at ICFP NY 6
Chair(s): Sukyoung RyuKAIST

Public livestreams: YouTube, Bilibili (China)

14:30
15m
Talk
Compiling Effect Handlers in Capability-Passing Style
ICFP Program
Philipp SchusterUniversity of Tübingen, Germany, Jonathan Immanuel BrachthäuserUniversity of Tübingen, Germany, Klaus OstermannUniversity 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. GiarrussoBedRock Systems, Leo StefanescoIRIF, University Paris Diderot & CNRS, Amin TimanyAarhus University, Lars BirkedalAarhus University, Robbert KrebbersDelft 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ščákUniversity of St Andrews
DOI Media Attached
15:15
15m
Talk
Raising Expectations: Automating Expected Cost Analysis with Types
ICFP Program
Di WangCarnegie Mellon University, David M. KahnCarnegie Mellon University, Jan HoffmannCarnegie Mellon University
DOI Media Attached
15:30
15m
Talk
Program Sketching with Live Bidirectional Evaluation
ICFP Program
Justin LubinUniversity of Chicago, Nick CollinsUniversity of Chicago, Cyrus OmarUniversity of Michigan, Ravi ChughUniversity of Chicago
DOI Media Attached
15:45
15m
Talk
Elaboration with First-Class Implicit Function Types
ICFP Program
András KovácsEötvös Loránd University
DOI Pre-print Media Attached
16:00
15m
Talk
Kinds are Calling Conventions
ICFP Program
Paul DownenUniversity of Oregon, USA, Zena M. AriolaUniversity of Oregon, USA, Simon Peyton JonesMicrosoft, UK, Richard A. EisenbergTweag I/O
DOI Media Attached
16:15
10m
Day closing
Conference closing
ICFP Program
Stephanie WeirichUniversity 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. PierceUniversity of Pennsylvania, Jonathan BellNortheastern University, Crista LopesUniversity of California, Irvine
22:30 - 00:00
Asia 5ICFP Program at ICFP Asia 5
Chair(s): Richard A. EisenbergTweag I/O

Public livestreams: YouTube, Bilibili (China)

22:00
30m
Talk
Denotational Recurrence Extraction for Amortized Analysis
ICFP Program
Joseph W. CutlerWesleyan University, Dan LicataWesleyan University, Norman DannerWesleyan 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 StumpThe University of Iowa, USA, Chris JenkinsThe University of Iowa, Stephan SpahnThe University of Iowa, Colin McDonaldUniversity of Notre Dame
DOI Media Attached
22:45
15m
Talk
Duplo: A Framework for OCaml Post-Link Optimisation
ICFP Program
Nandor LickerUniversity of Cambridge, Timothy M. JonesUniversity of Cambridge, UK
DOI Media Attached
23:00
15m
Talk
Recovering Purity with Comonads and Capabilities
ICFP Program
Vikraman ChoudhuryIndiana University & University of Cambridge, Neel KrishnaswamiComputer Laboratory, University of Cambridge
DOI Media Attached
23:15
15m
Talk
A General Approach to Define Binders Using Matching Logic
ICFP Program
Xiaohong ChenUniversity of Illinois at Urbana-Champaign, Grigore RoşuUniversity of Illinois at Urbana-Champaign
DOI Media Attached
23:30
15m
Talk
Parsing with Zippers (Functional Pearl)
ICFP Program
Pierce DarraghUniversity of Utah, Michael D. AdamsUniversity of Michigan
DOI Media Attached
23:45
15m
Talk
Regular Language Type Inference with Term Rewriting
ICFP Program
Timothée HaudebourgUniv Rennes, Inria, CNRS, IRISA, Thomas GenetIRISA, Univ Rennes, Thomas P. JensenINRIA 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

Conference Day
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 FelleisenPLT @ Northeastern University
02:30 - 04:25
Asia 6ICFP Program at ICFP Asia 6
Chair(s): Sukyoung RyuKAIST

Public livestreams: YouTube, Bilibili (China)

02:30
15m
Talk
Compiling Effect Handlers in Capability-Passing Style
ICFP Program
Philipp SchusterUniversity of Tübingen, Germany, Jonathan Immanuel BrachthäuserUniversity of Tübingen, Germany, Klaus OstermannUniversity 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. GiarrussoBedRock Systems, Leo StefanescoIRIF, University Paris Diderot & CNRS, Amin TimanyAarhus University, Lars BirkedalAarhus University, Robbert KrebbersDelft 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ščákUniversity of St Andrews
DOI Media Attached
03:15
15m
Talk
Raising Expectations: Automating Expected Cost Analysis with Types
ICFP Program
Di WangCarnegie Mellon University, David M. KahnCarnegie Mellon University, Jan HoffmannCarnegie Mellon University
DOI Media Attached
03:30
15m
Talk
Program Sketching with Live Bidirectional Evaluation
ICFP Program
Justin LubinUniversity of Chicago, Nick CollinsUniversity of Chicago, Cyrus OmarUniversity of Michigan, Ravi ChughUniversity of Chicago
DOI Media Attached
03:45
15m
Talk
Elaboration with First-Class Implicit Function Types
ICFP Program
András KovácsEötvös Loránd University
DOI Pre-print Media Attached
04:00
15m
Talk
Kinds are Calling Conventions
ICFP Program
Paul DownenUniversity of Oregon, USA, Zena M. AriolaUniversity of Oregon, USA, Simon Peyton JonesMicrosoft, UK, Richard A. EisenbergTweag I/O
DOI Media Attached
04:15
10m
Day closing
Conference closing
ICFP Program
Stephanie WeirichUniversity 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 KrishnaswamiComputer Laboratory, University of Cambridge
09:00 - 12:30
09:00
3h30m
Tutorial
Functional Software Architecture
Tutorials
Michael SperberActive 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 CoblenzCarnegie Mellon University, Jonathan AldrichCarnegie Mellon University
09:00 - 11:00
Morning KeynoteminiKanren at miniKanren
Chair(s): Dmitri BoulytchevSt. Petersburg State University, St. Petersburg, Russia
10:00
60m
Keynote
Executing Declarative Language Definitions
miniKanren
K: Eelco VisserDelft 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 KampsOpen University of the Netherlands, Netherlands, Bastiaan HeerenOpen University of the Netherlands, Netherlands, Johan JeuringOpen University of the Netherlands, Netherlands
DOI
12:00
30m
Talk
Describing Microservices using Modern Haskell (Experience Report)
Haskell
Alejandro Serrano47 Degrees, Spain, Flavio Corpa47 Degrees, Spain
DOI
12:30
30m
Talk
Towards Secure IoT Programming in Haskell
Haskell
Nachiappan ValliappanChalmers University of Technology, Sweden, Robert KrookChalmers University of Technology, Sweden, Alejandro RussoChalmers University of Technology, Sweden, Koen ClaessenChalmers University of Technology, Sweden
DOI
11:30 - 13:30
Morning SessionminiKanren at miniKanren
Chair(s): Joseph P. NearUniversity of Vermont, Gregory RosenblattUniversity of Alabama at Birmingham, USA
11:30
20m
Talk
On Fair Relational Conjunction
miniKanren
Petr LozovSain Petersburg State University, SPbGU, Dmitri BoulytchevSt. Petersburg State University, St. Petersburg, Russia
Pre-print
11:50
20m
Talk
An Empirical Study of Partial Deduction for miniKanren
miniKanren
Ekaterina VerbitskaiaJetBrains, Daniil BerezunJetBrains, Russia, Dmitri BoulytchevSt. Petersburg State University, St. Petersburg, Russia
Pre-print
12:10
20m
Talk
MicroKanren in J: an Embedding of the Relational Paradigm in an Array Language with Rank-Polymorphic Unification
miniKanren
Raoul SchorerGeneva University Hospitals
Pre-print
12:30
20m
Talk
λKanren: Higher-order Logic Programming with Shallow Embedding
miniKanren
Weixi MaIndiana University, Kuang-Chen LuIndiana University Bloomington, Daniel P. FriedmanIndiana University, USA
Pre-print
12:50
20m
Talk
Kanren Light: A Dynamically Semi-Certified Interactive Logic Programming System
miniKanren
Marco MaggesiUniversità di Firenze, Massimo NocentiniUniversità di Firenze
Pre-print
13:10
20m
Talk
Certified Semantics for Disequality
miniKanren
Dmitry RozplokhasHigher School of Economics, Dmitri BoulytchevSt. Petersburg State University, St. Petersburg, Russia
Pre-print
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 FonerGalois, Niki CarrollGeorge Mason University, Priya SrikumarCornell University, David JustoUniversity of California, San Diego, Justin LubinUniversity of Chicago, Akash Gaonkar, Alan JeffreyMozilla 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 ChenUniversity of Illinois at Urbana-Champaign, Grigore RoşuUniversity of Illinois at Urbana-Champaign
14:30 - 16:10
Paper Session 2 - Animations and DemonstrationsHaskell at Haskell
Chair(s): Exequiel RivasInria Paris
14:30
30m
Talk
A Low-Latency Garbage Collector for GHC (Demo)
Haskell
Ben GamariWell-Typed LLP, Laura DietzUniversity of New Hampshire
15:00
30m
Talk
Relational Lenses as a Library (Demo)
Haskell
Rudi HornUniversity of Edinburgh
File Attached
15:30
30m
Talk
Scripted Signal Functions
Haskell
DOI
16:00
10m
Other
PC Chair Report
Haskell
14:30 - 15:30
Afternoon KeynoteminiKanren at miniKanren
Chair(s): Jason HemannNortheastern University, United States
14:30
60m
Keynote
The Pill is in The Proof: Saving Lives with Logic
miniKanren
Matthew MightUniversity 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 AminHarvard University, Weixi MaIndiana University
15:30
20m
Talk
mediKanren: A System for Bio-medical Reasoning
miniKanren
Michael PattonUniversity of Alabama at Birmingham, Gregory RosenblattUniversity of Alabama at Birmingham, USA, William E. ByrdUniversity of Alabama at Birmingham, USA, Matthew MightUniversity of Alabama at Birmingham | Harvard Medical School
Pre-print
15:50
20m
Talk
Relational Synthesis for Pattern Matching
miniKanren
Dmitrii KosarevJetBrains Research, Saint Petersburg State University, Dmitri BoulytchevSt. Petersburg State University, St. Petersburg, Russia
Pre-print
16:10
20m
Talk
Some Novel miniKanren Synthesis Tasks
miniKanren
Jason HemannNortheastern University, United States, Daniel P. FriedmanIndiana University, USA
Pre-print
16:30
20m
Talk
A Relational Interpreter for Synthesizing JavaScript
miniKanren
Artem ChirkovUniversity of Toronto Mississauga, Gregory RosenblattUniversity of Alabama at Birmingham, USA, Matthew MightUniversity of Alabama at Birmingham | Harvard Medical School, Lisa ZhangUniversity of Toronto Mississauga
Pre-print
16:50
20m
Talk
dxo: A System for Relational Algebra and Differentiation
miniKanren
Julie SteeleGeorgetown Day School, William E. ByrdUniversity of Alabama at Birmingham, USA
Pre-print
16:10 - 17:30
Designated Social Interaction TimeHaskell at Haskell

Conference Day
Fri 28 Aug

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

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

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 LeonardOCaml Labs, Craig FergusonTarides, Kate DeplaixOCaml Labs, Magnus SkjegstadTarides and OCaml Labs, Anil MadhavapeddyOCaml Labs
07:00
30m
Talk
The final pieces of the OCaml documentation puzzle
OCaml
Jonathan LudlamUniversity of Cambridge, Gabriel RadanneInria, Leo WhiteJane Street
07:30
30m
Talk
API migration: compare transformed
OCaml
Joseph HarrisonUniversity of Kent, UK, Steven VaroumasUniversity of Kent, Simon ThompsonUniversity of Kent, Reuben RoweUniversity College London
08:00
30m
Talk
Parallelising your OCaml Code with Multicore OCaml
OCaml
Sadiq JafferOpsian and OCaml Labs, Sudha ParimalaIIT Madras, KC SivaramakrishnanIIT Madras, Tom KellyOCaml Labs, Anil MadhavapeddyOCaml Labs
Pre-print
09:00 - 12:00
Sessions 1 and 2HIW at HIW
09:00
22m
Talk
Asterius: bringing Haskell to WebAssembly
HIW
Cheng ShaoTweag I/O, Georgios KarachaliasTweag I/O, Hans HoeglundTweag 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 EgiRakuten Institute of Technology, Rakuten, Inc. / The University of Tokyo, Akira KawataKyoto University, Mayuko KoriThe University of Tokyo, Hiromi OgawaUniversity of Tsukuba
10:57
22m
Talk
Updating Immutable Code
HIW
Philipp SchusterUniversity of Tübingen, Germany, David BinderUniversity of Tübingen
11:19
12m
Talk
GHC Status Update
HIW
Simon Peyton JonesMicrosoft, UK, Ben GamariWell-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 SeriBernoulli 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 MidtgaardUniversity of Southern Denmark
09:30
30m
Talk
The ImpFS filesystem
OCaml
Tom RidgeUniversity of Leicester, UK
10:00
30m
Talk
Irmin v2
OCaml
Clément PascuttoTarides, Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, Ioana CristescuINRIA, France, Craig FergusonTarides, Thomas GazagnaireTarides, Romain LiautaudTarides
10:30
30m
Talk
AD-OCaml: Algorithmic Differentiation for OCaml
OCaml
Markus MottlUnaffiliated
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 VasilakisMIT CSAIL, USA, Grigoris NtousakisTU Crete
10:00 - 11:00
Paper Session 3 - DatastructuresHaskell at Haskell
Chair(s): Andrey MokhovJane Street
10:00
30m
Talk
Finger Trees Explained Anew, and Slightly Simplified (Functional Pearl)
Haskell
Koen ClaessenChalmers 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 SantosUniversity of Minho, Portugal / INESC TEC, Portugal, Jose Nuno OliveiraUniversity 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 HenzNational University of Singapore, Tobias WrigstadUppsala University, Sweden
11:30 - 13:00
Paper Session 4 - EffectsHaskell at Haskell
Chair(s): Pierre-Evariste DagandLIP6/CNRS
11:30
30m
Talk
A Graded Monad for Deadlock-Free Concurrency (Functional Pearl)
Haskell
Andrej IvaškovićUniversity of Cambridge, UK, Alan MycroftUniversity of Cambridge, UK
DOI
12:00
30m
Talk
Composing Effects into Tasks and Workflows
Haskell
Yves ParèsTweag I/O, France, Jean-Philippe BernardyUniversity of Gothenburg, Sweden, Richard A. EisenbergTweag I/O
DOI
12:30
30m
Talk
Effect Handlers in Haskell, Evidently
Haskell
Ningning XieMicrosoft Research, USA, Daan LeijenMicrosoft Research, USA
DOI
11:30 - 13:30
ExperienceOCaml at OCaml
Chair(s): Greta YorshJane 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 AmorimDelft University of Technology, Netherlands, Eelco VisserDelft University of Technology
Pre-print
12:30
30m
Talk
LexiFi Runtime Types
OCaml
Patrik KellerUniversity of Innsbruck, Marc LassonLexiFi
13:00
30m
Talk
Types in amber
OCaml
Paul StecklerO(1) Labs, Matthew RyanO(1) Labs
11:30 - 13:00
Research Session 1Scheme at Scheme
11:30
30m
Talk
Clotho: A Racket Library for Parametric Randomness
Scheme
Pierce DarraghUniversity of Utah, William G HatchUniversity of Utah, Eric EideUniversity of Utah
File Attached
12:00
30m
Talk
Scheme for scientific computing
Scheme
Francesco MontanariUniversidad Autónoma de Madrid
File Attached
12:30
10m
Talk
Designing a Programming Environment Based on the Program Design Recipe (Lightning Talk)
Scheme
Junya NoseTokyo Institute of Technology, Youyou CongTokyo Institute of Technology, Hidehiko MasuharaTokyo Institute of Technology
File Attached
12:40
10m
Talk
On Teaching Type Systems as Macros (Lightning Talk)
Scheme
Youyou CongTokyo Institute of Technology, Naoya FurudonoTokyo Institute of Technology, Hidehiko MasuharaTokyo Institute of Technology
File Attached
12:50
10m
Talk
Programming with Petri Nets to Reason about Concurrency (Lightning Talk)
Scheme
julien lepillerYale 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 NapoliWell-Typed LLP, Ranjit JhalaUniversity of California at San Diego, USA, Andres LöhWell-Typed LLP, Niki VazouIMDEA Software Institute
13:14
22m
Talk
Stan — Haskell Static Analyser
HIW
Dmitrii KovanikovStandard Chartered, Veronika RomashkinaNone
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-ZabuskyUniversity of Pennsylvania, Joachim BreitnerDFINITY Foundation, Stephanie WeirichUniversity of Pennsylvania, Yao LiUniversity of Pennsylvania
16:00
20m
Talk
Closing
HIW
Ben GamariWell-Typed LLP
14:00 - 15:00
Keynote IIOCaml at OCaml
Chair(s): Chris CasinghinoDraper 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 KoppelMassachusetts Institute of Technology, USA
14:30 - 16:00
Paper Session 5 - TypesHaskell at Haskell
Chair(s): Jurriaan HageUtrecht University, Netherlands
14:30
30m
Talk
Staged Sums of Products
Haskell
Matthew PickeringUniversity of Bristol, UK, Andres LöhWell-Typed LLP, Nicolas WuImperial College London, UK
DOI
15:00
30m
Talk
Eliminating Bugs with Dependent Haskell (Experience Report)
Haskell
Noam ZilbersteinFacebook, 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 CasinghinoDraper 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 HarrisonUniversity of Kent, UK, Steven VaroumasUniversity of Kent, Simon ThompsonUniversity of Kent, Reuben RoweUniversity College London
16:00
30m
Talk
OCaml-CI : A Zero-Configuration CI
OCaml
Thomas LeonardOCaml Labs, Craig FergusonTarides, Kate DeplaixOCaml Labs, Magnus SkjegstadTarides and OCaml Labs, Anil MadhavapeddyOCaml Labs
16:30
30m
Talk
The final pieces of the OCaml documentation puzzle
OCaml
Jonathan LudlamUniversity of Cambridge, Gabriel RadanneInria, Leo WhiteJane Street
17:00
30m
Talk
Parallelising your OCaml Code with Multicore OCaml
OCaml
Sadiq JafferOpsian and OCaml Labs, Sudha ParimalaIIT Madras, KC SivaramakrishnanIIT Madras, Tom KellyOCaml Labs, Anil MadhavapeddyOCaml 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 KhomtchoukUniversity of Chicago, Jonah FleishhackerUniversity of Chicago
17:30 - 19:30
FARM PerformanceSocial Events at FARM Performance
17:30
2h
Social Event
FARM Performance
Social Events
C: Donya QuickStevens Institute of Technology