ICFP 2021
Sun 22 - Sat 28 August 2021
VenueVirtual
Room nameICFP Talks
Room InformationNo extra information available
Program

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

Mon 23 Aug

Displayed time zone: Seoul change

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 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
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 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

Tue 24 Aug

Displayed time zone: Seoul change

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 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
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 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
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
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

Wed 25 Aug

Displayed time zone: Seoul change

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

Thu 26 Aug

Displayed time zone: Seoul change

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
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

Mon 23 Aug

Displayed time zone: Seoul change

Room16:003017:003018:003019:003020:0030
ICFP Talks

Tue 24 Aug

Displayed time zone: Seoul change

Room4:00305:00306:00307:00308:00309:003010:003011:003012:003013:003014:003015:003016:003017:003018:003019:003020:0030
ICFP Talks

Wed 25 Aug

Displayed time zone: Seoul change

Room4:00305:00306:00307:00308:00309:003010:003011:003012:003013:003014:003015:003016:003017:003018:003019:003020:0030
ICFP Talks

Thu 26 Aug

Displayed time zone: Seoul change

Tue 24 Aug

Displayed time zone: Seoul change

Room4:001530455:001530456:001530457:001530458:001530459:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:0015304519:0015304520:00153045
ICFP Talks

Wed 25 Aug

Displayed time zone: Seoul change

Room4:001530455:001530456:001530457:001530458:001530459:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:0015304518:0015304519:0015304520:00153045
ICFP Talks