Program - ICFP 2021

Detailed Table Session Timeline Detailed Timeline

Time Zone

The program is currently displayed in (GMT+09:00) Seoul.

Use conference time zone: (GMT+09:00) SeoulSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

You're viewing the program in a time zone which is different from your device's time zone change time zone

Sun 22 Aug
Displayed time zone: Seoul change

16:00 - 17:30	Session 1HOPE at HOPE

16:00 30m Talk		Representing Monads with Capabilities HOPE Aleksander Boruch-Gruszecki EPFL, Jonathan Immanuel Brachthäuser EPFL, Martin Odersky EPFL
16:30 30m Talk		Higher-order Programming with Effects and Handlers — with First-Class Functions HOPE Jonathan Immanuel Brachthäuser EPFL, Philipp Schuster University of Tübingen, Edward Lee University of Waterloo, Aleksander Boruch-Gruszecki EPFL
17:00 30m Talk		Computational and Contextual Program Differences: Reasoning About Non-equivalent Effectful Programs in an Higher-Order Scenario HOPE Ugo Dal Lago University of Bologna, Italy / Inria, France, Francesco Gavazzo University of Bologna & INRIA Sophia Antipolis

18:00 - 19:30	Session 1FHPNC at FHPNC

18:00 15m Day opening		Welcome to FHPNC 2021 FHPNC Troels Henriksen University of Copenhagen, Denmark, Gabriele Keller Utrecht University
18:15 30m Talk		Generating High Performance Code for Irregular Data Structures using Dependent Types FHPNC Federico Pizzuti University of Edinburgh, Michel Steuwer University of Edinburgh, Christophe Dubach McGill University
18:45 30m Talk		Improving GHC Haskell NUMA Profiling FHPNC Ruairidh Macgregor University of Glasgow, Phil Trinder University of Glasgow, Hans-Wolfgang Loidl Heriot-Watt University, UK

18:00 - 19:30	Session 2HOPE at HOPE

18:00 30m Talk		The Functional Machine Calculus HOPE Willem Heijltjes University of Bath
18:30 30m Talk		Formalising Algebraic Effects with Non-Recoverable Failure HOPE Timotej Tomandl University of Kent, Dominic Orchard University of Kent, UK Pre-print
19:00 30m Talk		Computational calculus: bridging reduction and evaluation HOPE Claudia Faggian Université de Paris & CNRS, Giulio Guerrieri University of Bath, Riccardo Treglia Università di Torino File Attached

18:00 - 19:30	Deductive Verification of OCaml Programs with Cameleer 1Tutorials at Tutorials

18:00 90m Tutorial		Deductive Verification of OCaml Programs in Cameleer Tutorials Mário Pereira LRI - Université Paris-Sud

20:00 - 21:30	GHC 1HIW at HIW Chair(s): Ningning Xie University of Toronto

20:00 22m Talk		Exact Print Annotations in GHC HIW Alan Zimmerman
20:22 22m Talk		Avoiding quadratic GHC core code size HIW Edsko de Vries Well-Typed LLP, Andres Löh Well-Typed LLP
20:44 22m Talk		Improvements to GHC's parallel garbage collector HIW Douglas Wilson Well Typed

20:00 - 21:30	Session 3HOPE at HOPE

20:00 30m Talk		Higher-Order Asynchronous Effects HOPE Danel Ahman University of Ljubljana, Matija Pretnar University of Ljubljana, Slovenia, Janez Radešček University of Ljubljana Pre-print File Attached
20:30 30m Talk		Handler calculus HOPE Sam Lindley The University of Edinburgh, UK File Attached
21:00 30m Talk		A Monad for Shared-State Concurrency HOPE Yotam Dvir Tel Aviv University, Ori Lahav Tel Aviv University, Ohad Kammar University of Edinburgh File Attached

20:00 - 21:30	Deductive Verification of OCaml Programs with Cameleer 2Tutorials at Tutorials

20:00 90m Tutorial		Deductive Verification of OCaml Programs in Cameleer Tutorials Mário Pereira LRI - Université Paris-Sud

20:00 - 21:30	Session ITyDe at TyDe Chair(s): Hsiang-Shang ‘Josh’ Ko Institute of Information Science, Academia Sinica

20:00 30m Talk		Interactive Haskell Type Inference Exploration (Extended Abstract) TyDe Shuai Fu Monash University, Tim Dwyer Monash University, Peter J. Stuckey Monash University File Attached
20:30 30m Talk		Contextual Effect Polymorphism Meets Bidirectional Effects (Extended Abstract) TyDe Kazuki Niimi Tokyo Institute of Technology, Youyou Cong Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology, Jonathan Immanuel Brachthäuser EPFL File Attached
21:00 30m Talk		Translation Certification for Smart Contracts (Extended Abstract) TyDe Jacco Krijnen Utrecht University, Manuel Chakravarty Tweag & IOHK, Gabriele Keller Utrecht University, Wouter Swierstra Utrecht University, Netherlands File Attached

22:00 - 23:00	Invited talk by Sven-Bodo ScholzFHPNC at FHPNC

22:00 60m Talk		Is Functional HPC the Key to Low Carbon Computing? by Sven-Bodo Scholz FHPNC

22:00 - 23:30	KeynoteHIW at HIW Chair(s): Ningning Xie University of Toronto

22:00 60m Talk		Haskell reinterpreted – large-scale real-world experience with the Mu compiler in Financial Markets HIW Marten Agren Standard Chartered Bank File Attached

22:00 - 23:00	Session 1PLMW @ ICFP at PLMW

22:00 15m Day opening		Welcome and Opening Remarks PLMW @ ICFP C: Jose Calderon Galois, Inc., C: Lindsey Kuper University of California at Santa Cruz
22:15 45m Talk		How to Write Papers So People Can Read Them PLMW @ ICFP S: Derek Dreyer MPI-SWS

22:00 - 23:30	KeynoteTyDe at TyDe Chair(s): Hsiang-Shang ‘Josh’ Ko Institute of Information Science, Academia Sinica

22:00 60m Keynote		Integrating Agda with SMT-LIB – An incomplete list of pits I fell inTyDe Keynote TyDe Wen Kokke University of Edinburgh

23:15 - 01:00	Session 2PLMW @ ICFP at PLMW

23:15 60m Panel		"I don't get it!" Panel PLMW @ ICFP M: Ronald Garcia University of British Columbia, P: Patricia Johann Appalachian State University, P: Norman Ramsey Tufts University, P: Steve Zdancewic University of Pennsylvania, P: Andrew D. Gordon Microsoft Research and University of Edinburgh
00:15 45m Talk		Managing Your Research, Your Advisor, Your Ph.D. PLMW @ ICFP S: Amal Ahmed Northeastern University, USA

23:30 - 01:00	Session 2FHPNC at FHPNC

23:30 30m Talk		Parallelism-preserving automatic differentiation for second-order array languages FHPNC Adam Paszke Google Research, Matthew J. Johnson Google Research, Roy Frostig Google Research, Dougal Maclaurin Google Research
00:00 30m Talk		Reverse Automatic Differentiation for Accelerate (Extended Abstract) FHPNC Tom Smeding Utrecht University, Matthijs Vákár Utrecht University, Trevor L. McDonell Utrecht University
00:30 30m Talk		Computing Persistent Homology in Futhark FHPNC Erik von Brömssen Chalmers University of Technology

23:30 - 01:00	Types and GHC 2HIW at HIW Chair(s): Andres Löh Well-Typed LLP

23:30 22m Talk		Generalization is hard, but somebody's got to do it HIW Richard A. Eisenberg Tweag
23:52 22m Talk		A new interface for GHC typechecker plugins and type-family rewriting HIW Sam Derbyshire Tweag Media Attached
00:14 22m Talk		The Dynamic Haskell Plugin for GHC HIW Matthías Páll Gissurarson Chalmers University of Technology, Sweden, Agustín Mista Chalmers University of Technology
00:36 22m Talk		GHC Status update HIW Simon Peyton Jones Microsoft, UK File Attached

23:30 - 01:00	Session 4HOPE at HOPE

23:30 30m Talk		First-class Names for Effect Handlers HOPE Ningning Xie University of Toronto, Youyou Cong Tokyo Institute of Technology, Daan Leijen Microsoft Research
00:00 30m Talk		Tensor Partial Evaluation HOPE Eli Bingham Broad Institute, Fritz Obermeyer Broad Institute of MIT and Harvard, Yerdos Ordabayev Brandeis University, Du Phan UIUC File Attached
00:30 30m Talk		Dynamic Scope + Laziness = Counterfactuals HOPE James Koppel Massachusetts Institute of Technology, USA, Armando Solar-Lezama Massachusetts Institute of Technology, Zenna Tavares Massachusetts Institute of Technology, Xin Zhang Peking University File Attached

23:30 - 01:00	Teaching Functional Programming 1Tutorials at Tutorials

23:30 90m Tutorial		Teaching Functional Programming Tutorials Michael Sperber Active Group GmbH

23:30 - 01:00	Session IITyDe at TyDe Chair(s): Dominic Orchard University of Kent, UK

23:30 30m Talk		Gradual Correctness: a Dynamically Bidirectional Full-Spectrum Dependent Type Theory (Extended Abstract) TyDe Mark Lemay Boston University, Qiancheng Fu Boston University, Hongwei Xi Boston University Media Attached File Attached
00:00 30m Talk		A Simpler Encoding of Indexed Types TyDe Tesla Zhang The Pennsylvania State University Link to publication DOI Pre-print Media Attached
00:30 30m Talk		Optics for Generic Declarative Server APIs (Extended Abstract) TyDe Andre Videla University Of Strathclyde Media Attached File Attached

Mon 23 Aug
Displayed time zone: Seoul change

	01:30 - 03:00	Community update and discussionFHPNC at FHPNC 45 min community update: brief summary (about 5-7 mins) of current work and future plans from Abhiroop Sarkar (Chalmers) Adam Pazke (JAX, Google Research) Michel Steuwer (University of Edinburgh) Hand-Wolfgang Loidl (Dependable Systems Group, Heriot-Watt University) and Phil Trinder (Glasgow Parallelism Group, Glasgow University) Sven-Bodo Scholz (Radboud University) Martin Elsman (DIKU, Futhark) Trevor McDonell (Utrecht University, Accelerate) 45 min discussion: future of FHPNC

01:30 - 03:00	ToolsHIW at HIW Chair(s): Daan Leijen Microsoft Research

01:30 22m Talk		Testing Haskell with Mocks HIW Chris Smith
01:52 22m Talk		Adventures in GHC compile times HIW Jeffrey M. Young Tweag, Richard A. Eisenberg Tweag
02:14 7m Talk		Lightning Talk: Pinned Warnings HIW Aaron Allen
02:21 7m Talk		Lightning Talk: GSOL: A Confluence Checker for Haskell Rewrite Rules HIW Faustin Date , Makoto Hamana Gunma University, Japan File Attached

01:30 - 03:00	Teaching Functional Programming 2Tutorials at Tutorials

01:30 90m Tutorial		Teaching Functional Programming Tutorials Michael Sperber Active Group GmbH

01:30 - 03:00	Session IIITyDe at TyDe Chair(s): Dominic Orchard University of Kent, UK

01:30 30m Talk		Actions You Can Handle: Dependent Types for AI Plans TyDe Alasdair Hill Heriot-Watt University, Ekaterina Komendantskaya Heriot-Watt University, UK, Matthew L. Daggitt Heriot-Watt University, Ronald P. A. Petrick Heriot-Watt University DOI Pre-print Media Attached
02:00 30m Talk		Co-Contextual Typing Inference for the Linear π-Calculus in Agda (Extended Abstract) TyDe Uma Zalakain University of Glasgow, Ornela Dardha University of Glasgow File Attached

02:00 - 03:30	Session 3PLMW @ ICFP at PLMW

02:00 45m Talk		Introduction to Mechanized Metatheory PLMW @ ICFP S: Brigitte Pientka McGill University
02:45 45m Talk		Emotional Machines PLMW @ ICFP S: Aaron Turon MPI-SWS

03:00 - 03:30	PLTeaPLTea at PLTea

03:00 30m Social Event		PLTea PLTea

03:30 - 05:00	Applications and ClosingHIW at HIW Chair(s): Edsko de Vries Well-Typed LLP

03:30 22m Talk		Securing Web-Applications with A Refinement Typed ORM HIW Nico Lehmann University of California, San Diego, Rose Kunkel University of California, San Diego, Niki Vazou IMDEA Software Institute, Nadia Polikarpova University of California at San Diego, Deian Stefan University of California at San Diego, USA, Ranjit Jhala University of California at San Diego
03:52 22m Talk		Generics for Hardware: Adding Haskell-inspired Generics to Bluespec HIW Lucas Kramer Google, Ravi Nanavati
04:14 3m Talk		Closing HIW Ningning Xie University of Toronto

04:00 - 06:15	Session 4PLMW @ ICFP at PLMW

04:00 90m Other		Small-group Mentoring Meetings PLMW @ ICFP
05:30 45m Talk		Increasing the Impact of PL Research PLMW @ ICFP S: Michael Hicks University of Maryland at College Park

16:00 - 17:30	Session 1Research Papers at ICFP Talks +12h Watch it on YouTube: https://youtu.be/x9Aecy3zVzk Watch it on Bilibili: https://www.bilibili.com/video/BV1VL4y1v7XK/

16:00 15m Talk		Client-Server Sessions in Linear LogicDistinguished Paper Research Papers Zesen Qian Aarhus University, Alex Kavvos University of Bristol, Lars Birkedal Aarhus University DOI Media Attached
16:15 15m Talk		An Order-Aware Dataflow Model for Parallel Unix Pipelines Research Papers Shivam Handa Massachusetts Institute of Technology, Konstantinos Kallas University of Pennsylvania, Nikos Vasilakis Massachusetts Institute of Technology, Martin C. Rinard Massachusetts Institute of Technology DOI Media Attached
16:30 15m Talk		CPS Transformation with Affine Types for Call-By-Value Implicit Polymorphism Research Papers Taro Sekiyama National Institute of Informatics, Takeshi Tsukada Chiba University, Japan DOI Media Attached
16:45 15m Talk		Getting to the Point: Index Sets and Parallelism-Preserving Autodiff for Pointful Array ProgrammingDistinguished Paper Research Papers Adam Paszke Google Research, Daniel D. Johnson Google Research, David Kristjanson Duvenaud University of Toronto, Dimitrios Vytiniotis DeepMind, Alexey Radul Google Research, Matthew J. Johnson Google Research, Jonathan Ragan-Kelley MIT CSAIL, Dougal Maclaurin Google Research DOI Media Attached
17:00 15m Talk		Propositions-as-Types and Shared State Research Papers Pedro Rocha Nova University of Lisbon, Luís Caires Universidade Nova de Lisboa and NOVA LINCS DOI Media Attached
17:15 15m Talk		Efficient Tree-Traversals: Reconciling Parallelism and Dense Data Representations Research Papers Chaitanya S. Koparkar Indiana University, Mike Rainey Carnegie Mellon University, Michael Vollmer University of Kent, Milind Kulkarni Purdue University, Ryan R. Newton Facebook DOI Media Attached

16:15 - 17:45	Q&A 1Research Papers at ICFP Q&A +12h

16:15 15m Live Q&A		Q&A: Client-Server Sessions in Linear LogicMirror Research Papers
16:30 15m Live Q&A		Q&A: An Order-Aware Dataflow Model for Parallel Unix PipelinesBoth Research Papers
16:45 15m Live Q&A		Q&A: CPS Transformation with Affine Types for Call-By-Value Implicit PolymorphismBoth Research Papers
17:00 15m Live Q&A		Q&A: Getting to the Point: Index Sets and Parallelism-Preserving Autodiff for Pointful Array ProgrammingBoth Research Papers
17:15 15m Live Q&A		Q&A: Propositions-as-Types and Shared StateBoth Research Papers
17:30 15m Live Q&A		Q&A: Efficient Tree-Traversals: Reconciling Parallelism and Dense Data RepresentationsBoth Research Papers

18:00 - 18:30	PLTeaPLTea at PLTea +12h

18:00 30m Social Event		PLTea PLTea

18:30 - 19:30	SRC Poster SessionStudent Research Competition at Student Research Competition

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

19:00 - 20:45	Session 2Research Papers at ICFP Talks +12h Watch it on YouTube: https://youtu.be/e4I_fX-vBco Watch it on Bilibili: https://www.bilibili.com/video/BV1w3411B75A/

19:00 15m Talk		Contextual Modal Types for Algebraic Effects and Handlers Research Papers Nikita Zyuzin IMDEA Software Institute, Aleksandar Nanevski IMDEA Software Institute DOI Media Attached
19:15 15m Talk		Calculating Dependently-Typed Compilers (Functional Pearl) Research Papers Mitchell Pickard University of Nottingham, Graham Hutton University of Nottingham DOI Media Attached
19:30 15m Talk		Reasoning about Effect Interaction by Fusion Research Papers Zhixuan Yang Imperial College London, Nicolas Wu Imperial College London, UK DOI Pre-print Media Attached
19:45 15m Talk		Compositional Optimizations for CertiCoq Research Papers Zoe Paraskevopoulou Northeastern University, John M. Li Princeton University, Andrew W. Appel Princeton DOI Media Attached
20:00 15m Talk		Generalized Evidence Passing for Effect Handlers Research Papers Ningning Xie University of Toronto, Daan Leijen Microsoft Research DOI Media Attached
20:15 15m Talk		Deriving Efficient Program Transformations from Rewrite Rules Research Papers John M. Li Princeton University, Andrew W. Appel Princeton University DOI Media Attached
20:30 15m Talk		Algebras for Weighted Search Research Papers Donnacha Oisín Kidney Imperial College London, Nicolas Wu Imperial College London, UK DOI Media Attached

19:15 - 21:00	Q&A 2Research Papers at ICFP Q&A +12h

19:15 15m Live Q&A		Q&A: Contextual Modal Types for Algebraic Effects and HandlersBoth Research Papers
19:30 15m Live Q&A		Q&A: Calculating Dependently-Typed Compilers (Functional Pearl)Main Research Papers
19:45 15m Live Q&A		Q&A: Reasoning about Effect Interaction by FusionMain Research Papers
20:00 15m Live Q&A		Q&A: Compositional Optimizations for CertiCoqMain Research Papers
20:15 15m Live Q&A		Q&A: Generalized Evidence Passing for Effect HandlersMirror Research Papers
20:30 15m Live Q&A		Q&A: Deriving Efficient Program Transformations from Rewrite RulesMirror Research Papers
20:45 15m Live Q&A		Q&A: Algebras for Weighted SearchMain Research Papers

21:00 - 21:30	PLTeaPLTea at PLTea +12h

21:00 30m Social Event		PLTea PLTea

21:30 - 22:00	Ask Me AnythingSocial Events at Social Chair(s): Jeehoon Kang KAIST

21:30 30m Live Q&A		Ask Me Anything on Rust with Ralf Jung Social Events Ralf Jung MPI-SWS

22:00 - 23:00	Keynote 1Research Papers at Keynotes

22:00 60m Keynote		Fun, Funky, Functional: The Pursuit of Better User Interfaces for Programming Research Papers Ravi Chugh University of Chicago Media Attached

Tue 24 Aug
Displayed time zone: Seoul change

00:00 - 01:00	PL Card GameSocial Events at Social

00:00 60m Social Event		PL Card Game Social Events Media Attached

01:00 - 01:30	BloombergSocial Events at Social

01:00 30m Social Event		OCaml at Bloomberg Social Events HongChang Wu

04:00 - 05:30	Session 1Research Papers at ICFP Talks Watch it on YouTube: https://youtu.be/j4Lme7vLl_o

04:00 15m Talk		Client-Server Sessions in Linear LogicDistinguished Paper Research Papers Zesen Qian Aarhus University, Alex Kavvos University of Bristol, Lars Birkedal Aarhus University DOI Media Attached
04:15 15m Talk		An Order-Aware Dataflow Model for Parallel Unix Pipelines Research Papers Shivam Handa Massachusetts Institute of Technology, Konstantinos Kallas University of Pennsylvania, Nikos Vasilakis Massachusetts Institute of Technology, Martin C. Rinard Massachusetts Institute of Technology DOI Media Attached
04:30 15m Talk		CPS Transformation with Affine Types for Call-By-Value Implicit Polymorphism Research Papers Taro Sekiyama National Institute of Informatics, Takeshi Tsukada Chiba University, Japan DOI Media Attached
04:45 15m Talk		Getting to the Point: Index Sets and Parallelism-Preserving Autodiff for Pointful Array ProgrammingDistinguished Paper Research Papers Adam Paszke Google Research, Daniel D. Johnson Google Research, David Kristjanson Duvenaud University of Toronto, Dimitrios Vytiniotis DeepMind, Alexey Radul Google Research, Matthew J. Johnson Google Research, Jonathan Ragan-Kelley MIT CSAIL, Dougal Maclaurin Google Research DOI Media Attached
05:00 15m Talk		Propositions-as-Types and Shared State Research Papers Pedro Rocha Nova University of Lisbon, Luís Caires Universidade Nova de Lisboa and NOVA LINCS DOI Media Attached
05:15 15m Talk		Efficient Tree-Traversals: Reconciling Parallelism and Dense Data Representations Research Papers Chaitanya S. Koparkar Indiana University, Mike Rainey Carnegie Mellon University, Michael Vollmer University of Kent, Milind Kulkarni Purdue University, Ryan R. Newton Facebook DOI Media Attached

04:15 - 05:45	Q&A 1Research Papers at ICFP Q&A

04:15 15m Live Q&A		Q&A: Client-Server Sessions in Linear LogicMirror Research Papers
04:30 15m Live Q&A		Q&A: An Order-Aware Dataflow Model for Parallel Unix PipelinesBoth Research Papers
04:45 15m Live Q&A		Q&A: CPS Transformation with Affine Types for Call-By-Value Implicit PolymorphismBoth Research Papers
05:00 15m Live Q&A		Q&A: Getting to the Point: Index Sets and Parallelism-Preserving Autodiff for Pointful Array ProgrammingBoth Research Papers
05:15 15m Live Q&A		Q&A: Propositions-as-Types and Shared StateBoth Research Papers
05:30 15m Live Q&A		Q&A: Efficient Tree-Traversals: Reconciling Parallelism and Dense Data RepresentationsBoth Research Papers

06:00 - 06:30	PLTeaPLTea at PLTea

06:00 30m Social Event		PLTea PLTea

06:30 - 07:00	Ask Me AnythingSocial Events at Social Chair(s): Michael Hicks University of Maryland at College Park

06:30 30m Live Q&A		Ask Me Anything on Climate Change with Benjamin Pierce Social Events Benjamin C. Pierce University of Pennsylvania

07:00 - 08:45	Session 2Research Papers at ICFP Talks Watch it on YouTube: https://youtu.be/VzTecUbVSzI

07:00 15m Talk		Contextual Modal Types for Algebraic Effects and Handlers Research Papers Nikita Zyuzin IMDEA Software Institute, Aleksandar Nanevski IMDEA Software Institute DOI Media Attached
07:15 15m Talk		Calculating Dependently-Typed Compilers (Functional Pearl) Research Papers Mitchell Pickard University of Nottingham, Graham Hutton University of Nottingham DOI Media Attached
07:30 15m Talk		Reasoning about Effect Interaction by Fusion Research Papers Zhixuan Yang Imperial College London, Nicolas Wu Imperial College London, UK DOI Pre-print Media Attached
07:45 15m Talk		Compositional Optimizations for CertiCoq Research Papers Zoe Paraskevopoulou Northeastern University, John M. Li Princeton University, Andrew W. Appel Princeton DOI Media Attached
08:00 15m Talk		Generalized Evidence Passing for Effect Handlers Research Papers Ningning Xie University of Toronto, Daan Leijen Microsoft Research DOI Media Attached
08:15 15m Talk		Deriving Efficient Program Transformations from Rewrite Rules Research Papers John M. Li Princeton University, Andrew W. Appel Princeton University DOI Media Attached
08:30 15m Talk		Algebras for Weighted Search Research Papers Donnacha Oisín Kidney Imperial College London, Nicolas Wu Imperial College London, UK DOI Media Attached

07:15 - 09:00	Q&A 2Research Papers at ICFP Q&A

07:15 15m Live Q&A		Q&A: Contextual Modal Types for Algebraic Effects and HandlersBoth Research Papers
07:30 15m Live Q&A		Q&A: Calculating Dependently-Typed Compilers (Functional Pearl)Main Research Papers
07:45 15m Live Q&A		Q&A: Reasoning about Effect Interaction by FusionMain Research Papers
08:00 15m Live Q&A		Q&A: Compositional Optimizations for CertiCoqMain Research Papers
08:15 15m Live Q&A		Q&A: Generalized Evidence Passing for Effect HandlersMirror Research Papers
08:30 15m Live Q&A		Q&A: Deriving Efficient Program Transformations from Rewrite RulesMirror Research Papers
08:45 15m Live Q&A		Q&A: Algebras for Weighted SearchMain Research Papers

09:00 - 09:30	PLTeaPLTea at PLTea

09:00 30m Social Event		PLTea PLTea

16:00 - 17:30	Session 3Research Papers at ICFP Talks +12h Watch it on YouTube: https://youtu.be/NMxyiYHT2Mc Watch it on Bilibili: https://www.bilibili.com/video/BV1fo4y1U7uc/

16:00 15m Talk		Modular, Compositional, and Executable Formal Semantics for LLVM IR Research Papers Yannick Zakowski Inria, Calvin Beck University of Pennsylvania, Irene Yoon University of Pennsylvania, Ilya Zaichuk Taras Shevchenko National University of Kyiv, Vadim Zaliva University of Cambridge, UK, Steve Zdancewic University of Pennsylvania DOI Media Attached
16:15 15m Talk		Higher-Order Probabilistic Adversarial Computations: Categorical Semantics and Program Logics Research Papers Alejandro Aguirre Aarhus University, Gilles Barthe MPI-SP; IMDEA Software Institute, Marco Gaboardi Boston University, Deepak Garg MPI-SWS, Shin-ya Katsumata National Institute of Informatics, Tetsuya Sato Tokyo Institute of Technology DOI Media Attached
16:30 15m Talk		How to Evaluate Blame for Gradual Types Research Papers Lukas Lazarek Northwestern University, Ben Greenman Brown University, Matthias Felleisen Northeastern University, Christos Dimoulas PLT @ Northwestern University DOI Media Attached
16:45 15m Talk		ProbNV: Probabilistic Verification of Network Control Planes Research Papers Nick Giannarakis University of Wisconsin-Madison, Alexandra Silva University College London, David Walker Princeton University DOI Media Attached
17:00 15m Talk		Of JavaScript AOT Compilation Performance Research Papers Manuel Serrano Inria, France DOI Media Attached
17:15 15m Talk		Symbolic and Automatic Differentiation of Languages Research Papers Conal Elliott n.n. DOI Media Attached

16:15 - 17:45	Q&A 3Research Papers at ICFP Q&A +12h

16:15 15m Live Q&A		Q&A: Modular, Compositional, and Executable Formal Semantics for LLVM IRBoth Research Papers
16:30 15m Live Q&A		Q&A: Higher-Order Probabilistic Adversarial Computations: Categorical Semantics and Program LogicsBoth Research Papers
16:45 15m Live Q&A		Q&A: How to Evaluate Blame for Gradual TypesMirror Research Papers
17:00 15m Live Q&A		Q&A: ProbNV: Probabilistic Verification of Network Control PlanesMirror Research Papers
17:15 15m Live Q&A		Q&A: Of JavaScript AOT Compilation PerformanceMain Research Papers
17:30 15m Live Q&A		Q&A: Symbolic and Automatic Differentiation of LanguagesMirror Research Papers

18:00 - 18:30	PLTeaPLTea at PLTea +12h

18:00 30m Talk		PLTea PLTea

18:30 - 19:00	SIGPLAN CARESSocial Events at CARES

18:30 30m Meeting		SIGPLAN CARES Social Events Simon Peyton Jones Microsoft, UK, Xinyu Feng Nanjing University

18:30 - 19:00	SRC Finalist PresentationStudent Research Competition at Student Research Competition

18:30 30m Talk		SRC Finalist Presentation Student Research Competition

19:00 - 20:45	Session 4Research Papers at ICFP Talks +12h Watch it on YouTube: https://youtu.be/vZ8X-Rx7apg Watch it on Bilibili: https://www.bilibili.com/video/BV1Eh411i7hq/

19:00 15m Talk		How to design co-programs (JFP Presentation) Research Papers Jeremy Gibbons Department of Computer Science, University of Oxford Link to publication DOI Media Attached
19:15 15m Talk		A Theory of Higher-Order Subtyping with Type Intervals Research Papers Sandro Stucki Chalmers \| University of Gothenburg, Paolo G. Giarrusso Delft University of Technology DOI Pre-print Media Attached
19:30 15m Talk		Typed dataspace actors (JFP Presentation) Research Papers Sam Caldwell Northeastern University, Tony Garnock-Jones Northeastern University, USA, Matthias Felleisen Northeastern University Link to publication DOI Media Attached
19:45 15m Talk		An Existential Crisis Resolved: Type Inference for First-Class Existential TypesDistinguished Paper Research Papers Richard A. Eisenberg Tweag, Guillaume Duboc ENS Lyon, Stephanie Weirich University of Pennsylvania, Daniel Lee DOI Media Attached
20:00 15m Talk		Proof-directed program transformation: A functional account of efficient regular expression matching (JFP Presentation) Research Papers Andrzej Filinski DIKU, University of Copenhagen Link to publication DOI Media Attached
20:15 15m Talk		Distributing Intersection and Union Types with Splits and Duality (Functional Pearl) Research Papers Xuejing Huang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong DOI Pre-print Media Attached
20:30 15m Talk		Leibniz equality is isomorphic to Martin-Löf identity, parametrically (JFP Presentation) Research Papers Dominique Devriese Vrije Universiteit Brussel, Andreas Abel Gothenburg University, Jesper Cockx TU Delft, Amin Timany Aarhus University, Philip Wadler University of Edinburgh Link to publication DOI Media Attached

19:15 - 21:00	Q&A 4Research Papers at ICFP Q&A +12h

19:15 15m Live Q&A		Q&A: How to design co-programs (JFP Presentation)Both Research Papers
19:30 15m Live Q&A		Q&A: A Theory of Higher-Order Subtyping with Type IntervalsBoth Research Papers
19:45 15m Live Q&A		Q&A: Typed dataspace actors (JFP Presentation)Both Research Papers
20:00 15m Live Q&A		Q&A: An Existential Crisis Resolved: Type Inference for First-Class Existential TypesBoth Research Papers
20:15 15m Live Q&A		Q&A: Proof-directed program transformation: A functional account of efficient regular expression matching (JFP Presentation)Both Research Papers
20:30 15m Live Q&A		Q&A: Distributing Intersection and Union Types with Splits and Duality (Functional Pearl)Both Research Papers
20:45 15m Live Q&A		Q&A: Leibniz equality is isomorphic to Martin-Löf identity, parametrically (JFP Presentation)Both Research Papers

21:00 - 21:30	PLTeaPLTea at PLTea +12h

21:00 30m Talk		PLTea PLTea

21:30 - 22:00	Ask Me AnythingSocial Events at Social Chair(s): Kihong Heo KAIST

21:30 30m Live Q&A		Ask Me Anything on Academic Move with José Pedro Magalhães Social Events José Pedro Magalhães Standard Chartered Bank

22:00 - 23:00	Keynote 2Research Papers at Keynotes

22:00 60m Keynote		Building PL-Powered Systems for Humans Research Papers Elena Glassman Harvard University

23:00 - 00:00	Virtual DinnerSocial Events at Social

23:00 60m Dinner		Virtual Dinner Social Events

Wed 25 Aug
Displayed time zone: Seoul change

03:00 - 04:00	Virtual LunchSocial Events at Social

03:00 60m Lunch		Virtual Lunch Social Events

04:00 - 05:30	Session 3Research Papers at ICFP Talks Watch it on YouTube: https://youtu.be/AGBR7RX86uE

04:00 15m Talk		Modular, Compositional, and Executable Formal Semantics for LLVM IR Research Papers Yannick Zakowski Inria, Calvin Beck University of Pennsylvania, Irene Yoon University of Pennsylvania, Ilya Zaichuk Taras Shevchenko National University of Kyiv, Vadim Zaliva University of Cambridge, UK, Steve Zdancewic University of Pennsylvania DOI Media Attached
04:15 15m Talk		Higher-Order Probabilistic Adversarial Computations: Categorical Semantics and Program Logics Research Papers Alejandro Aguirre Aarhus University, Gilles Barthe MPI-SP; IMDEA Software Institute, Marco Gaboardi Boston University, Deepak Garg MPI-SWS, Shin-ya Katsumata National Institute of Informatics, Tetsuya Sato Tokyo Institute of Technology DOI Media Attached
04:30 15m Talk		How to Evaluate Blame for Gradual Types Research Papers Lukas Lazarek Northwestern University, Ben Greenman Brown University, Matthias Felleisen Northeastern University, Christos Dimoulas PLT @ Northwestern University DOI Media Attached
04:45 15m Talk		ProbNV: Probabilistic Verification of Network Control Planes Research Papers Nick Giannarakis University of Wisconsin-Madison, Alexandra Silva University College London, David Walker Princeton University DOI Media Attached
05:00 15m Talk		Of JavaScript AOT Compilation Performance Research Papers Manuel Serrano Inria, France DOI Media Attached
05:15 15m Talk		Symbolic and Automatic Differentiation of Languages Research Papers Conal Elliott n.n. DOI Media Attached

04:15 - 05:45	Q&A 3Research Papers at ICFP Q&A

04:15 15m Live Q&A		Q&A: Modular, Compositional, and Executable Formal Semantics for LLVM IRBoth Research Papers
04:30 15m Live Q&A		Q&A: Higher-Order Probabilistic Adversarial Computations: Categorical Semantics and Program LogicsBoth Research Papers
04:45 15m Live Q&A		Q&A: How to Evaluate Blame for Gradual TypesMirror Research Papers
05:00 15m Live Q&A		Q&A: ProbNV: Probabilistic Verification of Network Control PlanesMirror Research Papers
05:15 15m Live Q&A		Q&A: Of JavaScript AOT Compilation PerformanceMain Research Papers
05:30 15m Live Q&A		Q&A: Symbolic and Automatic Differentiation of LanguagesMirror Research Papers

06:00 - 06:30	PLTeaPLTea at PLTea

06:00 30m Talk		PLTea PLTea

06:30 - 07:00	SIGPLAN CARESSocial Events at CARES

06:30 30m Meeting		SIGPLAN CARES Social Events Stephanie Weirich University of Pennsylvania, Alexandra Silva University College London

06:30 - 07:00	Ask Me AnythingSocial Events at Social Chair(s): Chung-Kil Hur Seoul National University

06:30 30m Live Q&A		Ask Me Anything on Coq with Adam Chlipala Social Events Adam Chlipala Massachusetts Institute of Technology

07:00 - 08:45	Session 4Research Papers at ICFP Talks Watch it on YouTube: https://youtu.be/_Paix-e_6eE

07:00 15m Talk		How to design co-programs (JFP Presentation) Research Papers Jeremy Gibbons Department of Computer Science, University of Oxford Link to publication DOI Media Attached
07:15 15m Talk		A Theory of Higher-Order Subtyping with Type Intervals Research Papers Sandro Stucki Chalmers \| University of Gothenburg, Paolo G. Giarrusso Delft University of Technology DOI Pre-print Media Attached
07:30 15m Talk		Typed dataspace actors (JFP Presentation) Research Papers Sam Caldwell Northeastern University, Tony Garnock-Jones Northeastern University, USA, Matthias Felleisen Northeastern University Link to publication DOI Media Attached
07:45 15m Talk		An Existential Crisis Resolved: Type Inference for First-Class Existential TypesDistinguished Paper Research Papers Richard A. Eisenberg Tweag, Guillaume Duboc ENS Lyon, Stephanie Weirich University of Pennsylvania, Daniel Lee DOI Media Attached
08:00 15m Talk		Proof-directed program transformation: A functional account of efficient regular expression matching (JFP Presentation) Research Papers Andrzej Filinski DIKU, University of Copenhagen Link to publication DOI Media Attached
08:15 15m Talk		Distributing Intersection and Union Types with Splits and Duality (Functional Pearl) Research Papers Xuejing Huang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong DOI Pre-print Media Attached
08:30 15m Talk		Leibniz equality is isomorphic to Martin-Löf identity, parametrically (JFP Presentation) Research Papers Dominique Devriese Vrije Universiteit Brussel, Andreas Abel Gothenburg University, Jesper Cockx TU Delft, Amin Timany Aarhus University, Philip Wadler University of Edinburgh Link to publication DOI Media Attached

07:15 - 09:00	Q&A 4Research Papers at ICFP Q&A

07:15 15m Live Q&A		Q&A: How to design co-programs (JFP Presentation)Both Research Papers
07:30 15m Live Q&A		Q&A: A Theory of Higher-Order Subtyping with Type IntervalsBoth Research Papers
07:45 15m Live Q&A		Q&A: Typed dataspace actors (JFP Presentation)Both Research Papers
08:00 15m Live Q&A		Q&A: An Existential Crisis Resolved: Type Inference for First-Class Existential TypesBoth Research Papers
08:15 15m Live Q&A		Q&A: Proof-directed program transformation: A functional account of efficient regular expression matching (JFP Presentation)Both Research Papers
08:30 15m Live Q&A		Q&A: Distributing Intersection and Union Types with Splits and Duality (Functional Pearl)Both Research Papers
08:45 15m Live Q&A		Q&A: Leibniz equality is isomorphic to Martin-Löf identity, parametrically (JFP Presentation)Both Research Papers

09:00 - 09:30	PLTeaPLTea at PLTea

09:00 30m Talk		PLTea PLTea

09:30 - 10:30	PL Trivia GameSocial Events at Social

09:30 60m Social Event		PL Trivia Game Social Events

16:00 - 17:30	Session 5Research Papers at ICFP Talks +12h Watch it on YouTube: https://youtu.be/YfgRUHbn4Tc Watch it on Bilibili: https://www.bilibili.com/video/BV1g44y1k7uR/

16:00 15m Talk		On Continuation-Passing Transformations and Expected Cost Analysis Research Papers Martin Avanzini Inria, Gilles Barthe MPI-SP; IMDEA Software Institute, Ugo Dal Lago University of Bologna, Italy / Inria, France DOI Media Attached
16:15 15m Talk		Steel: Proof-Oriented Programming in a Dependently Typed Concurrent Separation Logic Research Papers Aymeric Fromherz Carnegie Mellon University, Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research, Sydney Gibson Carnegie Mellon University, Guido Martínez CIFASIS-CONICET, Argentina, Denis Merigoux INRIA, Tahina Ramananandro Microsoft Research DOI Media Attached
16:30 15m Talk		Automatic Amortized Resource Analysis with the Quantum Physicist’s Method Research Papers David M. Kahn Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University DOI Media Attached
16:45 15m Talk		Theorems for Free from Separation Logic SpecificationsDistinguished Paper Research Papers Lars Birkedal Aarhus University, Thomas Dinsdale-Young Concordium, Armaël Guéneau Aarhus University, Guilhem Jaber University of Nantes, Kasper Svendsen Uber, Nikos Tzevelekos Queen Mary University of London DOI Pre-print Media Attached
17:00 15m Talk		Reasoning about the Garden of Forking Paths Research Papers Yao Li University of Pennsylvania, Li-yao Xia University of Pennsylvania, Stephanie Weirich University of Pennsylvania DOI Pre-print Media Attached
17:15 15m Talk		Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model Research Papers Glen Mével Inria; University of Paris-Saclay; CNRS; ENS Paris-Saclay; LMF, Jacques-Henri Jourdan Universersité Paris Saclay, CNRS, LRI DOI Media Attached

16:15 - 17:45	Q&A 5Research Papers at ICFP Q&A +12h

16:15 15m Live Q&A		Q&A: On Continuation-Passing Transformations and Expected Cost AnalysisBoth Research Papers
16:30 15m Live Q&A		Q&A: Steel: Proof-Oriented Programming in a Dependently Typed Concurrent Separation LogicBoth Research Papers
16:45 15m Live Q&A		Q&A: Automatic Amortized Resource Analysis with the Quantum Physicist‚Äôs MethodMirror Research Papers
17:00 15m Live Q&A		Q&A: Theorems for Free from Separation Logic SpecificationsBoth Research Papers
17:15 15m Live Q&A		Q&A: Reasoning about the Garden of Forking PathsBoth Research Papers
17:30 15m Live Q&A		Q&A: Formal Verification of a Concurrent Bounded Queue in a Weak Memory ModelBoth Research Papers

18:00 - 18:30	PLTeaPLTea at PLTea +12h

18:00 30m Talk		PLTea PLTea

18:30 - 19:00	Ask Me AnythingSocial Events at Social Chair(s): Woosuk Lee Hanyang University

18:30 30m Live Q&A		Ask Me Anything on V8 JS Engine with Ben Titzer and Toon Verwaest Social Events Ben L. Titzer Independent Consultant, Toon Verwaest Google

19:00 - 20:45	Session 6Research Papers at ICFP Talks +12h Watch it on YouTube: https://youtu.be/_m6WRM6nK_0 Watch it on Bilibili: https://www.bilibili.com/video/BV1my4y1V71V/

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

19:15 - 21:00	Q&A 6Research Papers at ICFP Q&A +12h

19:15 15m Live Q&A		Q&A: Newly-Single and Loving It: Improving Higher-Order Must-Alias Analysis with Heap FragmentsMirror Research Papers
19:30 15m Live Q&A		Q&A: Grafs: Declarative Graph AnalyticsMirror Research Papers
19:45 15m Live Q&A		Q&A: Certifying the Synthesis of Heap-Manipulating ProgramsBoth Research Papers
20:00 15m Live Q&A		Q&A: Skipping the Binder Bureaucracy with Mixed Embeddings in a Semantics Course (Functional Pearl)Both Research Papers
20:15 15m Live Q&A		Q&A: GhostCell: Separating Permissions from Data in RustBoth Research Papers
20:30 15m Live Q&A		Q&A: Catala: A Programming Language for the LawBoth Research Papers
20:45 15m Live Q&A		Q&A: Persistent Software Transactional Memory in HaskellMain Research Papers

21:00 - 21:30	PLTeaPLTea at PLTea +12h

21:00 30m Talk		PLTea PLTea

21:30 - 23:00	Awards & ReportsResearch Papers at Keynotes Chair(s): Sukyoung Ryu KAIST

21:30 45m Talk		Programming Contest Report Research Papers Jasper Van der Jeugt Fugue, Alex Lang
22:15 45m Talk		Award Presentations & Chair Report Research Papers Sukyoung Ryu KAIST

23:00 - 00:00	Industrial ReceptionSocial Events at Social

23:00 60m Social Event		Industrial Reception Social Events

Thu 26 Aug
Displayed time zone: Seoul change

00:00 - 01:00	Virtual DinnerSocial Events at Social

00:00 60m Dinner		Virtual Dinner Social Events

01:30 - 02:00	BloombergSocial Events at Social

01:30 30m Social Event		Automated Modernization of Fortran Code at Bloomberg Social Events Jason Xu

03:00 - 04:00	Virtual LunchSocial Events at Social

03:00 60m Lunch		Virtual Lunch Social Events

04:00 - 05:30	Session 5Research Papers at ICFP Talks Watch it on YouTube: https://youtu.be/3Kkc73ui7Ag

04:00 15m Talk		On Continuation-Passing Transformations and Expected Cost Analysis Research Papers Martin Avanzini Inria, Gilles Barthe MPI-SP; IMDEA Software Institute, Ugo Dal Lago University of Bologna, Italy / Inria, France DOI Media Attached
04:15 15m Talk		Steel: Proof-Oriented Programming in a Dependently Typed Concurrent Separation Logic Research Papers Aymeric Fromherz Carnegie Mellon University, Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research, Sydney Gibson Carnegie Mellon University, Guido Martínez CIFASIS-CONICET, Argentina, Denis Merigoux INRIA, Tahina Ramananandro Microsoft Research DOI Media Attached
04:30 15m Talk		Automatic Amortized Resource Analysis with the Quantum Physicist’s Method Research Papers David M. Kahn Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University DOI Media Attached
04:45 15m Talk		Theorems for Free from Separation Logic SpecificationsDistinguished Paper Research Papers Lars Birkedal Aarhus University, Thomas Dinsdale-Young Concordium, Armaël Guéneau Aarhus University, Guilhem Jaber University of Nantes, Kasper Svendsen Uber, Nikos Tzevelekos Queen Mary University of London DOI Pre-print Media Attached
05:00 15m Talk		Reasoning about the Garden of Forking Paths Research Papers Yao Li University of Pennsylvania, Li-yao Xia University of Pennsylvania, Stephanie Weirich University of Pennsylvania DOI Pre-print Media Attached
05:15 15m Talk		Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model Research Papers Glen Mével Inria; University of Paris-Saclay; CNRS; ENS Paris-Saclay; LMF, Jacques-Henri Jourdan Universersité Paris Saclay, CNRS, LRI DOI Media Attached

04:15 - 05:45	Q&A 5Research Papers at ICFP Q&A

04:15 15m Live Q&A		Q&A: On Continuation-Passing Transformations and Expected Cost AnalysisBoth Research Papers
04:30 15m Live Q&A		Q&A: Steel: Proof-Oriented Programming in a Dependently Typed Concurrent Separation LogicBoth Research Papers
04:45 15m Live Q&A		Q&A: Automatic Amortized Resource Analysis with the Quantum Physicist‚Äôs MethodMirror Research Papers
05:00 15m Live Q&A		Q&A: Theorems for Free from Separation Logic SpecificationsBoth Research Papers
05:15 15m Live Q&A		Q&A: Reasoning about the Garden of Forking PathsBoth Research Papers
05:30 15m Live Q&A		Q&A: Formal Verification of a Concurrent Bounded Queue in a Weak Memory ModelBoth Research Papers

06:00 - 06:30	PLTeaPLTea at PLTea

06:00 30m Talk		PLTea PLTea

06:30 - 07:00	Ask Me AnythingSocial Events at Social Chair(s): Hanneli Tavante McGill University

06:30 30m Live Q&A		Ask Me Anything on Mentoring with Talia Ringer Social Events Talia Ringer University of Illinois at Urbana-Champaign

07:00 - 08:45	Session 6Research Papers at ICFP Talks Watch it on YouTube: https://youtu.be/Yn1WC-mCBUc

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

07:15 - 09:00	Q&A 6Research Papers at ICFP Q&A

07:15 15m Live Q&A		Q&A: Newly-Single and Loving It: Improving Higher-Order Must-Alias Analysis with Heap FragmentsMirror Research Papers
07:30 15m Live Q&A		Q&A: Grafs: Declarative Graph AnalyticsMirror Research Papers
07:45 15m Live Q&A		Q&A: Certifying the Synthesis of Heap-Manipulating ProgramsBoth Research Papers
08:00 15m Live Q&A		Q&A: Skipping the Binder Bureaucracy with Mixed Embeddings in a Semantics Course (Functional Pearl)Both Research Papers
08:15 15m Live Q&A		Q&A: GhostCell: Separating Permissions from Data in RustBoth Research Papers
08:30 15m Live Q&A		Q&A: Catala: A Programming Language for the LawBoth Research Papers
08:45 15m Live Q&A		Q&A: Persistent Software Transactional Memory in HaskellMain Research Papers

09:00 - 09:30	PLTeaPLTea at PLTea

09:00 30m Talk		PLTea PLTea

18:00 - 19:30	Semantics & VerificationML at ML Chair(s): Martin Elsman University of Copenhagen, Denmark

18:00 30m Talk		Composing UNIX with Effect Handlers: A Case Study in Effect Handler Oriented Programming ML Daniel Hillerström The University of Edinburgh Pre-print Media Attached
18:30 30m Talk		Cameleer: a Deductive Verification Tool for OCaml ML Mário Pereira NOVA LINCS & DI -- Nova School of Science and Technology, António Ravara Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS File Attached
19:00 30m Talk		Hobbit: A Tool for Contextual Equivalence Checking Using Bisimulation Up-to Techniques ML Vasileios Koutavas Trinity College Dublin, Yu-Yang Lin Trinity College Dublin, Nikos Tzevelekos Queen Mary University of London File Attached

20:00 - 21:30	Session 1Erlang at Erlang

20:00 10m Day opening		Welcome Erlang Stavros Aronis Erlang Solutions, Sweden, Annette Bieniusa Technische Universität Kaiserslautern
20:10 30m Talk		Graft: General Purpose Raft Consensus in Elixir Erlang Matthew Alan Le Brun University of Malta, Duncan Paul Attard University of Malta, Adrian Francalanza University of Malta DOI
20:40 30m Talk		Makina: A New QuickCheck State Machine Library Erlang Luis Eduardo Bueso de Barrio Universidad Politécnica de Madrid, Lars-Åke Fredlund Universidad Politécnica de Madrid, Ángel Herranz Universidad Politécnica de Madrid, Clara Benac Earle Universidad Politécnica de Madrid, Julio Mariño Universidad Politécnica de Madrid DOI
21:10 10m Vision and Emerging Results		Lightning Talk: Expected Application of BeamAsm Erlang Susumu Yamazaki Univ. of Kitakyushu
21:20 10m Vision and Emerging Results		Lightning Talk: QuadBlockQuiz – Supply Chain Edition Erlang Duncan Sparrell sFractal Consulting

20:00 - 21:30	Paper Session 1Haskell at Haskell

20:00 30m Talk		Chesskell: A Two-Player Game at the Type Level Haskell Toby Bailey University of Warwick, Michael Gale University of Warwick, UK
20:30 30m Talk		Express: applications of dynamically typed Haskell expressions Haskell Rudy Matela Unaffiliated Link to publication DOI Pre-print
21:00 30m Talk		Haskell⁻¹: Automatic Function Inversion in Haskell Haskell Finn Teegen University of Kiel, Germany, Kai-Oliver Prott University of Kiel, Germany, Niels Bunkenburg University of Kiel, Germany DOI Pre-print

20:00 - 21:30	Compiler & Language CorrectnessML at ML Chair(s): Robert Atkey University of Strathclyde

20:00 30m Talk		Formalizing OCaml GADT typing in Coq ML Jacques Garrigue Nagoya University, Xuanrui Qi Nagoya University Pre-print File Attached
20:30 30m Talk		Demo Paper : Coqlex, an approach to generate verified lexers ML Wendlasida Ouedraogo Siemens Mobility & Inria Saclay, Danko Ilik Siemens Mobility, Lutz Strassburger Inria Saclay & LIX, Ecole Polytechnique Media Attached File Attached
21:00 30m Talk		Code Extraction from Coq to ML-like languages ML Danil Annenkov Concordium Blockchain Research Center, Aarhus University, Mikkel Milo Concordium Blockchain Research Center, Aarhus University, Bas Spitters Aarhus University Link to publication File Attached

20:00 - 21:30	Session AminiKanren at miniKanren Chair(s): William E. Byrd University of Alabama at Birmingham, USA

20:00 5m Day opening		Opening Remarks miniKanren
20:05 30m Paper		A Complexity Study for Interleaving Search miniKanren Dmitry Rozplokhas , Dmitri Boulytchev Saint Petersburg State University / JetBrains Research Pre-print Media Attached
20:35 30m Paper		metaKanren: Towards a Metacircular Relational Interpreter miniKanren Bharathi Ramana Joshi IIIT Hyderabad, William E. Byrd University of Alabama at Birmingham, USA Pre-print Media Attached
21:05 25m Paper		A New Higher-order Unification Algorithm for λKanren miniKanren Weixi Ma , Daniel P. Friedman Indiana University, USA Pre-print Media Attached

22:00 - 23:30	KeynoteErlang at Erlang

22:00 60m Keynote		Fifteen Years of Successfully Dialyzing Erlang and Elixir Code (Keynote) Erlang Konstantinos (Kostis) Sagonas Uppsala University, Sweden
23:00 10m Vision and Emerging Results		Lightning Talk: Using Regular Expressions in Erlang Erlang Kosorukov Anatolii
23:10 10m Vision and Emerging Results		Lightning Talk: eigr.io — A Serverless Runtime on the BEAM Erlang Marcel Lanz eigr.io – Member

22:00 - 23:30	Keynote 1Haskell at Haskell Chair(s): Jurriaan Hage Utrecht University, Netherlands

22:00 90m Keynote		Why Functional Programming with Linear Types Matters Haskell I: Mathieu Boespflug Tweag I/O

22:00 - 23:30	KeynoteML at ML

22:00 60m Keynote		Keynote: Narratives and Lessons from The Early History of F# ML Don Syme Microsoft

22:00 - 23:30	Morning KeynoteminiKanren at miniKanren Chair(s): Lisa Zhang University of Toronto Mississauga

22:00 60m Keynote		Adventures in extending miniKanren miniKanren Nada Amin Harvard University Media Attached

23:30 - 01:00	Session 2Erlang at Erlang

23:30 30m Talk		Detecting Oxbow Code in Erlang Codebases with the Highest Degree of Certainty Erlang Brujo Benavides Erlang Ecosystem Foundation, Laura M. Castro University of A Coruña DOI
00:00 30m Talk		Bidirectional Typing for Erlang Erlang Nithin Vadukkumchery Rajendrakumar TU Kaiserslautern, Annette Bieniusa Technische Universität Kaiserslautern DOI
00:30 10m Vision and Emerging Results		Lightning Talk: Experience teaching Erlang/Elixir on YouTube Erlang Adolfo Neto Federal University of Technology - Paraná
00:40 10m Vision and Emerging Results		Lightning Talk: AtomVM: A flyweight BEAM for microcontrollers Erlang Fred Dushin

23:30 - 01:00	Paper Session 2Haskell at Haskell

23:30 30m Talk		Design Patterns for Parser Combinators (Functional Pearl) Haskell Jamie Willis Imperial College London, Nicolas Wu Imperial College London, UK
00:00 30m Talk		Graded Monads and Type-Level Programming for Dependence Analysis Haskell Finnbar Keating University of Warwick, Michael Gale University of Warwick, UK
00:30 30m Talk		Chair Report Haskell Jurriaan Hage Utrecht University, Netherlands

23:30 - 01:00	Language & Library DesignML at ML Chair(s): Benoît Montagu Inria

23:30 30m Talk		A metalanguage for multi-phase modularity ML Jonathan Sterling Carnegie Mellon University, Robert Harper Carnegie Mellon University, USA File Attached
00:00 30m Talk		Unfolding ML datatype declarations without loops ML Nicolas Chataing ENS Paris, Gabriel Scherer INRIA Saclay Pre-print Media Attached
00:30 30m Talk		Verifying Multiparty Communication Protocols using ML Type Systems ML Keigo Imai Gifu University, Rumyana Neykova Brunel University London, Nobuko Yoshida Imperial College London, Shoji Yuen Nagoya University File Attached

23:30 - 01:00	Interaction Laws of Monads and Comonads 1Tutorials at Tutorials

23:30 90m Tutorial		Interaction laws of monads and comonads Tutorials Dylan McDermott Reykjavik University, Exequiel Rivas , Tarmo Uustalu Reykjavik University Pre-print

23:30 - 01:00	Session BminiKanren at miniKanren Chair(s): Michael Ballantyne Northeastern University

23:30 30m Paper		Prolog-Style Meta-Programming miniKanren miniKanren Nada Amin Harvard University, William E. Byrd University of Alabama at Birmingham, USA, Tiark Rompf Purdue University Pre-print Media Attached
00:00 30m Paper		Guarded Fresh Goals: Dependency-Directed Introduction of Fresh Logic Variables miniKanren Evan Donahue University of Tokyo Pre-print Media Attached
00:30 30m Paper		Universal Quantification and Implication in miniKanren miniKanren Ende Jin , Gregory Rosenblatt University of Alabama at Birmingham, USA, Matthew Might University of Alabama at Birmingham \| Harvard Medical School, Lisa Zhang University of Toronto Mississauga Pre-print Media Attached

Fri 27 Aug
Displayed time zone: Seoul change

01:30 - 03:00	Session 3Erlang at Erlang

01:30 30m Talk		What Are the Critical Security Flaws in My System? Erlang Viktória Fördős Cisco Systems DOI
02:00 30m Talk		The Hera Framework for Fault-Tolerant Sensor Fusion with Erlang and GRiSP on an IoT Network Erlang Sébastien Kalbusch Université Catholique de Louvain, Vincent Verpoten Université Catholique de Louvain, Peter Van Roy Université catholique de Louvain DOI
02:30 10m Vision and Emerging Results		Lightning Talk: The debugging tool that comes with Erlang/OTP I just learned exists after many years of using Erlang Erlang Peer Stritzinger Peer Stritzinger GmbH
02:40 10m Vision and Emerging Results		More lightning talks Erlang

01:30 - 03:00	Inference + Short talks ML at ML Chair(s): Ohad Kammar University of Edinburgh

01:30 30m Talk		Frozen inference constraints for type-directed disambiguation ML Olivier Martinot INRIA, Gabriel Scherer INRIA Saclay Pre-print Media Attached
02:00 15m Talk		Experience Report: Domain Modeling with F# (short talk) ML Scott Wlaschin None Media Attached File Attached
02:15 15m Talk		Isomorphisms are back! (short talk) ML Clément Allain Inria, Gabriel Radanne Inria, Laure Gonnord University of Lyon & LIP, France File Attached
02:30 15m Talk		Sylvester: Unified, typed, notation for symbolic mathematics and proofs (short talk) ML Allister Beharry None Media Attached File Attached
02:45 15m Talk		A Data-centered User Study for jsCoq (short talk) ML Hanneli Tavante McGill University File Attached

01:30 - 03:00	Interaction Laws of Monads and Comonads 2Tutorials at Tutorials

01:30 90m Tutorial		Interaction laws of monads and comonads Tutorials Dylan McDermott Reykjavik University, Exequiel Rivas , Tarmo Uustalu Reykjavik University Pre-print

01:30 - 03:00	Programming with Effect Handlers and FBIP in Koka 1Tutorials at Tutorials

01:30 90m Tutorial		Programming with Effect Handlers and FBIP in Koka Tutorials Daan Leijen Microsoft Research, Ningning Xie University of Toronto

01:30 - 03:00	Afternoon Keynote and Session CminiKanren at miniKanren Chair(s): Gregory Rosenblatt University of Alabama at Birmingham, USA

01:30 60m Keynote		Relational Content Generation miniKanren Chris Martens North Carolina State University Media Attached
02:30 25m Paper		Relational Floating-Point Arithmetic miniKanren Lucas Sandre University of Toronto Mississauga, Malaika Zaidi University of Toronto Mississauga, Lisa Zhang University of Toronto Mississauga Pre-print Media Attached
02:55 5m Day closing		Closing Remarks miniKanren

03:00 - 03:30	PLTeaPLTea at PLTea

03:00 30m Social Event		PLTea PLTea

03:30 - 05:00	Programming with Effect Handlers and FBIP in Koka 2Tutorials at Tutorials

03:30 90m Tutorial		Programming with Effect Handlers and FBIP in Koka Tutorials Daan Leijen Microsoft Research, Ningning Xie University of Toronto

16:00 - 17:30	Session 1OCaml at OCaml Chair(s): Youyou Cong Tokyo Institute of Technology

16:00 30m Talk		GopCaml: A Structural Editor for OCaml OCaml Kiran Gopinathan National University of Singapore File Attached
16:30 30m Talk		OCaml and Python: Getting the Best of Both Worlds OCaml Laurent Mazare Jane Street
17:00 30m Talk		Adapting the OCaml ecosystem for Multicore OCaml OCaml Sudha Parimala Segfault Systems, Enguerrand Decorne Tarides, Sadiq Jaffer Opsian and OCaml Labs, Tom Kelly OCaml Labs, KC Sivaramakrishnan IIT Madras File Attached

18:00 - 19:30	Welcome / Session 1FARM at FARM

18:00 30m Day opening		Welcome FARM
18:30 30m Talk		mimium: a self-extensible programming language for sound and music FARM Tomoya Matsuura Kyushu University, Kazuhiro Jo Faculty of Design, Kyushu University Link to publication DOI Pre-print
19:00 30m Talk		MidifilePerformer: a case study for chronologies FARM Juliette Chabassier Inria, Myriam Desainte-Catherine LaBRI, Jean Haury Scrime, Marin Pobel Université de Bordeaux, Bernard Serpette Inria

18:00 - 19:30	Session 2OCaml at OCaml Chair(s): Tim McGilchrist Tarides

18:00 30m Talk		Deductive Verification of Realistic OCaml Code OCaml Carlos Pinto NOVA LINCS & Universidade da Beira Interior, Portugal, Mário Pereira NOVA LINCS & DI -- Nova School of Science and Technology, Simão Melo de Sousa NOVA LINCS & Universidade da Beira Interior, Portugal
18:30 20m Talk		Parafuzz: Coverage-guided Property Fuzzing for Multicore OCaml programs OCaml Sumit Padhiyar Indian Institue Of Technology, Madras, Adharsh Kamath National Institute of Technology Karnataka, Surathkal, India, KC Sivaramakrishnan IIT Madras Media Attached File Attached
18:50 20m Talk		Wibbily Wobbly Timey Camly OCaml Di Long Li The Australian National University, Gabriel Radanne Inria
19:10 20m Talk		Leveraging Formal Specifications to Generate Fuzzing Suites OCaml Nicolas Osborne Tarides, Clément Pascutto Tarides, Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF

20:00 - 21:30	Session 2FARM at FARM

20:00 30m Talk		Temporal-Scope Grammars for Polyphonic Music Generation FARM Lukas Eibensteiner TU Wien, Martin Ilčík TU Wien, Michael Wimmer TU Wien
20:30 30m Talk		The W-calculus: A Synchronous Framework for the Verified Modelling of Digital Signal Processing Algorithms FARM Emilio Jesús Gallego Arias INRIA, Pierre Jouvelot MINES ParisTech, PSL University, Sylvain Ribstein Université Paris 7 Diderot, Dorian Desblancs École normale supérieure Paris-Saclay
21:00 30m Talk		Human-in-the-loop Program Synthesis for Live Coding FARM Mark Santolucito Barnard College, Columbia University, USA Pre-print

20:00 - 21:30	Paper Session 3Haskell at Haskell

20:00 30m Talk		Practical Normalization by Evaluation for EDSLs Haskell Nachiappan Valliappan Chalmers University of Technology, Sweden, Alejandro Russo Chalmers University of Technology, Sweden, Sam Lindley The University of Edinburgh, UK
20:30 30m Talk		Safe Mutation with Algebraic Effects Haskell Hashan Punchihewa Imperial College London, Nicolas Wu Imperial College London, UK
21:00 30m Talk		Seeking Stability by being Lazy and Shallow: Lazy and shallow instantiation is user friendly Haskell Gert-Jan Bottu KU Leuven, Richard A. Eisenberg Tweag

20:00 - 21:30	Session 3OCaml at OCaml Chair(s): Thomas Gazagnaire Tarides

20:00 30m Talk		Probabilistic resource limits, or: Programming with interrupts in OCaml OCaml Guillaume Munch-Maccagnoni Inria
20:30 20m Talk		Continuous Benchmarking for Ocaml Projects OCaml Gargi Sharma Tarides, Rizo Isrof Tarides, Magnus Skjegstad Tarides and OCaml Labs
20:50 20m Talk		A Multiverse of Glorious Documentation OCaml Lucas Pluvinage Tarides, Jonathan Ludlam University of Cambridge File Attached
21:10 20m Talk		Digodoc and Docs OCaml Mohamed Hernouf OCamlPro, Fabrice Le Fessant OCamlPro, Thomas Blanc OCamlPro, Louis Gesbert OCamlPro

20:00 - 21:30	Session AScheme at Scheme

20:00 30m Full-paper		Is Space-Efficient Polymorphic Gradual Typing Possible? Scheme Shota Ozaki , Taro Sekiyama National Institute of Informatics, Atsushi Igarashi Kyoto University, Japan Pre-print
20:30 30m Talk		Design with Blocks, Code in Text (Lightning Talk) Scheme Junya Nose Tokyo Institute of Technology, Youyou Cong Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology
21:00 30m Demonstration		GRASP: A GRAphical Scheme Programming environment (Lightning Talk) Scheme Panicz Godek

22:00 - 23:30	PerformancesFARM at FARM

22:00 20m Other		Performance: Logical Soundness FARM John Leo Halfaya Research
22:20 20m Other		Performance: Can One Hear the Shape of a Marble Drum? FARM Emiddio Vasquez
22:40 20m Other		Performance: Homotopy FARM José Miguél Fernandez ZKM

22:00 - 23:30	Keynote 2Haskell at Haskell Chair(s): Jurriaan Hage Utrecht University, Netherlands

22:00 90m Keynote		Linear Haskell, Today and Tomorrow Haskell I: Jean-Philippe Bernardy University of Gothenburg, Sweden

22:00 - 23:30	KeynoteOCaml at OCaml Chair(s): Anil Madhavapeddy University of Cambridge, UK

22:00 60m Keynote		25 years of OCaml OCaml Xavier Leroy Collège de France

22:00 - 23:30	Golden Hour Session (Invited Talk)Scheme at Scheme

22:00 60m Talk		Scheme as a framework for Deep Learning (Invited Talk) Scheme Jeffrey Mark Siskind Elmore Family School of Electrical and Computer Engineering, Purdue University

22:00 - 23:00	ShutdownPLSocial Events at Social

22:00 60m Social Event		ShutdownPL Social Events Justin Lubin University of California, Berkeley, Niki Carroll George Mason University, Alan Jeffrey Roblox, David Justo Microsoft

23:30 - 01:00	KeynoteFARM at FARM

23:30 60m Keynote		Keynote FARM Phoenix Perry

23:30 - 01:00	Paper Session 4Haskell at Haskell

23:30 30m Talk		Deadlock-Free Session Types in Linear Haskell Haskell Wen Kokke University of Edinburgh, Ornela Dardha University of Glasgow
00:00 30m Talk		Evaluating Linear Functions to Symmetric Monoidal Categories Haskell Jean-Philippe Bernardy University of Gothenburg, Sweden, Arnaud Spiwack Tweag DOI Pre-print
00:30 30m Talk		This is not really a talk, but should ensure the two talks before it are 30 min. long Haskell A: Jurriaan Hage Utrecht University, Netherlands

23:30 - 01:00	Session 4OCaml at OCaml Chair(s): Raja Boujbel OCamlPro

23:30 30m Talk		Experiences with Effects OCaml Thomas Leonard OCaml Labs, Craig Ferguson Tarides, Patrick Ferris OCaml Labs, Sadiq Jaffer Opsian and OCaml Labs, Tom Kelly OCaml Labs, KC Sivaramakrishnan IIT Madras, Anil Madhavapeddy University of Cambridge, UK File Attached
00:00 30m Talk		Opam-bin: Binary Packages with Opam OCaml Fabrice Le Fessant OCamlPro File Attached
00:30 30m Talk		Love: a readable language interpreted by a blockchain OCaml Steven de Oliveira OCamlPro, David Declerck OCamlPro

23:30 - 01:00	Session BScheme at Scheme

23:30 30m Talk		Adding AD to Scheme by Differentiating the Interpreter Scheme Mehrdad Maleki Mastercard Labs, Barak A. Pearlmutter Maynooth University, Jeffrey Mark Siskind Elmore Family School of Electrical and Computer Engineering, Purdue University
00:00 30m Talk		A lightweight approach for accessing Python modules from Gambit Scheme (Lightning Talk) Scheme Marc-André Bélanger Université de Montréal, Marc Feeley Université de Montréal
00:30 30m Talk		Graphite: A Library for Data Visualization (Lightning Talk) Scheme Hazel Levine Indiana University, Sam Tobin-Hochstadt Indiana University

23:30 - 01:00	Functional Software Architecture 1Tutorials at Tutorials

23:30 90m Tutorial		Functional Software Architecture Tutorials Michael Sperber Active Group GmbH

Sat 28 Aug
Displayed time zone: Seoul change

01:30 - 03:00	Session 5OCaml at OCaml Chair(s): Ashish Agarwal

01:30 30m Talk		From 2n+1 to n OCaml Nandor Licker University of Cambridge, Timothy M. Jones University of Cambridge, UK File Attached
02:00 20m Talk		Property-Based Testing for OCaml through Coq OCaml Paaras Bhandari University of Maryland, College Park, Leonidas Lampropoulos University of Maryland, College Park
02:20 20m Talk		Safe Protocol Updates via Propositional Logic OCaml Michael O'Connor Jane Street

01:30 - 03:00	Session CScheme at Scheme

01:30 30m Full-paper		Scheduling Musical Events in Max/MSP with Scheme For Max Scheme Iain Duncan University of Victoria Pre-print
02:00 30m Full-paper		So You Want To Analyze Scheme Programs With Datalog? Scheme Davis Silverman Syracuse University, USA, Yihao Sun Syracuse University, Kristopher Micinski Syracuse University, Thomas Gilray University of Alabama at Birmingham Pre-print
02:30 30m Full-paper		Prototypes: Object-Orientation, Functionally Scheme François-René Rideau Mutual Knowledge Systems, Inc., Alex Knauth Mutual Knowledge Systems, Inc., Nada Amin Harvard University Pre-print

01:30 - 03:00	Functional Software Architecture 2Tutorials at Tutorials

01:30 90m Tutorial		Functional Software Architecture Tutorials Michael Sperber Active Group GmbH

03:00 - 03:30	PLTeaPLTea at PLTea

03:00 30m Social Event		PLTea PLTea

03:30 - 05:00	Session 6OCaml at OCaml Chair(s): Rudi Grinberg OCaml Labs

03:30 30m Talk		Binary Analysis Platform (BAP). Using Universal Algebra and Tagless-Final Style for Developing Representation-Agnostic Frameworks OCaml Ivan Gotovchits Carnegie Mellon University, David Brumley Carnegie Mellon University File Attached
04:00 20m Talk		Semgrep, a fast, lightweight, polyglot, static analysis tool to find bugs OCaml Yoann Padioleau Return to Corp File Attached

03:30 - 05:00	Session DScheme at Scheme

03:30 30m Talk		Large Scheme: 'Tis Seven Years Since (Invited Talk) Scheme John Cowan R7RS Editor
04:00 60m Talk		Layering: The Architecture of Programs (Invited Talk) Scheme Gerald Jay Sussman MIT

ICFP 2021 Program

Sun 22 Aug
Displayed time zone: Seoul change

Mon 23 Aug
Displayed time zone: Seoul change

Tue 24 Aug
Displayed time zone: Seoul change

Wed 25 Aug
Displayed time zone: Seoul change

Thu 26 Aug
Displayed time zone: Seoul change

Fri 27 Aug
Displayed time zone: Seoul change

Sat 28 Aug
Displayed time zone: Seoul change

Tracks

Workshops

Co-hosted Symposia

ICFP 2021 Program

Switch Program View

Program Display Configuration

Sun 22 AugDisplayed time zone: Seoul change

Mon 23 AugDisplayed time zone: Seoul change

Tue 24 AugDisplayed time zone: Seoul change

Wed 25 AugDisplayed time zone: Seoul change

Thu 26 AugDisplayed time zone: Seoul change

Fri 27 AugDisplayed time zone: Seoul change

Sat 28 AugDisplayed time zone: Seoul change

Get Calendar (iCal)

Sun 22 Aug
Displayed time zone: Seoul change

Mon 23 Aug
Displayed time zone: Seoul change

Tue 24 Aug
Displayed time zone: Seoul change

Wed 25 Aug
Displayed time zone: Seoul change

Thu 26 Aug
Displayed time zone: Seoul change

Fri 27 Aug
Displayed time zone: Seoul change

Sat 28 Aug
Displayed time zone: Seoul change