ICFP 2021
Sun 22 - Sat 28 August 2021
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

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 Hong Kong
20:00
22m
Talk
Exact Print Annotations in GHC
HIW
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 Hong Kong
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
23:52
22m
Talk
A new interface for GHC typechecker plugins and type-family rewriting
HIW
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 Hong Kong, 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

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
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
04:14
3m
Talk
Closing
HIW
Ningning Xie University of Hong Kong
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
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 Koparkar Indiana University, Mike Rainey Carnegie Mellon University, Michael Vollmer University of Kent, Milind Kulkarni Purdue University, Ryan R. Newton Facebook
DOI Media Attached
18:00 - 18:30
PLTeaPLTea at PLTea +12h
18:00
30m
Social Event
PLTea
PLTea

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

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
04:00 - 05:30
Session 1Research Papers at ICFP Talks
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 Koparkar Indiana University, Mike Rainey Carnegie Mellon University, Michael Vollmer University of Kent, Milind Kulkarni Purdue University, Ryan R. Newton Facebook
DOI Media Attached
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
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 Hong Kong, 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
Oisín Kidney Imperial College London, Nicolas Wu Imperial College London, UK
DOI Media Attached
09:00 - 09:30
PLTeaPLTea at PLTea
09:00
30m
Social Event
PLTea
PLTea

16:00 - 17:30
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
DOI Media Attached
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
18:30
30m
Talk
SRC Finalist Presentation
Student Research Competition

19:00 - 20:45
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
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
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
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
DOI Media Attached
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
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
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
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
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
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
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
22:15
45m
Talk
Award Presentations & Chair Report
Research Papers
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
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
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
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
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
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
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
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
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 Hong Kong
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 Hong Kong
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
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
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
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
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
File Attached
00:30
30m
Talk
Love: a readable language interpreted by a blockchain
OCaml
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