Conference Dates
Conference Dates are in time zone (GMT-04:00) Eastern Time (US & Canada), and may differ from the viewed time zone.
Rooms
Tracks
Badges
Your Program
Thu 20 Aug Times are displayed in time zone: Eastern Time (US & Canada) change
Thu 20 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change
| 21:00 - 22:00 Other | Clowdr Training Sessions Clowdr Training Benjamin C. PierceUniversity of Pennsylvania | ||
Fri 21 Aug Times are displayed in time zone: Eastern Time (US & Canada) change
Fri 21 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change
| 09:00 - 10:00 Other | Clowdr Training Sessions Clowdr Training Benjamin C. PierceUniversity of Pennsylvania | ||
Sun 23 Aug Times are displayed in time zone: Eastern Time (US & Canada) change
Sun 23 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change
| 07:50 - 08:00 Day opening | Opening Erlang | ||
| 08:00 - 08:30 Short-paper | Transformations towards Clean Functional Code Erlang Boldizsár PoórEötvös Loránd University, Melinda TothEötvös Loránd University, Faculty of Informatics, Department of Programming Languages and Compilers & ELTE-Soft Nonprofit Ltd., István BozóEötvös Loránd University DOI | ||
| 08:30 - 09:00 Talk | Supporting Secure Coding with RefactorErl Erlang Brigitta BaranyaiELTE Eötvös Loránd University, István BozóEötvös Loránd University, Melinda TothEötvös Loránd University, Faculty of Informatics, Department of Programming Languages and Compilers & ELTE-Soft Nonprofit Ltd. | ||
| 09:00 - 09:30 Full-paper | Teaching Practical Realistic Verification of Distributed Algorithms in Erlang with TLA+ Erlang Peter ZellerTU Kaiserslautern, Annette BieniusaTechnische Universität Kaiserslautern, Carla FerreiraUniversidade Nova Lisboa DOI | ||
| 08:00 - 09:00 Keynote | Variants of call-by-push-value HOPE Paul Blain LevyUniversity of Birmingham | ||
| 09:15 - 10:00 Talk | Kripke open relations and operational game semantics HOPE | ||
| 10:00 - 10:45 Talk | Merging coeffect production into effect handling HOPE Tarmo UustaluReykjavik University, Tallinn University of Technology, Niels VoorneveldTallinn University of Technology | ||
| 10:45 - 11:30 Talk | Simply RaTT: A Fitch-style Modal Calculus for Reactive Programming HOPE Patrick BahrIT University of Copenhagen, Christian Uldal GraulundIT University of Copenhagen, Rasmus Ejlers MøgelbergIT University of Copenhagen | ||
| 09:00 - 09:15 Day opening | Welcome PLMW @ ICFP Lindsey KuperUniversity of California, Santa Cruz, Talia RingerUniversity of Washington, Nate FosterCornell University | ||
| 09:15 - 10:00 Talk | How To Write Papers So People Can Read Them PLMW @ ICFP Derek DreyerMPI-SWS | ||
| 09:00 - 12:30 Tutorial | Teaching Functional Programming Tutorials Michael SperberActive Group GmbH | ||
| 09:00 - 12:30 Tutorial | Audio, Video & Web Live Coding in Haskell Tutorials Manuel Bärenzsonnen eServices GmbH Pre-print | ||
| 10:00 - 10:30 Talk | Practical Dependent Type Checking Using Twin Types TyDe Víctor López JuanChalmers University of Technology, Nils Anders DanielssonUniversity of Gothenburg, Chalmers University of Technology Media Attached | ||
| 10:30 - 11:00 Talk | Shallowly Embedding Type Theories as Presheaf Models in Agda (Extended Abstract) TyDe File Attached | ||
| 11:00 - 11:30 Talk | Generalization of Meta-Programs with Dependent Types in Mtac2 with Mtac2 (Extended Abstract) TyDe | ||
10:30 - 12:00: Session 2Erlang at Erlang Chair(s): Annette BieniusaTechnische Universität Kaiserslautern | |||
| 10:30 - 11:00 Full-paper | Machine-Checked Natural Semantics for Core Erlang: Exceptions and Side Effects Erlang Simon ThompsonUniversity of Kent, Dániel HorpácsiEötvös Loránd University, Péter BereczkyEötvös Loránd University DOI | ||
| 11:00 - 11:30 Full-paper | Secure Design and Verification of Erlang Systems Erlang Viktória FördősCisco Systems DOI | ||
| 11:30 - 12:00 Full-paper | Clojerl: The Expressive Power of Clojure on the BEAM Erlang DOI | ||
| 10:30 - 11:10 Talk | Constraint Solvers for the Working PL Researcher PLMW @ ICFP Nadia PolikarpovaUniversity of California, San Diego | ||
| 11:10 - 11:50 Talk | Managing your Research, your Advisor, your PhD PLMW @ ICFP Amal AhmedNortheastern University, USA | ||
| 11:50 - 12:30 Talk | Basic Mechanics of Operational Semantics PLMW @ ICFP David Van HornUniversity of Maryland, USA | ||
| 12:00 - 12:45 Talk | Higher-order Programming with Effects and Handlers — without First-Class Functions HOPE Jonathan Immanuel BrachthäuserUniversity of Tübingen, Germany, Philipp SchusterUniversity of Tübingen, Germany | ||
| 12:45 - 13:30 Talk | Towards Highly Symmetric Effects and Coeffects and a Systematic Separation between the Extra- and Intra-Logical HOPE Ingo SkupinUniversity of Tübingen, Julian JabsUniversity of Tübingen, David BinderUniversity of Tübingen File Attached | ||
12:30 - 13:30: Session 3Erlang at Erlang Chair(s): Viktória FördősCisco Systems, Annette BieniusaTechnische Universität Kaiserslautern | |||
| 12:30 - 13:30 Keynote | Living on the Edge with Erlang Erlang Peter Van RoyUniversité catholique de Louvain | ||
| 12:30 - 13:00 Talk | Graded Modal Dependent Type Theory (Extended Abstract) TyDe Benjamin MoonSchool of Computing, University of Kent, Harley D. Eades IIIAugusta University, Dominic OrchardUniversity of Kent, UK File Attached | ||
| 13:00 - 13:30 Talk | Frex: indexing modulo equations with free extensions (Extended Abstract) TyDe Guillaume AllaisUniversity of St Andrews, Edwin BradyUniversity of St. Andrews, UK, Ohad KammarUniversity of Edinburgh, Jeremy YallopUniversity of Cambridge | ||
| 13:30 - 14:00 Talk | Retrofitting Symbolic Holes to LLVM IR (Extended Abstract) TyDe Pre-print | ||
| 13:30 - 14:00 Social Event | Optional Social Activity PLMW @ ICFP | ||
| 14:00 - 15:00 Industry talk | Panel - Erlang fuelled inventions Erlang | ||
| 14:00 - 14:45 Talk | How Can I Academia When My Brain Can't Even? Mental Health in Grad School and Beyond PLMW @ ICFP Kenny FonerGalois | ||
| 14:45 - 15:30 Talk | Functional Programming for COVID-19 Drug Repurposing PLMW @ ICFP Nada AminHarvard University | ||
| 14:00 - 17:30 Tutorial | Best Practices in Code Generation Tutorials Michal J. GajdaMigamake Pte Ltd | ||
14:00 - 17:30: Designing Hardware Systems and Accelerators with Open-Source Bluespec HaskellTutorials at Tutorials 2 | |||
| 14:00 - 17:30 Tutorial | Designing Hardware Systems and Accelerators with Open-Source Bluespec Haskell Tutorials Rishiyur NikhilBluespec, Inc. | ||
| 14:30 - 15:15 Talk | Effectful Improvement Theory HOPE Martin CeresaUNR - CIFASIS - CONICET | ||
| 15:15 - 16:00 Talk | Alef: A bidirectional effect system for algebraic effects. HOPE Antonio LocascioUniversidad Nacional de Rosario | ||
| 15:30 - 16:00 Talk | Predictable Macros for Hindley-Milner (Extended Abstract) TyDe | ||
| 16:00 - 16:30 Talk | Strongly Bounded Termination with Applications to Security and Hardware Synthesis TyDe Thomas ReynoldsUniversity of Missouri, William HarrisonOak Ridge National Laboratory, Rohit ChadhaUniversity of Missouri, Gerard AllweinU.S. Naval Research Laboratory | ||
| 16:30 - 17:00 Talk | Developing a Dependently Typed Language with Runtime Proof Search (Extended Abstract) TyDe | ||
| 16:00 - 17:00 Talk | Panel discussion: Making a career in PL (even in uncertain times) PLMW @ ICFP P: Simon Peyton JonesMicrosoft, UK, P: Kathleen FisherTufts University, USA, P: Jose CalderonGalois, Inc., P: Benjamin C. PierceUniversity of Pennsylvania, P: Sarah E. ChasinsUniversity of California, Berkeley, P: Jeff VaughanGoogle | ||
Mon 24 Aug Times are displayed in time zone: Eastern Time (US & Canada) change
Mon 24 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change
| 05:00 - 06:00 Live Q&A | Jane Street 1 ICFP Sponsors | ||
| 13:30 - 14:30 Live Q&A | Jane Street 3 ICFP Sponsors | ||
09:00 - 10:00: KeynoteICFP Program at ICFP Keynote 1 Chair(s): Chung-chieh ShanIndiana University, USA | |||
| 09:00 - 10:00 Talk | Referential transparency for pandemic resilience ICFP Program | ||
| 10:00 - 11:30 Social Event | ICFP Social Time Social Events | ||
| 10:00 - 10:30 Other | Information Desk Social Events Stephanie WeirichUniversity of Pennsylvania | ||
| 10:30 - 11:30 Meeting | How to Use Clowdr at ICFP Social Events Benjamin C. PierceUniversity of Pennsylvania | ||
| 10:30 - 10:38 Poster | A GHC-Plugin to Compile Effectful Languages Student Research Competition Kai-Oliver ProttCAU Kiel | ||
| 10:38 - 10:47 Poster | Certified double sided auction mechanisms Student Research Competition Suneel sarswatTIFR | ||
| 10:47 - 10:55 Poster | Certified Optimisation of Stream Operations Using Heterogeneous Staging Student Research Competition James LowenthalUniversity of Cambridge | ||
| 10:55 - 11:04 Poster | Pattern Matching with Typed Holes Student Research Competition Yongwei YuanUniversity of Michigan | ||
| 11:04 - 11:12 Poster | Type Hole Inference Student Research Competition Zhiyi PanUniversity of Michigan | ||
| 11:12 - 11:21 Poster | Semantics for a Simple Differentiable Language Using Distribution Theory Student Research Competition Christopher LamCornell University | ||
| 11:21 - 11:30 Poster | Gradual Enforcement of IO Trace Properties Student Research Competition Cezar-Constantin AndriciAlexandru Ioan Cuza University of Iasi | ||
11:30 - 13:00: New York 1ICFP Program at ICFP NY 1 Chair(s): Adam ChlipalaMassachusetts Institute of Technology | |||
| 11:30 - 11:45 Talk | Stable Relations and Abstract Interpretation of Higher-Order Programs ICFP Program DOI Media Attached File Attached | ||
| 11:45 - 12:00 Talk | Higher-Order Demand-Driven Symbolic Evaluation ICFP Program Zachary PalmerSwarthmore College, Theodore ParkSwarthmore and Hopkins, Scott F. SmithThe Johns Hopkins University, Shiwei WengThe Johns Hopkins University DOI Media Attached | ||
| 12:00 - 12:15 Talk | Sparcl: A Language for Partially-Invertible Computation ICFP Program DOI Media Attached | ||
| 12:15 - 12:30 Talk | SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs ICFP Program Nikhil SwamyMicrosoft Research, Aseem RastogiMicrosoft Research, Aymeric FromherzCarnegie Mellon University, Denis MerigouxINRIA, Danel AhmanUniversity of Ljubljana, Guido MartínezCIFASIS-CONICET, Argentina DOI Media Attached | ||
| 12:30 - 12:45 Talk | TLC: Temporal Logic of Distributed Components ICFP Program Jeremiah GriffinUniversity of California, Riverside, Mohsen LesaniUniversity of California, Riverside, Narges ShadabUniversity of California, Riverside, Xizhe YinUnivsersity of California, Riverside DOI Media Attached | ||
| 12:45 - 13:00 Talk | Effect Handlers, Evidently ICFP Program Ningning XieMicrosoft Research, USA, Jonathan Immanuel BrachthäuserUniversity of Tübingen, Germany, Daniel HillerströmThe University of Edinburgh, Philipp SchusterUniversity of Tübingen, Germany, Daan LeijenMicrosoft Research, USA DOI Media Attached | ||
| 11:45 - 12:15 Live Q&A | Stable Relations and Abstract Interpretation of Higher-Order Programs ICFP Q&A | ||
| 12:15 - 12:45 Live Q&A | Sparcl: A Language for Partially-Invertible Computation ICFP Q&A | ||
| 12:45 - 13:15 Live Q&A | TLC: Temporal Logic of Distributed Components ICFP Q&A | ||
| 12:00 - 12:30 Live Q&A | Higher-Order Demand-Driven Symbolic Evaluation ICFP Q&A | ||
| 12:30 - 13:00 Live Q&A | SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs ICFP Q&A | ||
| 13:00 - 13:30 Live Q&A | Effect Handlers, Evidently ICFP Q&A | ||
| 13:00 - 14:30 Social Event | ICFP Social Time Social Events | ||
| 13:00 - 13:30 Other | Information Desk Social Events Stephanie WeirichUniversity of Pennsylvania | ||
13:30 - 14:30: W@ICFPSocial Events at ICFP Social YouTube recording of event: https://www.youtube.com/watch?v=2FNX9SjAwMM | |||
| 13:30 - 14:30 Social Event | W@ICFP Social Events | ||
| 14:30 - 14:45 Talk | Achieving High-Performance the Functional Way - A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies ICFP Program Bastian HagedornUniversity of Münster, Germany, Johannes LenfersUniversity of Münster, Thomas KoehlerUniversity of Glasgow, United Kingdom, Xueying QinUniversity of Glasgow, United Kingdom, Sergei GorlatchUniversity of Münster, Germany, Michel SteuwerThe University of Edinburgh DOI Media Attached | ||
| 14:45 - 15:00 Talk | Staged Selective Parser Combinators ICFP Program Jamie WillisImperial College London, Nicolas WuImperial College London, UK, Matthew PickeringUniversity of Bristol, UK DOI Media Attached | ||
| 15:00 - 15:15 Talk | Kindly Bent to Free Us ICFP Program Gabriel RadanneInria, Hannes SaffrichUniversity of Freiburg, Peter ThiemannUniversity of Freiburg, Germany DOI Pre-print Media Attached File Attached | ||
| 15:15 - 15:30 Talk | Sealing Pointer-Based Optimizations Behind Pure Functions ICFP Program Daniel SelsamMicrosoft Research, Simon HudonCarnegie Mellon University, Leonardo De MouraMicrosoft Research, n.n. DOI Media Attached | ||
| 15:30 - 15:45 Talk | Effects for Efficiency: Asymptotic Speedup with First-Class Control ICFP Program Daniel HillerströmThe University of Edinburgh, Sam LindleyHeriot-Watt University, UK / The University of Edinburgh, UK, John LongleyThe University of Edinburgh DOI Media Attached | ||
| 15:45 - 16:00 Talk | Computation Focusing ICFP Program DOI Media Attached | ||
| 16:00 - 16:15 Talk | Retrofitting Parallelism onto OCamlDistinguished Paper ICFP Program KC SivaramakrishnanIIT Madras, Stephen DolanUniversity of Cambridge, UK, Leo WhiteJane Street, Sadiq JafferOpsian and OCaml Labs, Tom KellyOCaml Labs, Anmol SahooIIT Madras, Sudha ParimalaIIT Madras, Atul DhimanIIT Madras, Anil MadhavapeddyOCaml Labs DOI Media Attached | ||
| 16:15 - 16:30 Talk | Liquid Information Flow ControlDistinguished Paper ICFP Program Nadia PolikarpovaUniversity of California, San Diego, Deian StefanUniversity of California at San Diego, USA, Jean YangCarnegie Mellon University, Shachar ItzhakyTechnion, Israel, Travis HanceCarnegie Mellon University, Armando Solar-LezamaMassachusetts Institute of Technology, USA DOI Media Attached | ||
| 14:45 - 15:15 Live Q&A | Achieving High-Performance the Functional Way - A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies ICFP Q&A | ||
| 15:15 - 15:45 Live Q&A | Kindly Bent to Free Us ICFP Q&A | ||
| 15:45 - 16:15 Live Q&A | Effects for Efficiency: Asymptotic Speedup with First-Class Control ICFP Q&A | ||
| 16:15 - 16:45 Live Q&A | Retrofitting Parallelism onto OCaml ICFP Q&A | ||
| 15:00 - 15:30 Live Q&A | Staged Selective Parser Combinators ICFP Q&A | ||
| 15:30 - 16:00 Live Q&A | Sealing Pointer-Based Optimizations Behind Pure Functions ICFP Q&A | ||
| 16:00 - 16:30 Live Q&A | Computation Focusing ICFP Q&A | ||
| 16:30 - 17:00 Live Q&A | Liquid Information Flow Control ICFP Q&A | ||
| 16:30 - 17:30 Social Event | ICFP Social Time Social Events | ||
| 16:30 - 17:30 Social Event | Untitled PL Card Game Social Events Jasper Van der JeugtFugue, Niki VazouIMDEA Software Institute, Leonidas LampropoulosUniversity of Maryland, College Park Media Attached | ||
| 21:00 - 22:00 Social Event | ICFP Social Time Social Events | ||
21:00 - 22:00: Women in CS PanelSocial Events at ICFP Social Chair(s): Cristina CifuentesOracle Labs YouTube recording of event: https://youtu.be/uHdtXFEwVCs | |||
| 21:00 - 22:00 Social Event | Women in CS Panel Social Events P: Cristina CifuentesOracle Labs, P: Sukyoung RyuKAIST, P: Alena GriffithsRGB Assurance, P: Behnaz HassanshahiOracle Labs, Australia | ||
| 22:00 - 23:00 Meeting | How to Use Clowdr at ICFP Social Events Benjamin C. PierceUniversity of Pennsylvania | ||
22:30 - 00:00: Asia 1ICFP Program at ICFP Asia 1 Chair(s): Adam ChlipalaMassachusetts Institute of Technology | |||
| 22:30 - 22:45 Talk | Stable Relations and Abstract Interpretation of Higher-Order Programs ICFP Program DOI Media Attached File Attached | ||
| 22:45 - 23:00 Talk | Higher-Order Demand-Driven Symbolic Evaluation ICFP Program Zachary PalmerSwarthmore College, Theodore ParkSwarthmore and Hopkins, Scott F. SmithThe Johns Hopkins University, Shiwei WengThe Johns Hopkins University DOI Media Attached | ||
| 23:00 - 23:15 Talk | Sparcl: A Language for Partially-Invertible Computation ICFP Program DOI Media Attached | ||
| 23:15 - 23:30 Talk | SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs ICFP Program Nikhil SwamyMicrosoft Research, Aseem RastogiMicrosoft Research, Aymeric FromherzCarnegie Mellon University, Denis MerigouxINRIA, Danel AhmanUniversity of Ljubljana, Guido MartínezCIFASIS-CONICET, Argentina DOI Media Attached | ||
| 23:30 - 23:45 Talk | TLC: Temporal Logic of Distributed Components ICFP Program Jeremiah GriffinUniversity of California, Riverside, Mohsen LesaniUniversity of California, Riverside, Narges ShadabUniversity of California, Riverside, Xizhe YinUnivsersity of California, Riverside DOI Media Attached | ||
| 23:45 - 00:00 Talk | Effect Handlers, Evidently ICFP Program Ningning XieMicrosoft Research, USA, Jonathan Immanuel BrachthäuserUniversity of Tübingen, Germany, Daniel HillerströmThe University of Edinburgh, Philipp SchusterUniversity of Tübingen, Germany, Daan LeijenMicrosoft Research, USA DOI Media Attached | ||
| 23:15 - 23:45 Live Q&A | Sparcl: A Language for Partially-Invertible Computation ICFP Q&A | ||
| 23:45 - 00:15 Live Q&A | TLC: Temporal Logic of Distributed Components ICFP Q&A | ||
| 23:00 - 23:30 Live Q&A | Higher-Order Demand-Driven Symbolic Evaluation ICFP Q&A | ||
| 23:30 - 00:00 Live Q&A | SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs ICFP Q&A | ||
| 00:00 - 00:30 Live Q&A | Effect Handlers, Evidently ICFP Q&A | ||
Tue 25 Aug Times are displayed in time zone: Eastern Time (US & Canada) change
Tue 25 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change
| 01:00 - 02:00 Social Event | ICFP Social Time Social Events | ||
| 01:00 - 02:00 Talk | Mentoring with Ranjit Jhala Social Events Ranjit JhalaUniversity of California at San Diego, USA | ||
| 02:30 - 02:45 Talk | Achieving High-Performance the Functional Way - A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies ICFP Program Bastian HagedornUniversity of Münster, Germany, Johannes LenfersUniversity of Münster, Thomas KoehlerUniversity of Glasgow, United Kingdom, Xueying QinUniversity of Glasgow, United Kingdom, Sergei GorlatchUniversity of Münster, Germany, Michel SteuwerThe University of Edinburgh DOI Media Attached | ||
| 02:45 - 03:00 Talk | Staged Selective Parser Combinators ICFP Program Jamie WillisImperial College London, Nicolas WuImperial College London, UK, Matthew PickeringUniversity of Bristol, UK DOI Media Attached | ||
| 03:00 - 03:15 Talk | Kindly Bent to Free Us ICFP Program Gabriel RadanneInria, Hannes SaffrichUniversity of Freiburg, Peter ThiemannUniversity of Freiburg, Germany DOI Pre-print Media Attached File Attached | ||
| 03:15 - 03:30 Talk | Sealing Pointer-Based Optimizations Behind Pure Functions ICFP Program Daniel SelsamMicrosoft Research, Simon HudonCarnegie Mellon University, Leonardo De MouraMicrosoft Research, n.n. DOI Media Attached | ||
| 03:30 - 03:45 Talk | Effects for Efficiency: Asymptotic Speedup with First-Class Control ICFP Program Daniel HillerströmThe University of Edinburgh, Sam LindleyHeriot-Watt University, UK / The University of Edinburgh, UK, John LongleyThe University of Edinburgh DOI Media Attached | ||
| 03:45 - 04:00 Talk | Computation Focusing ICFP Program DOI Media Attached | ||
| 04:00 - 04:15 Talk | Retrofitting Parallelism onto OCamlDistinguished Paper ICFP Program KC SivaramakrishnanIIT Madras, Stephen DolanUniversity of Cambridge, UK, Leo WhiteJane Street, Sadiq JafferOpsian and OCaml Labs, Tom KellyOCaml Labs, Anmol SahooIIT Madras, Sudha ParimalaIIT Madras, Atul DhimanIIT Madras, Anil MadhavapeddyOCaml Labs DOI Media Attached | ||
| 04:15 - 04:30 Talk | Liquid Information Flow ControlDistinguished Paper ICFP Program Nadia PolikarpovaUniversity of California, San Diego, Deian StefanUniversity of California at San Diego, USA, Jean YangCarnegie Mellon University, Shachar ItzhakyTechnion, Israel, Travis HanceCarnegie Mellon University, Armando Solar-LezamaMassachusetts Institute of Technology, USA DOI Media Attached | ||
| 02:45 - 03:15 Live Q&A | Achieving High-Performance the Functional Way - A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies ICFP Q&A | ||
| 03:15 - 03:45 Live Q&A | Kindly Bent to Free Us ICFP Q&A | ||
| 03:45 - 04:15 Live Q&A | Effects for Efficiency: Asymptotic Speedup with First-Class Control ICFP Q&A | ||
| 04:15 - 04:45 Live Q&A | Retrofitting Parallelism onto OCaml ICFP Q&A | ||
| 04:30 - 05:30 Social Event | ICFP Social Time Social Events | ||
| 04:30 - 05:30 Meeting | Online Lecture Panel Social Events Atsushi IgarashiKyoto University, Japan, Sukyoung RyuKAIST, Ilya SergeyYale-NUS College and National University of Singapore, Alex PotaninVictoria University of Wellington | ||
| 05:00 - 06:00 Live Q&A | Jane Street 1 ICFP Sponsors | ||
| 10:00 - 11:00 Live Q&A | Jane Street 2 ICFP Sponsors | ||
| 13:30 - 14:30 Live Q&A | Jane Street 3 ICFP Sponsors | ||
09:00 - 10:00: KeynoteICFP Program at ICFP Keynote 2 Chair(s): Adam ChlipalaMassachusetts Institute of Technology | |||
| 09:00 - 10:00 Talk | On Language Adoption ICFP Program | ||
| 10:00 - 10:30 Other | Information Desk Social Events Stephanie WeirichUniversity of Pennsylvania | ||
| 10:30 - 11:30 Social Event | Virtual Art Gallery Social Events Alan JeffreyMozilla Research | ||
| 10:30 - 11:00 Meeting | SIGPLAN CARES Social Events David WalkerPrinceton University, USA, Simon Peyton JonesMicrosoft, UK, Alexandra SilvaUniversity College London, Shriram KrishnamurthiBrown University, United States | ||
11:30 - 12:15: SRC Finalist Presentation 1Student Research Competition at Student Research Competition | |||
| 11:30 - 12:15 Talk | SRC Finalist Presentation 1 Student Research Competition | ||
| 11:41 - 12:03 Live Q&A | A theory of RPC calculi for client–server model ICFP Q&A | ||
| 12:03 - 12:26 Live Q&A | Local algebraic effect theories ICFP Q&A | ||
| 12:26 - 12:48 Live Q&A | POPLMark reloaded: Mechanizing proofs by logical relations ICFP Q&A | ||
| 12:48 - 13:10 Live Q&A | Elastic Sheet-Defined Functions: Generalising Spreadsheet Functions to Variable-Size Input Arrays ICFP Q&A | ||
| 11:52 - 12:15 Live 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 - 12:37 Live Q&A | Heterogeneous binary random-access lists ICFP Q&A | ||
| 12:37 - 13:00 Live Q&A | Perturbation confusion in forward automatic differentiation of higher-order functions ICFP Q&A | ||
| 13:00 - 14:30 Social Event | ICFP Social Time Social Events | ||
| 13:00 - 13:30 Other | Information Desk Social Events Stephanie WeirichUniversity of Pennsylvania | ||
| 13:30 - 14:30 Talk | LGBTQ Meetup Social Events | ||
| 14:45 - 15:15 Live Q&A | The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy (Functional Pearl) ICFP Q&A | ||
| 15:15 - 15:45 Live Q&A | Cosmo: A Concurrent Separation Logic for Multicore OCaml ICFP Q&A | ||
| 15:45 - 16:15 Live Q&A | A Quick Look at Impredicativity ICFP Q&A | ||
| 16:15 - 16:45 Live Q&A | Lower Your Guards: A Compositional Pattern-Match Coverage Checker ICFP Q&A | ||
| 15:00 - 15:30 Live Q&A | Liquid Resource Types ICFP Q&A | ||
| 15:30 - 16:00 Live Q&A | Composing and Decomposing Op-Based CRDTs with Semidirect Products ICFP Q&A | ||
| 16:00 - 16:30 Live Q&A | A Unified View of Modalities in Type Systems ICFP Q&A | ||
| 16:30 - 17:30 Social Event | ICFP Social Time Social Events | ||
| 16:30 - 17:30 Social Event | ICFP Triva Social Events | ||
| 21:00 - 22:30 Social Event | ICFP Social Time Social Events | ||
| 21:00 - 21:30 Meeting | SIGPLAN CARES Social Events David WalkerPrinceton University, USA, Simon Peyton JonesMicrosoft, UK, Alexandra SilvaUniversity College London, Shriram KrishnamurthiBrown University, United States | ||
| 21:30 - 22:30 Meeting | Mind the Title Social Events Olivier DanvyYale-NUS College and School of Computing, Singapore | ||
23:30 - 00:15: SRC Finalist Presentation 2Student Research Competition at Student Research Competition | |||
| 23:30 - 00:15 Talk | SRC Finalist Presentation 2 Student Research Competition | ||
Wed 26 Aug Times are displayed in time zone: Eastern Time (US & Canada) change
Wed 26 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change
| 00:00 - 01:00 Social Event | ICFP Social Time Social Events | ||
| 00:00 - 01:00 Talk | Mentoring with Guy Steele Social Events Guy L. Steele Jr.Oracle Labs | ||
| 02:45 - 03:15 Live Q&A | The Simple Essence of Algebraic Subtyping: Principal Type Inference with Subtyping Made Easy (Functional Pearl) ICFP Q&A | ||
| 03:15 - 03:45 Live Q&A | Cosmo: A Concurrent Separation Logic for Multicore OCaml ICFP Q&A | ||
| 03:45 - 04:15 Live Q&A | A Quick Look at Impredicativity ICFP Q&A | ||
| 04:15 - 04:45 Live Q&A | Lower Your Guards: A Compositional Pattern-Match Coverage Checker ICFP Q&A | ||
| 04:00 - 04:30 Live Q&A | A Unified View of Modalities in Type Systems ICFP Q&A | ||
| 04:30 - 05:00 Live Q&A | Signature restriction for polymorphic algebraic effects ICFP Q&A | ||
| 04:30 - 05:30 Social Event | ICFP Social Time Social Events | ||
| 04:30 - 05:30 Talk | Some Proverbs in Type Theory Social Events Neel KrishnaswamiComputer Laboratory, University of Cambridge | ||
| 05:00 - 06:00 Live Q&A | Jane Street 1 ICFP Sponsors | ||
| 10:00 - 11:00 Live Q&A | Jane Street 2 ICFP Sponsors | ||
| 13:30 - 14:30 Live Q&A | Jane Street 3 ICFP Sponsors | ||
| 16:30 - 17:30 Social Event | Jane Street at Industrial Reception ICFP Sponsors | ||
| 16:30 - 17:30 Social Event | Ahrefs at Industrial Reception ICFP Sponsors | ||
| 16:30 - 17:30 Social Event | Facebook at Industrial Reception ICFP Sponsors | ||
| 16:30 - 17:30 Social Event | Galois at Industrial Reception ICFP Sponsors | ||
09:00 - 09:45: ICFP Programming ContestICFP Program at ICFP Awards Chair(s): Stephanie WeirichUniversity of Pennsylvania | |||
| 09:00 - 09:45 Keynote | Programming Contest Report ICFP Program Igor LukaninKontur | ||
| 16:30 - 17:30 Social Event | Standard Chartered at Industrial Reception ICFP Sponsors | ||
09:45 - 10:30: Awards & ReportsICFP Program at ICFP Awards Chair(s): Stephanie WeirichUniversity of Pennsylvania | |||
| 09:45 - 10:30 Talk | Award Presentations & Chair Report ICFP Program Stephanie WeirichUniversity of Pennsylvania, Adam ChlipalaMassachusetts Institute of Technology, Mira MeziniTechnische Universität Darmstadt, Sukyoung RyuKAIST, Jens PalsbergUniversity of California, Los Angeles, Youyou CongTokyo Institute of Technology | ||
| 10:30 - 11:00 Other | Information Desk Social Events Stephanie WeirichUniversity of Pennsylvania | ||
| 11:15 - 11:45 Live Q&A | Denotational Recurrence Extraction for Amortized Analysis ICFP Q&A | ||
| 11:45 - 12:15 Live Q&A | Strong Functional Pearl: Harper's Regular-Expression Matcher in Cedille ICFP Q&A | ||
| 12:15 - 12:45 Live Q&A | Recovering Purity with Comonads and Capabilities ICFP Q&A | ||
| 12:45 - 13:15 Live Q&A | Parsing with Zippers (Functional Pearl) ICFP Q&A | ||
| 11:30 - 12:00 Live Q&A | Separation Logic for Sequential Programs (Functional Pearl) ICFP Q&A | ||
| 12:00 - 12:30 Live Q&A | Duplo: A Framework for OCaml Post-Link Optimisation ICFP Q&A | ||
| 12:30 - 13:00 Live Q&A | A General Approach to Define Binders Using Matching Logic ICFP Q&A | ||
| 13:00 - 13:30 Live Q&A | Regular Language Type Inference with Term Rewriting ICFP Q&A | ||
| 13:00 - 14:30 Social Event | ICFP Social Time Social Events | ||
| 13:00 - 13:30 Other | Information Desk Social Events Stephanie WeirichUniversity of Pennsylvania | ||
| 13:30 - 14:30 Meeting | Virtualization Feedback Social Events Benjamin C. PierceUniversity of Pennsylvania, Jonathan BellNortheastern University, Crista LopesUniversity of California, Irvine | ||
| 14:45 - 15:15 Live Q&A | Compiling Effect Handlers in Capability-Passing Style ICFP Q&A | ||
| 15:15 - 15:45 Live Q&A | A dependently typed calculus with pattern matching and erasure inference ICFP Q&A | ||
| 15:45 - 16:15 Live Q&A | Program Sketching with Live Bidirectional Evaluation ICFP Q&A | ||
| 16:15 - 16:45 Live Q&A | Kinds are Calling Conventions ICFP Q&A | ||
| 15:00 - 15:30 Live Q&A | Scala Step-by-Step — Soundness for DOT with Step-Indexed Logical Relations in Iris ICFP Q&A | ||
| 15:30 - 16:00 Live Q&A | Raising Expectations: Automating Expected Cost Analysis with Types ICFP Q&A | ||
| 16:00 - 16:30 Live Q&A | Elaboration with First-Class Implicit Function Types ICFP Q&A | ||
| 16:30 - 17:30 Social Event | Industrial Reception Social Events | ||
| 16:30 - 17:30 Social Event | Tweag at Industrial Reception ICFP Sponsors | ||
| 16:30 - 17:30 Social Event | Bloomberg at Industrial Reception ICFP Sponsors | ||
| 16:30 - 17:30 Social Event | Microsoft at Industrial Reception ICFP Sponsors | ||
| 16:30 - 17:30 Social Event | Oracle at Industrial Reception ICFP Sponsors | ||
| 21:00 - 22:00 Social Event | ICFP Social Time Social Events | ||
| 21:00 - 22:00 Meeting | Virtualization Feedback Social Events Benjamin C. PierceUniversity of Pennsylvania, Jonathan BellNortheastern University, Crista LopesUniversity of California, Irvine | ||
| 22:15 - 22:45 Live Q&A | Denotational Recurrence Extraction for Amortized Analysis ICFP Q&A | ||
| 22:45 - 23:15 Live Q&A | Strong Functional Pearl: Harper's Regular-Expression Matcher in Cedille ICFP Q&A | ||
| 23:15 - 23:45 Live Q&A | Recovering Purity with Comonads and Capabilities ICFP Q&A | ||
| 23:30 - 00:00 Live Q&A | A General Approach to Define Binders Using Matching Logic ICFP Q&A | ||
Thu 27 Aug Times are displayed in time zone: Eastern Time (US & Canada) change
Thu 27 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change
| 00:30 - 01:30 Social Event | ICFP Social Time Social Events | ||
| 00:30 - 01:30 Talk | Mentoring with Matthias Felleisen Social Events Matthias FelleisenPLT @ Northeastern University | ||
| 02:45 - 03:15 Live Q&A | Compiling Effect Handlers in Capability-Passing Style ICFP Q&A | ||
| 03:15 - 03:45 Live Q&A | A dependently typed calculus with pattern matching and erasure inference ICFP Q&A | ||
| 04:15 - 04:45 Live Q&A | Kinds are Calling Conventions ICFP Q&A | ||
| 03:00 - 03:30 Live Q&A | Scala Step-by-Step — Soundness for DOT with Step-Indexed Logical Relations in Iris ICFP Q&A | ||
| 04:00 - 04:30 Live Q&A | Elaboration with First-Class Implicit Function Types ICFP Q&A | ||
| 04:30 - 05:30 Social Event | ICFP Social Time Social Events | ||
| 09:00 - 10:00 Meeting | Academic Career Planning During a Crisis Social Events Neel KrishnaswamiComputer Laboratory, University of Cambridge | ||
09:00 - 12:30: Functional Software ArchitectureTutorials at Tutorials 1 https://www.youtube.com/watch?v=7UvauMsBtDw&feature=youtu.be | |||
| 09:00 - 12:30 Tutorial | Functional Software Architecture Tutorials Michael SperberActive Group GmbH | ||
09:00 - 12:30: Integrating User Centered Methods into Programming Language DesignTutorials at Tutorials 2 | |||
| 09:00 - 12:30 Tutorial | Integrating User-Centered Methods into Programming Language Design Tutorials | ||
09:00 - 11:00: Morning KeynoteminiKanren at miniKanren Chair(s): Dmitri BoulytchevSt. Petersburg State University, St. Petersburg, Russia | |||
| 10:00 - 11:00 Keynote | Executing Declarative Language Definitions miniKanren | ||
| 10:00 - 11:00 Keynote | Using STM for Modular Concurrency: An Industrial Experience Report on Software Transactional Memory Haskell | ||
| 10:00 - 11:00 Keynote | Verification of OCaml programs using CFML ML Arthur CharguéraudInria Media Attached | ||
11:30 - 13:00: Paper Session 1 - Software EngineeringHaskell at Haskell Chair(s): José Pedro Magalhães | |||
| 11:30 - 12:00 Talk | Assessing the Quality of Evolving Haskell Systems by Measuring Structural Inequality Haskell Sander KampsOpen University of the Netherlands, Netherlands, Bastiaan HeerenOpen University of the Netherlands, Netherlands, Johan JeuringOpen University of the Netherlands, Netherlands DOI | ||
| 12:00 - 12:30 Talk | Describing Microservices using Modern Haskell (Experience Report) Haskell DOI | ||
| 12:30 - 13:00 Talk | Towards Secure IoT Programming in Haskell Haskell Nachiappan ValliappanChalmers University of Technology, Sweden, Robert KrookChalmers University of Technology, Sweden, Alejandro RussoChalmers University of Technology, Sweden, Koen ClaessenChalmers University of Technology, Sweden DOI | ||
| 11:30 - 11:55 Talk | Tracking injectivity and nominality beyond abstraction ML Jacques GarrigueNagoya University Media Attached File Attached | ||
| 11:55 - 12:20 Talk | Quantified Applicatives – API design for type-inference constraints ML Media Attached File Attached | ||
| 12:20 - 12:45 Talk | High-level error messages for modules through diffing ML Media Attached File Attached | ||
| 12:45 - 13:10 Talk | The Virtues of Semi-Explicit Polymorphism ML Frank EmrichUniversity of Edinburgh, UK, Sam LindleyHeriot-Watt University, UK / The University of Edinburgh, UK, Jan StolarekUniversity of Edinburgh, UK Media Attached File Attached | ||
| 14:00 - 18:00 Social Event | ShutdownPL: Keynote and Getting Started With Anti-racist Action Social Events Kenny FonerGalois, Niki CarrollGeorge Mason University, Priya SrikumarCornell University, David JustoUniversity of California, San Diego, Justin LubinUniversity of Chicago, Akash Gaonkar, Alan JeffreyMozilla Research | ||
14:00 - 17:30: Using the K Framework to Formalize Functional LanguagesTutorials at Tutorials 1 https://www.youtube.com/watch?v=VlQMi_N42B8&feature=youtu.be | |||
| 14:00 - 17:30 Tutorial | Using the K Framework to Formalize Functional Languages Tutorials Xiaohong ChenUniversity of Illinois at Urbana-Champaign, Grigore RoşuUniversity of Illinois at Urbana-Champaign | ||
14:30 - 16:10: Paper Session 2 - Animations and DemonstrationsHaskell at Haskell Chair(s): Exequiel RivasInria Paris | |||
| 14:30 - 15:00 Talk | A Low-Latency Garbage Collector for GHC (Demo) Haskell | ||
| 15:00 - 15:30 Talk | Relational Lenses as a Library (Demo) Haskell Rudi HornUniversity of Edinburgh File Attached | ||
| 15:30 - 16:00 Talk | Scripted Signal Functions Haskell David A. StuartNone DOI | ||
| 16:00 - 16:10 Other | PC Chair Report Haskell Tom SchrijversKU Leuven | ||
14:30 - 15:30: Afternoon KeynoteminiKanren at miniKanren Chair(s): Jason HemannNortheastern University, United States | |||
| 14:30 - 15:30 Keynote | The Pill is in The Proof: Saving Lives with Logic miniKanren Matthew MightUniversity of Alabama at Birmingham | Harvard Medical School | ||
| 15:20 - 17:40 Social Event | ShutdownPL: Accountability Social Events | ||
| 15:20 - 17:40 Social Event | ShutdownPL: Pedagogy Social Events | ||
| 15:20 - 17:40 Social Event | ShutdownPL: Mentorship Social Events | ||
15:30 - 17:10: Afternoon SessionminiKanren at miniKanren Chair(s): Nada AminHarvard University, Weixi MaIndiana University | |||
| 15:30 - 15:50 Talk | mediKanren: A System for Bio-medical Reasoning miniKanren Michael PattonUniversity of Alabama at Birmingham, Gregory RosenblattUniversity of Alabama at Birmingham, USA, William E. ByrdUniversity of Alabama at Birmingham, USA, Matthew MightUniversity of Alabama at Birmingham | Harvard Medical School Pre-print | ||
| 15:50 - 16:10 Talk | Relational Synthesis for Pattern Matching miniKanren Dmitrii KosarevJetBrains Research, Saint Petersburg State University, Dmitri BoulytchevSt. Petersburg State University, St. Petersburg, Russia Pre-print | ||
| 16:10 - 16:30 Talk | Some Novel miniKanren Synthesis Tasks miniKanren Pre-print | ||
| 16:30 - 16:50 Talk | A Relational Interpreter for Synthesizing JavaScript miniKanren Artem ChirkovUniversity of Toronto Mississauga, Gregory RosenblattUniversity of Alabama at Birmingham, USA, Matthew MightUniversity of Alabama at Birmingham | Harvard Medical School, Lisa ZhangUniversity of Toronto Mississauga Pre-print | ||
| 16:50 - 17:10 Talk | dxo: A System for Relational Algebra and Differentiation miniKanren Pre-print | ||
Fri 28 Aug Times are displayed in time zone: Eastern Time (US & Canada) change
Fri 28 Aug
Times are displayed in time zone: Eastern Time (US & Canada) change
05:30 - 08:30: EcosystemOCaml at OCaml Chair(s): Florian AngelettiInria Infrastructure, tooling, and ecosystem in general. | |||
| 05:30 - 06:30 Keynote | The OCaml Platform OCaml Anil MadhavapeddyOCaml Labs | ||
| 06:30 - 07:00 Talk | OCaml-CI : A Zero-Configuration CI OCaml Thomas LeonardOCaml Labs, Craig FergusonTarides, Kate DeplaixOCaml Labs, Magnus SkjegstadTarides and OCaml Labs, Anil MadhavapeddyOCaml Labs | ||
| 07:00 - 07:30 Talk | The final pieces of the OCaml documentation puzzle OCaml | ||
| 07:30 - 08:00 Talk | API migration: compare transformed OCaml Joseph HarrisonUniversity of Kent, UK, Steven VaroumasUniversity of Kent, Simon ThompsonUniversity of Kent, Reuben RoweUniversity College London | ||
| 08:00 - 08:30 Talk | Parallelising your OCaml Code with Multicore OCaml OCaml Sadiq JafferOpsian and OCaml Labs, Sudha ParimalaIIT Madras, KC SivaramakrishnanIIT Madras, Tom KellyOCaml Labs, Anil MadhavapeddyOCaml Labs Pre-print | ||
| 09:00 - 09:22 Talk | Asterius: bringing Haskell to WebAssembly HIW | ||
| 09:22 - 09:44 Talk | Multiple Home Units HIW | ||
| 10:00 - 10:35 Talk | Lightning Talks 1 HIW | ||
| 10:35 - 10:57 Talk | Sweet Egison: a Haskell Library for Non-Deterministic Pattern Matching HIW Satoshi EgiRakuten Institute of Technology, Rakuten, Inc. / The University of Tokyo, Akira KawataKyoto University, Mayuko KoriThe University of Tokyo, Hiromi OgawaUniversity of Tsukuba | ||
| 10:57 - 11:19 Talk | Updating Immutable Code HIW | ||
| 11:19 - 11:31 Talk | GHC Status Update HIW | ||
| 11:31 - 12:00 Break | Social break HIW | ||
09:00 - 11:00: ApplicationsOCaml at OCaml Chair(s): Marcello SeriBernoulli Institute for Mathematics, Computer Science and Artificial Intelligence, University of Groningen Talks about new and existing OCaml applications and libraries. | |||
| 09:00 - 09:30 Talk | A Simple State-Machine Framework for Property-Based Testing in OCaml OCaml Jan MidtgaardUniversity of Southern Denmark | ||
| 09:30 - 10:00 Talk | The ImpFS filesystem OCaml Tom RidgeUniversity of Leicester, UK | ||
| 10:00 - 10:30 Talk | Irmin v2 OCaml Clément PascuttoTarides, Ioana CristescuINRIA, France, Craig FergusonTarides, Thomas GazagnaireTarides, Romain LiautaudTarides | ||
| 10:30 - 11:00 Talk | AD-OCaml: Algorithmic Differentiation for OCaml OCaml Markus MottlUnaffiliated | ||
| 09:00 - 12:30 Tutorial | Library-Oriented Dynamic Analysis with Lya Tutorials | ||
| 09:00 - 12:30 Tutorial | Creating SVG graphics and Animations using Elm Tutorials Link to publication DOI | ||
10:00 - 11:00: Paper Session 3 - DatastructuresHaskell at Haskell Chair(s): Andrey MokhovJane Street | |||
| 10:00 - 10:30 Talk | Finger Trees Explained Anew, and Slightly Simplified (Functional Pearl) Haskell Koen ClaessenChalmers University of Technology, Sweden DOI | ||
| 10:30 - 11:00 Talk | Type Your Matrices for Great Good: A Haskell Library of Typed Matrices and Applications (Functional Pearl) Haskell Armando João Isaías Ferreira dos SantosUniversity of Minho, Portugal / INESC TEC, Portugal, Jose Nuno OliveiraUniversity of Minho, Portugal / INESC TEC, Portugal DOI | ||
| 10:00 - 11:00 Keynote | SICP JS: Ketchup on Caviar? Scheme | ||
11:30 - 13:00: Paper Session 4 - EffectsHaskell at Haskell Chair(s): Pierre-Evariste DagandLIP6/CNRS | |||
| 11:30 - 12:00 Talk | A Graded Monad for Deadlock-Free Concurrency (Functional Pearl) Haskell DOI | ||
| 12:00 - 12:30 Talk | Composing Effects into Tasks and Workflows Haskell Yves ParèsTweag I/O, France, Jean-Philippe BernardyUniversity of Gothenburg, Sweden, Richard A. EisenbergTweag I/O DOI | ||
| 12:30 - 13:00 Talk | Effect Handlers in Haskell, Evidently Haskell DOI | ||
11:30 - 13:30: ExperienceOCaml at OCaml Chair(s): Greta YorshJane Street Sharing experience about using OCaml in various scenarios. | |||
| 11:30 - 12:00 Talk | OCaml Under The Hood: SmartPy OCaml Sebastien MondetTQ Tezos | ||
| 12:00 - 12:30 Talk | |||