ICFP 2021
Sun 22 - Sat 28 August 2021
Toggle navigation
Attending
Venue: Virtual
Student Volunteers
Code of Conduct
Call For Sponsorship
Registration
Accessibility
Program
ICFP Program
Your Program
Filter by Day
Sun 22 Aug
Mon 23 Aug
Tue 24 Aug
Wed 25 Aug
Thu 26 Aug
Fri 27 Aug
Sat 28 Aug
Tracks
ICFP 2021
JFP Talks
PLTea
Research Papers
Social Events
Artifact Evaluation
Student Research Competition
Workshops
Tutorials
ICFP Programming Contest
Student Volunteers
Workshops
Erlang
Erlang
- Fifteen Years of Successfully Dialyzing Erlang and Elixir Code (Keynote)
FARM
FHPNC
HIW
HOPE
ML
OCaml
PLMW @ ICFP
Scheme
TyDe
miniKanren
Co-hosted Symposia
Haskell
Organization
ICFP 2021 Committees
Organizing Committee
Steering Committee
Virtualization Committee
Track Committees
PLTea
Research Papers
Student Research Competition
Tutorials
Student Volunteers
Contributors
People Index
Workshops
Erlang
Organizing Committee
Program Committee
FARM
Organizing Committee
Program Committee
FHPNC
Organizing Committee
Program Committee
HIW
Program Committee
HOPE
Program Committee
ML
Organizing Committee
Program Committee
OCaml
Organizing Committee
Program Committee
PLMW @ ICFP
Organizing Committee
Scheme
Organizing Committee
Program Committee
TyDe
Program Committee
miniKanren
Organizing Committee
Program Committee
Co-hosted Symposia
Haskell
Program Committee
Search
Series
Series
ICFP 2025
ICFP 2024
ICFP 2023
ICFP 2022
ICFP 2021
ICFP 2020
ICFP 2019
ICFP 2018
ICFP 2017
ICFP 2016
Sign in
Sign up
ICFP 2021
(
series
) /
Virtual
/
Room information: ICFP Talks
Venue
Virtual
Room name
ICFP Talks
Room Information
No extra information available
Program
Detailed Table
Session Timeline
Detailed Timeline
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT+09:00) Seoul
.
Use conference time zone: (GMT+09:00) Seoul
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-09:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-08:00) Alaska
(GMT-07:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-07:00) Pacific Time (US & Canada)
(GMT-06:00) Mountain Time (US & Canada)
(GMT-06:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-06:00) Easter Island
(GMT-05:00) Central Time (US & Canada)
(GMT-04:00) Eastern Time (US & Canada)
(GMT-04:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-04:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-03:00) Atlantic Time (Goose Bay)
(GMT-03:00) Atlantic Time (Canada)
(GMT-02:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-02:00) Miquelon, St. Pierre
(GMT-02:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-03:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT) Azores
(UTC) Coordinated Universal Time
(GMT+01:00) Belfast
(GMT+01:00) Dublin
(GMT+01:00) Lisbon
(GMT+01:00) London
(GMT) Monrovia, Reykjavik
(GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+02:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+03:00) Athens
(GMT+03:00) Beirut
(GMT+02:00) Cairo
(GMT+03:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+03:00) Jerusalem
(GMT+03:00) Minsk
(GMT+03:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+04:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+09:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+10:00) Hobart
(GMT+10:00) Vladivostok
(GMT+10:30) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+11:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+12:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+12:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
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 program
Specify 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
Mon 23 Aug
Displayed time zone:
Seoul
change
16:00 - 17:30
Session 1
Research 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 Logic
Distinguished 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 Programming
Distinguished 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
19:00 - 20:45
Session 2
Research 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
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 1
Research Papers
at
ICFP Talks
Watch it on YouTube:
https://youtu.be/j4Lme7vLl_o
04:00
15m
Talk
Client-Server Sessions in Linear Logic
Distinguished 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 Programming
Distinguished 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
07:00 - 08:45
Session 2
Research 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
Oisín Kidney
Imperial College London
,
Nicolas Wu
Imperial College London, UK
DOI
Media Attached
16:00 - 17:30
Session 3
Research 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
19:00 - 20:45
Session 4
Research 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 Types
Distinguished 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 3
Research 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
07:00 - 08:45
Session 4
Research 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 Types
Distinguished 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
Session 5
Research 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 Specifications
Distinguished 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
Session 6
Research 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
Thu 26 Aug
Displayed time zone:
Seoul
change
04:00 - 05:30
Session 5
Research 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 Specifications
Distinguished 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 6
Research 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
Mon 23 Aug
Displayed time zone:
Seoul
change
Room
16:00
30
17:00
30
18:00
30
19:00
30
20:00
30
ICFP Talks
Research Papers
Session 1
Research Papers
Session 2
Tue 24 Aug
Displayed time zone:
Seoul
change
Room
4:00
30
5:00
30
6:00
30
7:00
30
8:00
30
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
18:00
30
19:00
30
20:00
30
ICFP Talks
Research Papers
Session 1
Research Papers
Session 2
Research Papers
Session 3
Research Papers
Session 4
Wed 25 Aug
Displayed time zone:
Seoul
change
Room
4:00
30
5:00
30
6:00
30
7:00
30
8:00
30
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
18:00
30
19:00
30
20:00
30
ICFP Talks
Research Papers
Session 3
Research Papers
Session 4
Research Papers
Session 5
Research Papers
Session 6
Thu 26 Aug
Displayed time zone:
Seoul
change
Room
4:00
30
5:00
30
6:00
30
7:00
30
8:00
30
ICFP Talks
Research Papers
Session 5
Research Papers
Session 6
Mon 23 Aug
Displayed time zone:
Seoul
change
Room
16:00
15
30
45
17:00
15
30
45
18:00
15
30
45
19:00
15
30
45
20:00
15
30
45
ICFP Talks
ICFP Research Papers
Distinguished Paper
Client-Server Sessions in Linear Logic
16:00 - 16:15
ICFP Research Papers
An Order-Aware Dataflow Model for Parallel Unix Pipelines
16:15 - 16:30
ICFP Research Papers
CPS Transformation with Affine Types for Call-By-Value Implicit Polymor ...
16:30 - 16:45
ICFP Research Papers
Distinguished Paper
Getting to the Point: Index Sets and Parallelism-Preserving Autodiff fo ...
16:45 - 17:00
ICFP Research Papers
Propositions-as-Types and Shared State
17:00 - 17:15
ICFP Research Papers
Efficient Tree-Traversals: Reconciling Parallelism and Dense Data Repre ...
17:15 - 17:30
ICFP Research Papers
Contextual Modal Types for Algebraic Effects and Handlers
19:00 - 19:15
ICFP Research Papers
Calculating Dependently-Typed Compilers (Functional Pearl)
19:15 - 19:30
ICFP Research Papers
Reasoning about Effect Interaction by Fusion
19:30 - 19:45
ICFP Research Papers
Compositional Optimizations for CertiCoq
19:45 - 20:00
ICFP Research Papers
Generalized Evidence Passing for Effect Handlers
20:00 - 20:15
ICFP Research Papers
Deriving Efficient Program Transformations from Rewrite Rules
20:15 - 20:30
ICFP Research Papers
Algebras for Weighted Search
20:30 - 20:45
Tue 24 Aug
Displayed time zone:
Seoul
change
Room
4:00
15
30
45
5:00
15
30
45
6:00
15
30
45
7:00
15
30
45
8:00
15
30
45
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
18:00
15
30
45
19:00
15
30
45
20:00
15
30
45
ICFP Talks
ICFP Research Papers
Distinguished Paper
Client-Server Sessions in Linear Logic
04:00 - 04:15
ICFP Research Papers
An Order-Aware Dataflow Model for Parallel Unix Pipelines
04:15 - 04:30
ICFP Research Papers
CPS Transformation with Affine Types for Call-By-Value Implicit Polymor ...
04:30 - 04:45
ICFP Research Papers
Distinguished Paper
Getting to the Point: Index Sets and Parallelism-Preserving Autodiff fo ...
04:45 - 05:00
ICFP Research Papers
Propositions-as-Types and Shared State
05:00 - 05:15
ICFP Research Papers
Efficient Tree-Traversals: Reconciling Parallelism and Dense Data Repre ...
05:15 - 05:30
ICFP Research Papers
Contextual Modal Types for Algebraic Effects and Handlers
07:00 - 07:15
ICFP Research Papers
Calculating Dependently-Typed Compilers (Functional Pearl)
07:15 - 07:30
ICFP Research Papers
Reasoning about Effect Interaction by Fusion
07:30 - 07:45
ICFP Research Papers
Compositional Optimizations for CertiCoq
07:45 - 08:00
ICFP Research Papers
Generalized Evidence Passing for Effect Handlers
08:00 - 08:15
ICFP Research Papers
Deriving Efficient Program Transformations from Rewrite Rules
08:15 - 08:30
ICFP Research Papers
Algebras for Weighted Search
08:30 - 08:45
ICFP Research Papers
Modular, Compositional, and Executable Formal Semantics for LLVM IR
16:00 - 16:15
ICFP Research Papers
Higher-Order Probabilistic Adversarial Computations: Categorical Semant ...
16:15 - 16:30
ICFP Research Papers
How to Evaluate Blame for Gradual Types
16:30 - 16:45
ICFP Research Papers
ProbNV: Probabilistic Verification of Network Control Planes
16:45 - 17:00
ICFP Research Papers
Of JavaScript AOT Compilation Performance
17:00 - 17:15
ICFP Research Papers
Symbolic and Automatic Differentiation of Languages
17:15 - 17:30
ICFP Research Papers
How to design co-programs (JFP Presentation)
19:00 - 19:15
ICFP Research Papers
A Theory of Higher-Order Subtyping with Type Intervals
19:15 - 19:30
ICFP Research Papers
Typed dataspace actors (JFP Presentation)
19:30 - 19:45
ICFP Research Papers
Distinguished Paper
An Existential Crisis Resolved: Type Inference for First-Class Existent ...
19:45 - 20:00
ICFP Research Papers
Proof-directed program transformation: A functional account of efficien ...
20:00 - 20:15
ICFP Research Papers
Distributing Intersection and Union Types with Splits and Duality (Func ...
20:15 - 20:30
ICFP Research Papers
Leibniz equality is isomorphic to Martin-Löf identity, parametrically ( ...
20:30 - 20:45
Wed 25 Aug
Displayed time zone:
Seoul
change
Room
4:00
15
30
45
5:00
15
30
45
6:00
15
30
45
7:00
15
30
45
8:00
15
30
45
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
18:00
15
30
45
19:00
15
30
45
20:00
15
30
45
ICFP Talks
ICFP Research Papers
Modular, Compositional, and Executable Formal Semantics for LLVM IR
04:00 - 04:15
ICFP Research Papers
Higher-Order Probabilistic Adversarial Computations: Categorical Semant ...
04:15 - 04:30
ICFP Research Papers
How to Evaluate Blame for Gradual Types
04:30 - 04:45
ICFP Research Papers
ProbNV: Probabilistic Verification of Network Control Planes
04:45 - 05:00
ICFP Research Papers
Of JavaScript AOT Compilation Performance
05:00 - 05:15
ICFP Research Papers
Symbolic and Automatic Differentiation of Languages
05:15 - 05:30
ICFP Research Papers
How to design co-programs (JFP Presentation)
07:00 - 07:15
ICFP Research Papers
A Theory of Higher-Order Subtyping with Type Intervals
07:15 - 07:30
ICFP Research Papers
Typed dataspace actors (JFP Presentation)
07:30 - 07:45
ICFP Research Papers
Distinguished Paper
An Existential Crisis Resolved: Type Inference for First-Class Existent ...
07:45 - 08:00
ICFP Research Papers
Proof-directed program transformation: A functional account of efficien ...
08:00 - 08:15
ICFP Research Papers
Distributing Intersection and Union Types with Splits and Duality (Func ...
08:15 - 08:30
ICFP Research Papers
Leibniz equality is isomorphic to Martin-Löf identity, parametrically ( ...
08:30 - 08:45
ICFP Research Papers
On Continuation-Passing Transformations and Expected Cost Analysis
16:00 - 16:15
ICFP Research Papers
Steel: Proof-Oriented Programming in a Dependently Typed Concurrent Sep ...
16:15 - 16:30
ICFP Research Papers
Automatic Amortized Resource Analysis with the Quantum Physicist’s Method
16:30 - 16:45
ICFP Research Papers
Distinguished Paper
Theorems for Free from Separation Logic Specifications
16:45 - 17:00
ICFP Research Papers
Reasoning about the Garden of Forking Paths
17:00 - 17:15
ICFP Research Papers
Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model
17:15 - 17:30
ICFP Research Papers
Newly-Single and Loving It: Improving Higher-Order Must-Alias Analysis ...
19:00 - 19:15
ICFP Research Papers
Grafs: Declarative Graph Analytics
19:15 - 19:30
ICFP Research Papers
Certifying the Synthesis of Heap-Manipulating Programs
19:30 - 19:45
ICFP Research Papers
Skipping the Binder Bureaucracy with Mixed Embeddings in a Semantics Co ...
19:45 - 20:00
ICFP Research Papers
GhostCell: Separating Permissions from Data in Rust
20:00 - 20:15
ICFP Research Papers
Catala: A Programming Language for the Law
20:15 - 20:30
ICFP Research Papers
Persistent Software Transactional Memory in Haskell
20:30 - 20:45
Thu 26 Aug
Displayed time zone:
Seoul
change
Room
4:00
15
30
45
5:00
15
30
45
6:00
15
30
45
7:00
15
30
45
8:00
15
30
45
ICFP Talks
ICFP Research Papers
On Continuation-Passing Transformations and Expected Cost Analysis
04:00 - 04:15
ICFP Research Papers
Steel: Proof-Oriented Programming in a Dependently Typed Concurrent Sep ...
04:15 - 04:30
ICFP Research Papers
Automatic Amortized Resource Analysis with the Quantum Physicist’s Method
04:30 - 04:45
ICFP Research Papers
Distinguished Paper
Theorems for Free from Separation Logic Specifications
04:45 - 05:00
ICFP Research Papers
Reasoning about the Garden of Forking Paths
05:00 - 05:15
ICFP Research Papers
Formal Verification of a Concurrent Bounded Queue in a Weak Memory Model
05:15 - 05:30
ICFP Research Papers
Newly-Single and Loving It: Improving Higher-Order Must-Alias Analysis ...
07:00 - 07:15
ICFP Research Papers
Grafs: Declarative Graph Analytics
07:15 - 07:30
ICFP Research Papers
Certifying the Synthesis of Heap-Manipulating Programs
07:30 - 07:45
ICFP Research Papers
Skipping the Binder Bureaucracy with Mixed Embeddings in a Semantics Co ...
07:45 - 08:00
ICFP Research Papers
GhostCell: Separating Permissions from Data in Rust
08:00 - 08:15
ICFP Research Papers
Catala: A Programming Language for the Law
08:15 - 08:30
ICFP Research Papers
Persistent Software Transactional Memory in Haskell
08:30 - 08:45
x
Thu 21 Nov 10:18