During the conference, the ICFP technical program will run twice—a first time starting at 9AM in New York and then a second time 12 hours later, starting at 9AM (the next day) in Beijing. To make this work, all authors have pre-recorded their talks and will participate in text-based discussion during and in live video discussion after one or both “showings” of their paper. The text chat will persist across mirrors and this video Q&A track will allow interested colleagues to get into a deep discussion right away. The videos will be freely available through a youtube livestream, but only registered ICFP participants will be able to access the text and video discussions.
The program on this track is 15-minutes delayed from the research papers track and only includes those papers where the authors have indicated their availibility.
Mon 24 AugDisplayed time zone: Eastern Time (US & Canada) change
11:45 - 13:15 | |||
11:45 30mLive Q&A | Stable Relations and Abstract Interpretation of Higher-Order Programs ICFP Q&A | ||
12:15 30mLive Q&A | Sparcl: A Language for Partially-Invertible Computation ICFP Q&A | ||
12:45 30mLive Q&A | TLC: Temporal Logic of Distributed Components ICFP Q&A |
11:45 - 13:15 | |||
12:00 30mLive Q&A | Higher-Order Demand-Driven Symbolic Evaluation ICFP Q&A | ||
12:30 30mLive Q&A | SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs ICFP Q&A | ||
13:00 30mLive Q&A | Effect Handlers, Evidently ICFP Q&A |
14:45 - 16:45 | |||
14:45 30mLive Q&A | Achieving High-Performance the Functional Way - A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies ICFP Q&A | ||
15:15 30mLive Q&A | Kindly Bent to Free Us ICFP Q&A | ||
15:45 30mLive Q&A | Effects for Efficiency: Asymptotic Speedup with First-Class Control ICFP Q&A | ||
16:15 30mLive Q&A | Retrofitting Parallelism onto OCaml ICFP Q&A |
14:45 - 16:45 | |||
15:00 30mLive Q&A | Staged Selective Parser Combinators ICFP Q&A | ||
15:30 30mLive Q&A | Sealing Pointer-Based Optimizations Behind Pure Functions ICFP Q&A | ||
16:00 30mLive Q&A | Computation Focusing ICFP Q&A | ||
16:30 30mLive Q&A | Liquid Information Flow Control ICFP Q&A |
22:45 - 00:15 | |||
23:15 30mLive Q&A | Sparcl: A Language for Partially-Invertible Computation ICFP Q&A | ||
23:45 30mLive Q&A | TLC: Temporal Logic of Distributed Components ICFP Q&A |
22:45 - 00:15 | |||
23:00 30mLive Q&A | Higher-Order Demand-Driven Symbolic Evaluation ICFP Q&A | ||
23:30 30mLive Q&A | SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs ICFP Q&A | ||
00:00 30mLive Q&A | Effect Handlers, Evidently ICFP Q&A |
Tue 25 AugDisplayed time zone: Eastern Time (US & Canada) change
02:45 - 04:45 | |||
02:45 30mLive Q&A | Achieving High-Performance the Functional Way - A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies ICFP Q&A | ||
03:15 30mLive Q&A | Kindly Bent to Free Us ICFP Q&A | ||
03:45 30mLive Q&A | Effects for Efficiency: Asymptotic Speedup with First-Class Control ICFP Q&A | ||
04:15 30mLive Q&A | Retrofitting Parallelism onto OCaml ICFP Q&A |
02:45 - 04:45 | |||
11:40 - 13:10 | |||
11:41 22mLive Q&A | A theory of RPC calculi for client–server model ICFP Q&A | ||
12:03 23mLive Q&A | Local algebraic effect theories ICFP Q&A | ||
12:26 22mLive Q&A | POPLMark reloaded: Mechanizing proofs by logical relations ICFP Q&A | ||
12:48 22mLive Q&A | Elastic Sheet-Defined Functions: Generalising Spreadsheet Functions to Variable-Size Input Arrays ICFP Q&A |
11:40 - 13:10 | |||
11:52 23mLive Q&A | The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus ICFP Q&A | ||
12:15 22mLive Q&A | Heterogeneous binary random-access lists ICFP Q&A | ||
12:37 23mLive Q&A | Perturbation confusion in forward automatic differentiation of higher-order functions ICFP Q&A |
14:45 - 16:45 | |||
14:45 30mLive Q&A | The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy (Functional Pearl) ICFP Q&A | ||
15:15 30mLive Q&A | Cosmo: A Concurrent Separation Logic for Multicore OCaml ICFP Q&A | ||
15:45 30mLive Q&A | A Quick Look at Impredicativity ICFP Q&A | ||
16:15 30mLive Q&A | Lower Your Guards: A Compositional Pattern-Match Coverage Checker ICFP Q&A |
14:45 - 16:45 | |||
15:00 30mLive Q&A | Liquid Resource Types ICFP Q&A | ||
15:30 30mLive Q&A | Composing and Decomposing Op-Based CRDTs with Semidirect Products ICFP Q&A | ||
16:00 30mLive Q&A | A Unified View of Modalities in Type Systems ICFP Q&A |
22:40 - 00:10 | |||
22:40 - 00:10 | |||
Wed 26 AugDisplayed time zone: Eastern Time (US & Canada) change
02:45 - 04:45 | |||
02:45 30mLive Q&A | The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy (Functional Pearl) ICFP Q&A | ||
03:15 30mLive Q&A | Cosmo: A Concurrent Separation Logic for Multicore OCaml ICFP Q&A | ||
03:45 30mLive Q&A | A Quick Look at Impredicativity ICFP Q&A | ||
04:15 30mLive Q&A | Lower Your Guards: A Compositional Pattern-Match Coverage Checker ICFP Q&A |
02:45 - 04:45 | |||
04:00 30mLive Q&A | A Unified View of Modalities in Type Systems ICFP Q&A | ||
04:30 30mLive Q&A | Signature restriction for polymorphic algebraic effects ICFP Q&A |
10:45 - 13:15 | |||
11:15 30mLive Q&A | Denotational Recurrence Extraction for Amortized Analysis ICFP Q&A | ||
11:45 30mLive Q&A | Strong Functional Pearl: Harper's Regular-Expression Matcher in Cedille ICFP Q&A | ||
12:15 30mLive Q&A | Recovering Purity with Comonads and Capabilities ICFP Q&A | ||
12:45 30mLive Q&A | Parsing with Zippers (Functional Pearl) ICFP Q&A |
10:45 - 13:15 | |||
11:30 30mLive Q&A | Separation Logic for Sequential Programs (Functional Pearl) ICFP Q&A | ||
12:00 30mLive Q&A | Duplo: A Framework for OCaml Post-Link Optimisation ICFP Q&A | ||
12:30 30mLive Q&A | A General Approach to Define Binders Using Matching Logic ICFP Q&A | ||
13:00 30mLive Q&A | Regular Language Type Inference with Term Rewriting ICFP Q&A |
14:45 - 16:45 | |||
14:45 30mLive Q&A | Compiling Effect Handlers in Capability-Passing Style ICFP Q&A | ||
15:15 30mLive Q&A | A dependently typed calculus with pattern matching and erasure inference ICFP Q&A | ||
15:45 30mLive Q&A | Program Sketching with Live Bidirectional Evaluation ICFP Q&A | ||
16:15 30mLive Q&A | Kinds are Calling Conventions ICFP Q&A |
14:45 - 16:45 | |||
15:00 30mLive Q&A | Scala Step-by-Step — Soundness for DOT with Step-Indexed Logical Relations in Iris ICFP Q&A | ||
15:30 30mLive Q&A | Raising Expectations: Automating Expected Cost Analysis with Types ICFP Q&A | ||
16:00 30mLive Q&A | Elaboration with First-Class Implicit Function Types ICFP Q&A |
22:45 - 00:15 | |||
22:15 30mLive Q&A | Denotational Recurrence Extraction for Amortized Analysis ICFP Q&A | ||
22:45 30mLive Q&A | Strong Functional Pearl: Harper's Regular-Expression Matcher in Cedille ICFP Q&A | ||
23:15 30mLive Q&A | Recovering Purity with Comonads and Capabilities ICFP Q&A |
22:45 - 00:15 | |||
23:30 30mLive Q&A | A General Approach to Define Binders Using Matching Logic ICFP Q&A |
Thu 27 AugDisplayed time zone: Eastern Time (US & Canada) change
02:45 - 04:45 | |||
02:45 30mLive Q&A | Compiling Effect Handlers in Capability-Passing Style ICFP Q&A | ||
03:15 30mLive Q&A | A dependently typed calculus with pattern matching and erasure inference ICFP Q&A | ||
04:15 30mLive Q&A | Kinds are Calling Conventions ICFP Q&A |
02:45 - 04:45 | |||
03:00 30mLive Q&A | Scala Step-by-Step — Soundness for DOT with Step-Indexed Logical Relations in Iris ICFP Q&A | ||
04:00 30mLive Q&A | Elaboration with First-Class Implicit Function Types ICFP Q&A |
Unscheduled Events
Not scheduled Live Q&A | Emerging languages: An alternative approach to teaching programming languages ICFP Q&A |