Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Thu 20 AugDisplayed time zone: Eastern Time (US & Canada) change
Thu 20 Aug
Displayed time zone: Eastern Time (US & Canada) change
21:00 - 22:00 | |||
21:00 60mOther | Clowdr Training Sessions Clowdr Training Benjamin C. Pierce University of Pennsylvania | ||
Fri 21 AugDisplayed time zone: Eastern Time (US & Canada) change
Fri 21 Aug
Displayed time zone: Eastern Time (US & Canada) change
09:00 - 10:00 | |||
09:00 60mOther | Clowdr Training Sessions Clowdr Training Benjamin C. Pierce University of Pennsylvania | ||
Sun 23 AugDisplayed time zone: Eastern Time (US & Canada) change
Sun 23 Aug
Displayed time zone: Eastern Time (US & Canada) change
07:50 - 09:30 | |||
07:50 10mDay opening | Opening Erlang | ||
08:00 30mShort-paper | Transformations towards Clean Functional Code Erlang Boldizsár Poór Eötvös Loránd University, Melinda Tóth Eö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 30mTalk | Supporting Secure Coding with RefactorErl Erlang Brigitta Baranyai ELTE Eötvös Loránd University, István Bozó Eötvös Loránd University, Melinda Tóth Eötvös Loránd University, Faculty of Informatics, Department of Programming Languages and Compilers & ELTE-Soft Nonprofit Ltd. | ||
09:00 30mFull-paper | Teaching Practical Realistic Verification of Distributed Algorithms in Erlang with TLA+ Erlang Peter Zeller TU Kaiserslautern, Annette Bieniusa Technische Universität Kaiserslautern, Carla Ferreira Universidade Nova Lisboa DOI | ||
08:00 - 11:30 | |||
08:00 60mKeynote | Variants of call-by-push-value HOPE Paul Blain Levy University of Birmingham | ||
09:15 45mTalk | Kripke open relations and operational game semantics HOPE | ||
10:00 45mTalk | Merging coeffect production into effect handling HOPE Tarmo Uustalu Reykjavik University, Tallinn University of Technology, Niels Voorneveld Tallinn University of Technology | ||
10:45 45mTalk | Simply RaTT: A Fitch-style Modal Calculus for Reactive Programming HOPE Patrick Bahr IT University of Copenhagen, Christian Uldal Graulund IT University of Copenhagen, Rasmus Ejlers Møgelberg IT University of Copenhagen | ||
09:00 - 10:00 | |||
09:00 15mDay opening | Welcome PLMW @ ICFP Lindsey Kuper University of California, Santa Cruz, Talia Ringer University of Washington, Nate Foster Cornell University | ||
09:15 45mTalk | How To Write Papers So People Can Read Them PLMW @ ICFP Derek Dreyer MPI-SWS | ||
09:00 - 12:30 | |||
09:00 3h30mTutorial | Teaching Functional Programming Tutorials Michael Sperber Active Group GmbH | ||
09:00 - 12:30 | |||
09:00 3h30mTutorial | Audio, Video & Web Live Coding in Haskell Tutorials Manuel Bärenz sonnen eServices GmbH Pre-print | ||
10:00 - 11:30 | |||
10:00 30mTalk | Practical Dependent Type Checking Using Twin Types TyDe Víctor López Juan Chalmers University of Technology, Nils Anders Danielsson University of Gothenburg, Chalmers University of Technology Media Attached | ||
10:30 30mTalk | Shallowly Embedding Type Theories as Presheaf Models in Agda (Extended Abstract) TyDe File Attached | ||
11:00 30mTalk | Generalization of Meta-Programs with Dependent Types in Mtac2 with Mtac2 (Extended Abstract) TyDe | ||
10:30 - 12:00 | |||
10:30 30mFull-paper | Machine-Checked Natural Semantics for Core Erlang: Exceptions and Side Effects Erlang Simon Thompson University of Kent, Dániel Horpácsi Eötvös Loránd University, Péter Bereczky Eötvös Loránd University DOI | ||
11:00 30mFull-paper | Secure Design and Verification of Erlang Systems Erlang Viktória Fördős Cisco Systems DOI | ||
11:30 30mFull-paper | Clojerl: The Expressive Power of Clojure on the BEAM Erlang DOI | ||
10:30 - 12:30 | |||
10:30 40mTalk | Constraint Solvers for the Working PL Researcher PLMW @ ICFP Nadia Polikarpova University of California, San Diego | ||
11:10 40mTalk | Managing your Research, your Advisor, your PhD PLMW @ ICFP Amal Ahmed Northeastern University, USA | ||
11:50 40mTalk | Basic Mechanics of Operational Semantics PLMW @ ICFP David Van Horn University of Maryland, USA | ||
12:00 - 14:00 | |||
12:00 45mTalk | Higher-order Programming with Effects and Handlers — without First-Class Functions HOPE Jonathan Immanuel Brachthäuser University of Tübingen, Germany, Philipp Schuster University of Tübingen, Germany | ||
12:45 45mTalk | Towards Highly Symmetric Effects and Coeffects and a Systematic Separation between the Extra- and Intra-Logical HOPE Ingo Skupin University of Tübingen, Julian Jabs University of Tübingen, David Binder University of Tübingen File Attached | ||
12:30 - 13:30 | Session 3Erlang at Erlang Chair(s): Annette Bieniusa Technische Universität Kaiserslautern, Viktória Fördős Cisco Systems | ||
12:30 60mKeynote | Living on the Edge with Erlang Erlang Peter Van Roy Université catholique de Louvain | ||
12:30 - 14:00 | |||
12:30 30mTalk | Graded Modal Dependent Type Theory (Extended Abstract) TyDe Benjamin Moon School of Computing, University of Kent, Harley D. Eades III Augusta University, Dominic Orchard University of Kent, UK File Attached | ||
13:00 30mTalk | Frex: indexing modulo equations with free extensions (Extended Abstract) TyDe Guillaume Allais University of St Andrews, Edwin Brady University of St. Andrews, UK, Ohad Kammar University of Edinburgh, Jeremy Yallop University of Cambridge | ||
13:30 30mTalk | Retrofitting Symbolic Holes to LLVM IR (Extended Abstract) TyDe Pre-print | ||
13:30 - 14:00 | |||
13:30 30mSocial Event | Optional Social Activity PLMW @ ICFP | ||
14:00 - 15:00 | |||
14:00 60mIndustry talk | Panel - Erlang fuelled inventions Erlang | ||
14:00 - 15:30 | |||
14:00 45mTalk | How Can I Academia When My Brain Can't Even? Mental Health in Grad School and Beyond PLMW @ ICFP Kenny Foner Galois | ||
14:45 45mTalk | Functional Programming for COVID-19 Drug Repurposing PLMW @ ICFP Nada Amin Harvard University | ||
14:00 - 17:30 | |||
14:00 3h30mTutorial | Best Practices in Code Generation Tutorials Michal J. Gajda Migamake Pte Ltd | ||
14:00 - 17:30 | Designing Hardware Systems and Accelerators with Open-Source Bluespec HaskellTutorials at Tutorials 2 | ||
14:00 3h30mTutorial | Designing Hardware Systems and Accelerators with Open-Source Bluespec Haskell Tutorials Rishiyur Nikhil Bluespec, Inc. | ||
14:30 - 16:00 | |||
14:30 45mTalk | Effectful Improvement Theory HOPE Martin Ceresa UNR - CIFASIS - CONICET | ||
15:15 45mTalk | Alef: A bidirectional effect system for algebraic effects. HOPE Antonio Locascio Universidad Nacional de Rosario | ||
15:30 - 17:00 | |||
15:30 30mTalk | Predictable Macros for Hindley-Milner (Extended Abstract) TyDe | ||
16:00 30mTalk | Strongly Bounded Termination with Applications to Security and Hardware Synthesis TyDe Thomas Reynolds University of Missouri, William Harrison Oak Ridge National Laboratory, Rohit Chadha University of Missouri, Gerard Allwein U.S. Naval Research Laboratory | ||
16:30 30mTalk | Developing a Dependently Typed Language with Runtime Proof Search (Extended Abstract) TyDe | ||
16:00 - 17:00 | |||
16:00 60mTalk | Panel discussion: Making a career in PL (even in uncertain times) PLMW @ ICFP P: Simon Peyton Jones Microsoft, UK, P: Kathleen Fisher Tufts University, USA, P: Jose Calderon Galois, Inc., P: Benjamin C. Pierce University of Pennsylvania, P: Sarah E. Chasins University of California, Berkeley, P: Jeff Vaughan Google | ||
Mon 24 AugDisplayed time zone: Eastern Time (US & Canada) change
Mon 24 Aug
Displayed time zone: Eastern Time (US & Canada) change
05:00 - 18:00 | |||
05:00 60mLive Q&A | Jane Street 1 ICFP Sponsors | ||
13:30 60mLive Q&A | Jane Street 3 ICFP Sponsors | ||
09:00 - 18:00 | |||
09:00 - 18:00 | |||
09:00 - 18:00 | |||
09:00 - 10:00 | |||
09:00 60mTalk | Referential transparency for pandemic resilience ICFP Program | ||
09:00 - 18:00 | |||
10:00 - 11:30 | |||
10:00 90mSocial Event | ICFP Social Time Social Events | ||
10:00 - 10:30 | |||
10:00 30mOther | Information Desk Social Events Stephanie Weirich University of Pennsylvania | ||
10:30 - 11:30 | |||
10:30 60mMeeting | How to Use Clowdr at ICFP Social Events Benjamin C. Pierce University of Pennsylvania | ||
10:30 - 11:30 | |||
10:30 8mPoster | A GHC-Plugin to Compile Effectful Languages Student Research Competition Kai-Oliver Prott CAU Kiel | ||
10:38 8mPoster | Certified double sided auction mechanisms Student Research Competition Suneel sarswat TIFR | ||
10:47 8mPoster | Certified Optimisation of Stream Operations Using Heterogeneous Staging Student Research Competition James Lowenthal University of Cambridge | ||
10:55 8mPoster | Pattern Matching with Typed Holes Student Research Competition Yongwei Yuan University of Michigan | ||
11:04 8mPoster | Type Hole Inference Student Research Competition Zhiyi Pan University of Michigan | ||
11:12 8mPoster | Semantics for a Simple Differentiable Language Using Distribution Theory Student Research Competition Christopher Lam Cornell University | ||
11:21 8mPoster | Gradual Enforcement of IO Trace Properties Student Research Competition Cezar-Constantin Andrici Alexandru Ioan Cuza University of Iasi | ||
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 | ||
13:00 - 14:30 | |||
13:00 90mSocial Event | ICFP Social Time Social Events | ||
13:00 - 13:30 | |||
13:00 30mOther | Information Desk Social Events Stephanie Weirich University 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 60mSocial Event | W@ICFP Social Events | ||
14:30 - 16:30 | |||
14:30 15mTalk | Achieving High-Performance the Functional Way - A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies ICFP Program Bastian Hagedorn University of Münster, Germany, Johannes Lenfers University of Münster, Thomas Koehler University of Glasgow, United Kingdom, Xueying Qin University of Glasgow, United Kingdom, Sergei Gorlatch University of Münster, Germany, Michel Steuwer The University of Edinburgh DOI Media Attached | ||
14:45 15mTalk | Staged Selective Parser Combinators ICFP Program Jamie Willis Imperial College London, Nicolas Wu Imperial College London, UK, Matthew Pickering University of Bristol, UK DOI Media Attached | ||
15:00 15mTalk | Kindly Bent to Free Us ICFP Program Gabriel Radanne Inria, Hannes Saffrich University of Freiburg, Peter Thiemann University of Freiburg, Germany DOI Pre-print Media Attached File Attached | ||
15:15 15mTalk | Sealing Pointer-Based Optimizations Behind Pure Functions ICFP Program Daniel Selsam Microsoft Research, Simon Hudon Carnegie Mellon University, Leonardo de Moura Microsoft Research, n.n. DOI Media Attached | ||
15:30 15mTalk | Effects for Efficiency: Asymptotic Speedup with First-Class Control ICFP Program Daniel Hillerström The University of Edinburgh, Sam Lindley Heriot-Watt University, UK / The University of Edinburgh, UK, John Longley The University of Edinburgh DOI Media Attached | ||
15:45 15mTalk | Computation Focusing ICFP Program DOI Media Attached | ||
16:00 15mTalk | Retrofitting Parallelism onto OCamlDistinguished Paper ICFP Program KC Sivaramakrishnan IIT Madras, Stephen Dolan University of Cambridge, UK, Leo White Jane Street, Sadiq Jaffer Opsian and OCaml Labs, Tom Kelly OCaml Labs, Anmol Sahoo IIT Madras, Sudha Parimala IIT Madras, Atul Dhiman IIT Madras, Anil Madhavapeddy OCaml Labs DOI Media Attached | ||
16:15 15mTalk | Liquid Information Flow ControlDistinguished Paper ICFP Program Nadia Polikarpova University of California, San Diego, Deian Stefan University of California at San Diego, USA, Jean Yang Carnegie Mellon University, Shachar Itzhaky Technion, Israel, Travis Hance Carnegie Mellon University, Armando Solar-Lezama Massachusetts Institute of Technology, USA DOI Media Attached | ||
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 | ||
16:30 - 17:30 | |||
16:30 60mSocial Event | ICFP Social Time Social Events | ||
16:30 - 17:30 | |||
16:30 60mSocial Event | Untitled PL Card Game Social Events Jasper Van der Jeugt Fugue, Niki Vazou IMDEA Software Institute, Leonidas Lampropoulos University of Maryland, College Park Media Attached | ||
21:00 - 22:00 | |||
21:00 60mSocial Event | ICFP Social Time Social Events | ||
21:00 - 22:00 | Women in CS PanelSocial Events at ICFP Social Chair(s): Cristina Cifuentes Oracle Labs YouTube recording of event: https://youtu.be/uHdtXFEwVCs | ||
21:00 60mSocial Event | Women in CS Panel Social Events P: Cristina Cifuentes Oracle Labs, P: Sukyoung Ryu KAIST, P: Alena Griffiths RGB Assurance, P: Behnaz Hassanshahi Oracle Labs, Australia | ||
22:00 - 23:00 | |||
22:00 60mMeeting | How to Use Clowdr at ICFP Social Events Benjamin C. Pierce University of Pennsylvania | ||
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
Tue 25 Aug
Displayed time zone: Eastern Time (US & Canada) change
01:00 - 02:00 | |||
01:00 60mSocial Event | ICFP Social Time Social Events | ||
01:00 - 02:00 | |||
01:00 60mTalk | Mentoring with Ranjit Jhala Social Events Ranjit Jhala University of California at San Diego, USA | ||
02:30 - 04:30 | |||
02:30 15mTalk | Achieving High-Performance the Functional Way - A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies ICFP Program Bastian Hagedorn University of Münster, Germany, Johannes Lenfers University of Münster, Thomas Koehler University of Glasgow, United Kingdom, Xueying Qin University of Glasgow, United Kingdom, Sergei Gorlatch University of Münster, Germany, Michel Steuwer The University of Edinburgh DOI Media Attached | ||
02:45 15mTalk | Staged Selective Parser Combinators ICFP Program Jamie Willis Imperial College London, Nicolas Wu Imperial College London, UK, Matthew Pickering University of Bristol, UK DOI Media Attached | ||
03:00 15mTalk | Kindly Bent to Free Us ICFP Program Gabriel Radanne Inria, Hannes Saffrich University of Freiburg, Peter Thiemann University of Freiburg, Germany DOI Pre-print Media Attached File Attached | ||
03:15 15mTalk | Sealing Pointer-Based Optimizations Behind Pure Functions ICFP Program Daniel Selsam Microsoft Research, Simon Hudon Carnegie Mellon University, Leonardo de Moura Microsoft Research, n.n. DOI Media Attached | ||
03:30 15mTalk | Effects for Efficiency: Asymptotic Speedup with First-Class Control ICFP Program Daniel Hillerström The University of Edinburgh, Sam Lindley Heriot-Watt University, UK / The University of Edinburgh, UK, John Longley The University of Edinburgh DOI Media Attached | ||
03:45 15mTalk | Computation Focusing ICFP Program DOI Media Attached | ||
04:00 15mTalk | Retrofitting Parallelism onto OCamlDistinguished Paper ICFP Program KC Sivaramakrishnan IIT Madras, Stephen Dolan University of Cambridge, UK, Leo White Jane Street, Sadiq Jaffer Opsian and OCaml Labs, Tom Kelly OCaml Labs, Anmol Sahoo IIT Madras, Sudha Parimala IIT Madras, Atul Dhiman IIT Madras, Anil Madhavapeddy OCaml Labs DOI Media Attached | ||
04:15 15mTalk | Liquid Information Flow ControlDistinguished Paper ICFP Program Nadia Polikarpova University of California, San Diego, Deian Stefan University of California at San Diego, USA, Jean Yang Carnegie Mellon University, Shachar Itzhaky Technion, Israel, Travis Hance Carnegie Mellon University, Armando Solar-Lezama Massachusetts Institute of Technology, USA DOI Media Attached | ||
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 | |||
04:30 - 05:30 | |||
04:30 60mSocial Event | ICFP Social Time Social Events | ||
04:30 - 05:30 | |||
04:30 60mMeeting | Online Lecture Panel Social Events Atsushi Igarashi Kyoto University, Japan, Sukyoung Ryu KAIST, Ilya Sergey Yale-NUS College and National University of Singapore, Alex Potanin Victoria University of Wellington | ||
05:00 - 18:00 | |||
05:00 60mLive Q&A | Jane Street 1 ICFP Sponsors | ||
10:00 60mLive Q&A | Jane Street 2 ICFP Sponsors | ||
13:30 60mLive Q&A | Jane Street 3 ICFP Sponsors | ||
09:00 - 18:00 | |||
09:00 - 18:00 | |||
09:00 - 18:00 | |||
09:00 - 10:00 | |||
09:00 60mTalk | On Language Adoption ICFP Program | ||
09:00 - 18:00 | |||
10:00 - 10:30 | |||
10:00 30mOther | Information Desk Social Events Stephanie Weirich University of Pennsylvania | ||
10:30 - 11:30 | |||
10:30 60mSocial Event | Virtual Art Gallery Social Events Alan Jeffrey Mozilla Research | ||
10:30 - 11:30 | |||
10:30 30mMeeting | SIGPLAN CARES Social Events David Walker Princeton University, USA, Simon Peyton Jones Microsoft, UK, Alexandra Silva University College London, Shriram Krishnamurthi Brown University, United States | ||
11:30 - 12:15 | |||
11:30 45mTalk | SRC Finalist Presentation 1 Student Research Competition | ||
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 | ||
13:00 - 14:30 | |||
13:00 90mSocial Event | ICFP Social Time Social Events | ||
13:00 - 13:30 | |||
13:00 30mOther | Information Desk Social Events Stephanie Weirich University of Pennsylvania | ||
13:30 - 14:30 | |||
13:30 60mTalk | LGBTQ Meetup Social Events | ||
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 | ||
16:30 - 17:30 | |||
16:30 60mSocial Event | ICFP Social Time Social Events | ||
16:30 - 17:30 | |||
16:30 60mSocial Event | ICFP Triva Social Events | ||
21:00 - 22:30 | |||
21:00 90mSocial Event | ICFP Social Time Social Events | ||
21:00 - 22:00 | |||
21:00 30mMeeting | SIGPLAN CARES Social Events David Walker Princeton University, USA, Simon Peyton Jones Microsoft, UK, Alexandra Silva University College London, Shriram Krishnamurthi Brown University, United States | ||
21:30 - 22:30 | |||
21:30 60mMeeting | Mind the Title Social Events Olivier Danvy Yale-NUS College and School of Computing, Singapore | ||
22:40 - 00:10 | |||
22:40 - 00:10 | |||
23:30 - 00:15 | |||
23:30 45mTalk | SRC Finalist Presentation 2 Student Research Competition | ||
Wed 26 AugDisplayed time zone: Eastern Time (US & Canada) change
Wed 26 Aug
Displayed time zone: Eastern Time (US & Canada) change
00:00 - 01:00 | |||
00:00 60mSocial Event | ICFP Social Time Social Events | ||
00:00 - 01:00 | |||
00:00 60mTalk | Mentoring with Guy Steele Social Events Guy L. Steele Jr. Oracle Labs | ||
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 | ||
04:30 - 05:30 | |||
04:30 60mSocial Event | ICFP Social Time Social Events | ||
04:30 - 05:30 | |||
04:30 60mTalk | Some Proverbs in Type Theory Social Events Neel Krishnaswami Computer Laboratory, University of Cambridge | ||
05:00 - 18:00 | |||
05:00 60mLive Q&A | Jane Street 1 ICFP Sponsors | ||
10:00 60mLive Q&A | Jane Street 2 ICFP Sponsors | ||
13:30 60mLive Q&A | Jane Street 3 ICFP Sponsors | ||
16:30 60mSocial Event | Jane Street at Industrial Reception ICFP Sponsors | ||
09:00 - 18:00 | |||
16:30 60mSocial Event | Ahrefs at Industrial Reception ICFP Sponsors | ||
09:00 - 18:00 | |||
16:30 60mSocial Event | Facebook at Industrial Reception ICFP Sponsors | ||
09:00 - 18:00 | |||
16:30 60mSocial Event | Galois at Industrial Reception ICFP Sponsors | ||
09:00 - 09:45 | ICFP Programming ContestICFP Program at ICFP Awards Chair(s): Stephanie Weirich University of Pennsylvania | ||
09:00 45mKeynote | Programming Contest Report ICFP Program Igor Lukanin Kontur | ||
09:00 - 18:00 | |||
16:30 60mSocial Event | Standard Chartered at Industrial Reception ICFP Sponsors | ||
09:45 - 10:30 | |||
09:45 45mTalk | Award Presentations & Chair Report ICFP Program Stephanie Weirich University of Pennsylvania, Adam Chlipala Massachusetts Institute of Technology, Mira Mezini Technische Universität Darmstadt, Sukyoung Ryu KAIST, Jens Palsberg University of California, Los Angeles, Youyou Cong Tokyo Institute of Technology | ||
10:30 - 11:00 | |||
10:30 30mOther | Information Desk Social Events Stephanie Weirich University of Pennsylvania | ||
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 | ||
13:00 - 14:30 | |||
13:00 90mSocial Event | ICFP Social Time Social Events | ||
13:00 - 13:30 | |||
13:00 30mOther | Information Desk Social Events Stephanie Weirich University of Pennsylvania | ||
13:30 - 14:30 | |||
13:30 60mMeeting | Virtualization Feedback Social Events Benjamin C. Pierce University of Pennsylvania, Jonathan Bell Northeastern University, Crista Lopes University of California, Irvine | ||
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 | ||
16:30 - 17:30 | |||
16:30 60mSocial Event | Industrial Reception Social Events | ||
16:30 - 17:30 | |||
16:30 60mSocial Event | Tweag at Industrial Reception ICFP Sponsors | ||
16:30 - 17:30 | |||
16:30 60mSocial Event | Bloomberg at Industrial Reception ICFP Sponsors | ||
16:30 - 17:30 | |||
16:30 60mSocial Event | Microsoft at Industrial Reception ICFP Sponsors | ||
16:30 - 17:30 | |||
16:30 60mSocial Event | Oracle at Industrial Reception ICFP Sponsors | ||
21:00 - 22:00 | |||
21:00 60mSocial Event | ICFP Social Time Social Events | ||
21:00 - 22:00 | |||
21:00 60mMeeting | Virtualization Feedback Social Events Benjamin C. Pierce University of Pennsylvania, Jonathan Bell Northeastern University, Crista Lopes University of California, Irvine | ||
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
Thu 27 Aug
Displayed time zone: Eastern Time (US & Canada) change
00:30 - 01:30 | |||
00:30 60mSocial Event | ICFP Social Time Social Events | ||
00:30 - 01:30 | |||
00:30 60mTalk | Mentoring with Matthias Felleisen Social Events Matthias Felleisen PLT @ Northeastern University | ||
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 | ||
04:30 - 05:30 | |||
04:30 60mSocial Event | ICFP Social Time Social Events | ||
09:00 - 10:00 | |||
09:00 60mMeeting | Academic Career Planning During a Crisis Social Events Neel Krishnaswami Computer 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 3h30mTutorial | Functional Software Architecture Tutorials Michael Sperber Active Group GmbH | ||
09:00 - 12:30 | |||
09:00 3h30mTutorial | Integrating User-Centered Methods into Programming Language Design Tutorials | ||
09:00 - 11:00 | Morning KeynoteminiKanren at miniKanren Chair(s): Dmitri Boulytchev St. Petersburg State University, St. Petersburg, Russia | ||
10:00 60mKeynote | Executing Declarative Language Definitions miniKanren | ||
10:00 - 11:00 | |||
10:00 60mKeynote | Using STM for Modular Concurrency: An Industrial Experience Report on Software Transactional Memory Haskell | ||
10:00 - 11:00 | |||
10:00 60mKeynote | Verification of OCaml programs using CFML ML Arthur Charguéraud Inria Media Attached | ||
11:30 - 13:00 | |||
11:30 30mTalk | Assessing the Quality of Evolving Haskell Systems by Measuring Structural Inequality Haskell Sander Kamps Open University of the Netherlands, Netherlands, Bastiaan Heeren Open University of the Netherlands, Netherlands, Johan Jeuring Open University of the Netherlands, Netherlands DOI | ||
12:00 30mTalk | Describing Microservices using Modern Haskell (Experience Report) Haskell DOI | ||
12:30 30mTalk | Towards Secure IoT Programming in Haskell Haskell Nachiappan Valliappan Chalmers University of Technology, Sweden, Robert Krook Chalmers University of Technology, Sweden, Alejandro Russo Chalmers University of Technology, Sweden, Koen Claessen Chalmers University of Technology, Sweden DOI | ||
11:30 - 13:10 | |||
11:30 25mTalk | Tracking injectivity and nominality beyond abstraction ML Jacques Garrigue Nagoya University Media Attached File Attached | ||
11:55 25mTalk | Quantified Applicatives – API design for type-inference constraints ML Media Attached File Attached | ||
12:20 25mTalk | High-level error messages for modules through diffing ML Media Attached File Attached | ||
12:45 25mTalk | The Virtues of Semi-Explicit Polymorphism ML Frank Emrich University of Edinburgh, UK, Sam Lindley Heriot-Watt University, UK / The University of Edinburgh, UK, Jan Stolarek University of Edinburgh, UK Media Attached File Attached | ||
14:00 - 18:00 | |||
14:00 4hSocial Event | ShutdownPL: Keynote and Getting Started With Anti-racist Action Social Events Kenny Foner Galois, Niki Carroll George Mason University, Priya Srikumar Cornell University, David Justo University of California, San Diego, Justin Lubin University of Chicago, Akash Gaonkar , Alan Jeffrey Mozilla 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 3h30mTutorial | Using the K Framework to Formalize Functional Languages Tutorials Xiaohong Chen University of Illinois at Urbana-Champaign, Grigore Roşu University of Illinois at Urbana-Champaign | ||
14:30 - 16:10 | Paper Session 2 - Animations and DemonstrationsHaskell at Haskell Chair(s): Exequiel Rivas Inria Paris | ||
14:30 30mTalk | A Low-Latency Garbage Collector for GHC (Demo) Haskell | ||
15:00 30mTalk | Relational Lenses as a Library (Demo) Haskell Rudi Horn University of Edinburgh File Attached | ||
15:30 30mTalk | Scripted Signal Functions Haskell David A. Stuart None DOI | ||
16:00 10mOther | PC Chair Report Haskell Tom Schrijvers KU Leuven | ||
14:30 - 15:30 | Afternoon KeynoteminiKanren at miniKanren Chair(s): Jason Hemann Northeastern University, United States | ||
14:30 60mKeynote | The Pill is in The Proof: Saving Lives with Logic miniKanren Matthew Might University of Alabama at Birmingham | Harvard Medical School | ||
15:20 - 17:40 | |||
15:20 2h20mSocial Event | ShutdownPL: Accountability Social Events | ||
15:20 - 17:40 | |||
15:20 2h20mSocial Event | ShutdownPL: Pedagogy Social Events | ||
15:20 - 17:40 | |||
15:20 2h20mSocial Event | ShutdownPL: Mentorship Social Events | ||
15:30 - 17:10 | Afternoon SessionminiKanren at miniKanren Chair(s): Nada Amin Harvard University, Weixi Ma Indiana University | ||
15:30 20mTalk | mediKanren: A System for Bio-medical Reasoning miniKanren Michael Patton University of Alabama at Birmingham, Gregory Rosenblatt University of Alabama at Birmingham, USA, William E. Byrd University of Alabama at Birmingham, USA, Matthew Might University of Alabama at Birmingham | Harvard Medical School Link to publication | ||
15:50 20mTalk | Relational Synthesis for Pattern Matching miniKanren Dmitrii Kosarev JetBrains Research, Saint Petersburg State University, Dmitri Boulytchev St. Petersburg State University, St. Petersburg, Russia Link to publication | ||
16:10 20mTalk | Some Novel miniKanren Synthesis Tasks miniKanren Link to publication | ||
16:30 20mTalk | A Relational Interpreter for Synthesizing JavaScript miniKanren Artem Chirkov University of Toronto Mississauga, Gregory Rosenblatt University of Alabama at Birmingham, USA, Matthew Might University of Alabama at Birmingham | Harvard Medical School, Lisa Zhang University of Toronto Mississauga Link to publication | ||
16:50 20mTalk | dxo: A System for Relational Algebra and Differentiation miniKanren Link to publication | ||
Fri 28 AugDisplayed time zone: Eastern Time (US & Canada) change
Fri 28 Aug
Displayed time zone: Eastern Time (US & Canada) change
05:30 - 08:30 | EcosystemOCaml at OCaml Chair(s): Florian Angeletti Inria Infrastructure, tooling, and ecosystem in general. | ||
05:30 60mKeynote | The OCaml Platform OCaml Anil Madhavapeddy OCaml Labs | ||
06:30 30mTalk | OCaml-CI : A Zero-Configuration CI OCaml Thomas Leonard OCaml Labs, Craig Ferguson Tarides, Kate Deplaix OCaml Labs, Magnus Skjegstad Tarides and OCaml Labs, Anil Madhavapeddy OCaml Labs | ||
07:00 30mTalk | The final pieces of the OCaml documentation puzzle OCaml | ||
07:30 30mTalk | API migration: compare transformed OCaml Joseph Harrison University of Kent, UK, Steven Varoumas University of Kent, Simon Thompson University of Kent, Reuben Rowe University College London | ||
08:00 30mTalk | Parallelising your OCaml Code with Multicore OCaml OCaml Sadiq Jaffer Opsian and OCaml Labs, Sudha Parimala IIT Madras, KC Sivaramakrishnan IIT Madras, Tom Kelly OCaml Labs, Anil Madhavapeddy OCaml Labs Pre-print | ||
09:00 - 12:00 | |||
09:00 22mTalk | Asterius: bringing Haskell to WebAssembly HIW | ||
09:22 22mTalk | Multiple Home Units HIW Hannes Siebenhandl None | ||
10:00 35mTalk | Lightning Talks 1 HIW | ||
10:35 22mTalk | Sweet Egison: a Haskell Library for Non-Deterministic Pattern Matching HIW Satoshi Egi Rakuten Institute of Technology, Rakuten, Inc. / The University of Tokyo, Akira Kawata Kyoto University, Mayuko Kori The University of Tokyo, Hiromi Ogawa University of Tsukuba | ||
10:57 22mTalk | Updating Immutable Code HIW | ||
11:19 12mTalk | GHC Status Update HIW | ||
11:31 29mBreak | Social break HIW | ||
09:00 - 11:00 | ApplicationsOCaml at OCaml Chair(s): Marcello Seri Bernoulli Institute for Mathematics, Computer Science and Artificial Intelligence, University of Groningen Talks about new and existing OCaml applications and libraries. | ||
09:00 30mTalk | A Simple State-Machine Framework for Property-Based Testing in OCaml OCaml Jan Midtgaard University of Southern Denmark | ||
09:30 30mTalk | The ImpFS filesystem OCaml Tom Ridge University of Leicester, UK | ||
10:00 30mTalk | Irmin v2 OCaml Clément Pascutto Tarides, Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, Ioana Cristescu INRIA, France, Craig Ferguson Tarides, Thomas Gazagnaire Tarides, Romain Liautaud Tarides | ||
10:30 30mTalk | AD-OCaml: Algorithmic Differentiation for OCaml OCaml Markus Mottl Unaffiliated | ||
09:00 - 12:30 | |||
09:00 3h30mTutorial | Library-Oriented Dynamic Analysis with Lya Tutorials | ||
09:00 - 12:30 | |||
09:00 3h30mTutorial | Creating SVG graphics and Animations using Elm Tutorials Link to publication DOI | ||
10:00 - 11:00 | |||
10:00 30mTalk | Finger Trees Explained Anew, and Slightly Simplified (Functional Pearl) Haskell Koen Claessen Chalmers University of Technology, Sweden DOI | ||
10:30 30mTalk | Type Your Matrices for Great Good: A Haskell Library of Typed Matrices and Applications (Functional Pearl) Haskell Armando João Isaías Ferreira dos Santos University of Minho, Portugal / INESC TEC, Portugal, Jose Nuno Oliveira University of Minho, Portugal / INESC TEC, Portugal DOI | ||
10:00 - 11:00 | |||
10:00 60mKeynote | SICP JS: Ketchup on Caviar? Scheme | ||
11:30 - 13:00 | |||
11:30 30mTalk | A Graded Monad for Deadlock-Free Concurrency (Functional Pearl) Haskell DOI | ||
12:00 30mTalk | Composing Effects into Tasks and Workflows Haskell Yves Parès Tweag I/O, France, Jean-Philippe Bernardy University of Gothenburg, Sweden, Richard A. Eisenberg Tweag I/O DOI | ||
12:30 30mTalk | Effect Handlers in Haskell, Evidently Haskell DOI | ||
11:30 - 13:30 | ExperienceOCaml at OCaml Chair(s): Greta Yorsh Jane Street Sharing experience about using OCaml in various scenarios. | ||
11:30 30mTalk | OCaml Under The Hood: SmartPy OCaml Sebastien Mondet TQ Tezos | ||
12:00 30mTalk | A Declarative Syntax Definition for OCaml OCaml Luis Eduardo de Souza Amorim Delft University of Technology, Netherlands, Eelco Visser Delft University of Technology Pre-print | ||
12:30 30mTalk | LexiFi Runtime Types OCaml | ||
13:00 30mTalk | Types in amber OCaml | ||
11:30 - 13:00 | |||
11:30 30mTalk | Clotho: A Racket Library for Parametric Randomness Scheme File Attached | ||
12:00 30mTalk | Scheme for scientific computing Scheme Francesco Montanari Universidad Autónoma de Madrid File Attached | ||
12:30 10mTalk | Designing a Programming Environment Based on the Program Design Recipe (Lightning Talk) Scheme Junya Nose Tokyo Institute of Technology, Youyou Cong Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology File Attached | ||
12:40 10mTalk | On Teaching Type Systems as Macros (Lightning Talk) Scheme Youyou Cong Tokyo Institute of Technology, Naoya Furudono Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology File Attached | ||
12:50 10mTalk | Programming with Petri Nets to Reason about Concurrency (Lightning Talk) Scheme Julien Lepiller Yale University File Attached | ||
12:30 - 13:30 | |||
12:30 22mTalk | Exactprint in GHC HIW | ||
12:52 22mTalk | Liquid Haskell as a GHC Plugin HIW Alfredo Di Napoli Well-Typed LLP, Ranjit Jhala University of California at San Diego, USA, Andres Löh Well-Typed LLP, Niki Vazou IMDEA Software Institute | ||
13:14 22mTalk | Stan — Haskell Static Analyser HIW | ||
14:00 - 17:30 | |||
14:00 22mTalk | Implementation of linear types HIW | ||
14:22 22mTalk | Circuit Notation Source Plugin HIW Christopher Chalmers Myrtle.ai | ||
15:00 45mTalk | Lightning Talks 2 HIW | ||
15:45 12mTalk | Embracing a Mechanized Formalization Gap: Interactive reasoning for Haskell at scale HIW Antal Spector-Zabusky University of Pennsylvania, Joachim Breitner DFINITY Foundation, Stephanie Weirich University of Pennsylvania, Yao Li University of Pennsylvania | ||
16:00 20mTalk | Closing HIW Ben Gamari Well-Typed LLP | ||
14:00 - 15:00 | Keynote IIOCaml at OCaml Chair(s): Chris Casinghino Draper Laboratory The recitation of the Keynote speech for those who weren’t able to attend the first one. | ||
14:00 60mKeynote | The OCaml Platform OCaml Anil Madhavapeddy OCaml Labs | ||
14:00 - 17:30 | |||
14:00 3h30mTutorial | Building Multi-Language Tools with Cubix Tutorials James Koppel Massachusetts Institute of Technology, USA | ||
14:30 - 16:00 | |||
14:30 30mTalk | Staged Sums of Products Haskell Matthew Pickering University of Bristol, UK, Andres Löh Well-Typed LLP, Nicolas Wu Imperial College London, UK DOI | ||
15:00 30mTalk | Eliminating Bugs with Dependent Haskell (Experience Report) Haskell Noam Zilberstein Facebook, USA DOI | ||
15:30 30mTalk | Stitch: The Sound Type-Indexed Type Checker (Functional Pearl) Haskell Richard A. Eisenberg Tweag I/O DOI File Attached | ||
14:30 - 16:00 | |||
14:30 30mTalk | Running Scheme On Bare Metal (Experience Report) Scheme File Attached | ||
15:00 30mTalk | Experience Report on Solving the Problem Set of SICP completely. Scheme Vladimir Nikishkin Unaffiliated File Attached | ||
15:30 - 17:30 | RecitationOCaml at OCaml Chair(s): Chris Casinghino Draper Laboratory Repeats Session I for those who weren’t able to attend the earlier time slot. | ||
15:30 30mTalk | API migration: compare transformed OCaml Joseph Harrison University of Kent, UK, Steven Varoumas University of Kent, Simon Thompson University of Kent, Reuben Rowe University College London | ||
16:00 30mTalk | OCaml-CI : A Zero-Configuration CI OCaml Thomas Leonard OCaml Labs, Craig Ferguson Tarides, Kate Deplaix OCaml Labs, Magnus Skjegstad Tarides and OCaml Labs, Anil Madhavapeddy OCaml Labs | ||
16:30 30mTalk | The final pieces of the OCaml documentation puzzle OCaml | ||
17:00 30mTalk | Parallelising your OCaml Code with Multicore OCaml OCaml Sadiq Jaffer Opsian and OCaml Labs, Sudha Parimala IIT Madras, KC Sivaramakrishnan IIT Madras, Tom Kelly OCaml Labs, Anil Madhavapeddy OCaml Labs Pre-print | ||
16:00 - 17:00 | |||
16:00 60mKeynote | 21st Century Lisp in Academic Research and Pedagogy Scheme | ||
17:30 - 19:30 | |||
17:30 2hSocial Event | FARM Performance Social Events | ||