Filter Program
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
Conference DayThu 20 AugDisplayed time zone: Eastern Time (US & Canada) change
Conference Day
Thu 20 AugDisplayed time zone: Eastern Time (US & Canada) change
21:00 - 22:00 | |||
21:00 60mOther | Clowdr Training Sessions Clowdr Training Benjamin C. PierceUniversity of Pennsylvania | ||
Conference DayFri 21 AugDisplayed time zone: Eastern Time (US & Canada) change
Conference Day
Fri 21 AugDisplayed time zone: Eastern Time (US & Canada) change
09:00 - 10:00 | |||
09:00 60mOther | Clowdr Training Sessions Clowdr Training Benjamin C. PierceUniversity of Pennsylvania | ||
Conference DaySun 23 AugDisplayed time zone: Eastern Time (US & Canada) change
Conference Day
Sun 23 AugDisplayed 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órEötvös Loránd University, Melinda TóthEö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 BaranyaiELTE Eötvös Loránd University, István BozóEötvös Loránd University, Melinda TóthEö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 ZellerTU Kaiserslautern, Annette BieniusaTechnische Universität Kaiserslautern, Carla FerreiraUniversidade Nova Lisboa DOI | ||
08:00 - 11:30 | |||
08:00 60mKeynote | Variants of call-by-push-value HOPE Paul Blain LevyUniversity of Birmingham | ||
09:15 45mTalk | Kripke open relations and operational game semantics HOPE | ||
10:00 45mTalk | Merging coeffect production into effect handling HOPE Tarmo UustaluReykjavik University, Tallinn University of Technology, Niels VoorneveldTallinn University of Technology | ||
10:45 45mTalk | 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 - 10:00 | |||
09:00 15mDay opening | Welcome PLMW @ ICFP Lindsey KuperUniversity of California, Santa Cruz, Talia RingerUniversity of Washington, Nate FosterCornell University | ||
09:15 45mTalk | How To Write Papers So People Can Read Them PLMW @ ICFP Derek DreyerMPI-SWS | ||
09:00 - 12:30 | |||
09:00 3h30mTutorial | Teaching Functional Programming Tutorials Michael SperberActive Group GmbH | ||
09:00 - 12:30 | |||
09:00 3h30mTutorial | Audio, Video & Web Live Coding in Haskell Tutorials Manuel Bärenzsonnen eServices GmbH Pre-print | ||
10:00 - 11:30 | |||
10:00 30mTalk | 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 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 ThompsonUniversity of Kent, Dániel HorpácsiEötvös Loránd University, Péter BereczkyEötvös Loránd University DOI | ||
11:00 30mFull-paper | Secure Design and Verification of Erlang Systems Erlang Viktória FördősCisco 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 PolikarpovaUniversity of California, San Diego | ||
11:10 40mTalk | Managing your Research, your Advisor, your PhD PLMW @ ICFP Amal AhmedNortheastern University, USA | ||
11:50 40mTalk | Basic Mechanics of Operational Semantics PLMW @ ICFP David Van HornUniversity 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äuserUniversity of Tübingen, Germany, Philipp SchusterUniversity 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 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 60mKeynote | Living on the Edge with Erlang Erlang Peter Van RoyUniversité catholique de Louvain | ||
12:30 - 14:00 | |||
12:30 30mTalk | 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 30mTalk | 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 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 FonerGalois | ||
14:45 45mTalk | Functional Programming for COVID-19 Drug Repurposing PLMW @ ICFP Nada AminHarvard University | ||
14:00 - 17:30 | |||
14:00 3h30mTutorial | 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 3h30mTutorial | Designing Hardware Systems and Accelerators with Open-Source Bluespec Haskell Tutorials Rishiyur NikhilBluespec, Inc. | ||
14:30 - 16:00 | |||
14:30 45mTalk | Effectful Improvement Theory HOPE Martin CeresaUNR - CIFASIS - CONICET | ||
15:15 45mTalk | Alef: A bidirectional effect system for algebraic effects. HOPE Antonio LocascioUniversidad 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 ReynoldsUniversity of Missouri, William HarrisonOak Ridge National Laboratory, Rohit ChadhaUniversity of Missouri, Gerard AllweinU.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 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 | ||
Conference DayMon 24 AugDisplayed time zone: Eastern Time (US & Canada) change
Conference Day
Mon 24 AugDisplayed 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 WeirichUniversity of Pennsylvania | ||
10:30 - 11:30 | |||
10:30 60mMeeting | How to Use Clowdr at ICFP Social Events Benjamin C. PierceUniversity of Pennsylvania | ||
10:30 - 11:30 | |||
10:30 8mPoster | A GHC-Plugin to Compile Effectful Languages Student Research Competition Kai-Oliver ProttCAU Kiel | ||
10:38 8mPoster | Certified double sided auction mechanisms Student Research Competition Suneel sarswatTIFR | ||
10:47 8mPoster | Certified Optimisation of Stream Operations Using Heterogeneous Staging Student Research Competition James LowenthalUniversity of Cambridge | ||
10:55 8mPoster | Pattern Matching with Typed Holes Student Research Competition Yongwei YuanUniversity of Michigan | ||
11:04 8mPoster | Type Hole Inference Student Research Competition Zhiyi PanUniversity of Michigan | ||
11:12 8mPoster | Semantics for a Simple Differentiable Language Using Distribution Theory Student Research Competition Christopher LamCornell University | ||
11:21 8mPoster | Gradual Enforcement of IO Trace Properties Student Research Competition Cezar-Constantin AndriciAlexandru 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 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 60mSocial Event | W@ICFP Social Events O: Mary Sheeran | ||
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 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 15mTalk | 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 15mTalk | 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 15mTalk | 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 15mTalk | 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 15mTalk | Computation Focusing ICFP Program DOI Media Attached | ||
16:00 15mTalk | 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 15mTalk | 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 - 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 JeugtFugue, Niki VazouIMDEA Software Institute, Leonidas LampropoulosUniversity 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 CifuentesOracle Labs YouTube recording of event: https://youtu.be/uHdtXFEwVCs | ||
21:00 60mSocial 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 | |||
22:00 60mMeeting | How to Use Clowdr at ICFP Social Events Benjamin C. PierceUniversity 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 | ||
Conference DayTue 25 AugDisplayed time zone: Eastern Time (US & Canada) change
Conference Day
Tue 25 AugDisplayed 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 JhalaUniversity 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 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 15mTalk | 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 15mTalk | 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 15mTalk | 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 15mTalk | 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 15mTalk | Computation Focusing ICFP Program DOI Media Attached | ||
04:00 15mTalk | 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 15mTalk | 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 - 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 IgarashiKyoto University, Japan, Sukyoung RyuKAIST, Ilya SergeyYale-NUS College and National University of Singapore, Alex PotaninVictoria 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 WeirichUniversity of Pennsylvania | ||
10:30 - 11:30 | |||
10:30 60mSocial Event | Virtual Art Gallery Social Events Alan JeffreyMozilla Research | ||
10:30 - 11:30 | |||
10:30 30mMeeting | 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 | |||
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 WeirichUniversity 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 WalkerPrinceton University, USA, Simon Peyton JonesMicrosoft, UK, Alexandra SilvaUniversity College London, Shriram KrishnamurthiBrown University, United States | ||
21:30 - 22:30 | |||
21:30 60mMeeting | Mind the Title Social Events Olivier DanvyYale-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 | ||
Conference DayWed 26 AugDisplayed time zone: Eastern Time (US & Canada) change
Conference Day
Wed 26 AugDisplayed 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 KrishnaswamiComputer 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 WeirichUniversity of Pennsylvania | ||
09:00 45mKeynote | Programming Contest Report ICFP Program Igor LukaninKontur | ||
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 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 | |||
10:30 30mOther | Information Desk Social Events Stephanie WeirichUniversity 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 WeirichUniversity of Pennsylvania | ||
13:30 - 14:30 | |||
13:30 60mMeeting | Virtualization Feedback Social Events Benjamin C. PierceUniversity of Pennsylvania, Jonathan BellNortheastern University, Crista LopesUniversity 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. PierceUniversity of Pennsylvania, Jonathan BellNortheastern University, Crista LopesUniversity 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 | ||
Conference DayThu 27 AugDisplayed time zone: Eastern Time (US & Canada) change
Conference Day
Thu 27 AugDisplayed 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 FelleisenPLT @ 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 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 3h30mTutorial | Functional Software Architecture Tutorials Michael SperberActive 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 BoulytchevSt. 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éraudInria Media Attached | ||
11:30 - 13:00 | |||
11:30 30mTalk | 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 30mTalk | Describing Microservices using Modern Haskell (Experience Report) Haskell DOI | ||
12:30 30mTalk | 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 - 13:10 | |||
11:30 25mTalk | Tracking injectivity and nominality beyond abstraction ML Jacques GarrigueNagoya 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 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 | |||
14:00 4hSocial 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 3h30mTutorial | 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 30mTalk | A Low-Latency Garbage Collector for GHC (Demo) Haskell | ||
15:00 30mTalk | Relational Lenses as a Library (Demo) Haskell Rudi HornUniversity of Edinburgh File Attached | ||
15:30 30mTalk | Scripted Signal Functions Haskell David A. StuartNone DOI | ||
16:00 10mOther | PC Chair Report Haskell Tom SchrijversKU Leuven | ||
14:30 - 15:30 | Afternoon KeynoteminiKanren at miniKanren Chair(s): Jason HemannNortheastern University, United States | ||
14:30 60mKeynote | The Pill is in The Proof: Saving Lives with Logic miniKanren Matthew MightUniversity 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 AminHarvard University, Weixi MaIndiana University | ||
15:30 20mTalk | 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 20mTalk | 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 20mTalk | Some Novel miniKanren Synthesis Tasks miniKanren Pre-print | ||
16:30 20mTalk | 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 20mTalk | dxo: A System for Relational Algebra and Differentiation miniKanren Pre-print | ||
Conference DayFri 28 AugDisplayed time zone: Eastern Time (US & Canada) change
Conference Day
Fri 28 AugDisplayed 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 60mKeynote | The OCaml Platform OCaml Anil MadhavapeddyOCaml Labs | ||
06:30 30mTalk | 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 30mTalk | The final pieces of the OCaml documentation puzzle OCaml | ||
07:30 30mTalk | API migration: compare transformed OCaml Joseph HarrisonUniversity of Kent, UK, Steven VaroumasUniversity of Kent, Simon ThompsonUniversity of Kent, Reuben RoweUniversity College London | ||
08:00 30mTalk | 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 - 12:00 | |||
09:00 22mTalk | Asterius: bringing Haskell to WebAssembly HIW | ||
09:22 22mTalk | Multiple Home Units HIW | ||
10:00 35mTalk | Lightning Talks 1 HIW | ||
10:35 22mTalk | 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 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 SeriBernoulli 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 MidtgaardUniversity of Southern Denmark | ||
09:30 30mTalk | The ImpFS filesystem OCaml Tom RidgeUniversity of Leicester, UK | ||
10:00 30mTalk | Irmin v2 OCaml Clément PascuttoTarides, Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, Ioana CristescuINRIA, France, Craig FergusonTarides, Thomas GazagnaireTarides, Romain LiautaudTarides | ||
10:30 30mTalk | AD-OCaml: Algorithmic Differentiation for OCaml OCaml Markus MottlUnaffiliated | ||
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 ClaessenChalmers 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 SantosUniversity of Minho, Portugal / INESC TEC, Portugal, Jose Nuno OliveiraUniversity 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èsTweag I/O, France, Jean-Philippe BernardyUniversity of Gothenburg, Sweden, Richard A. EisenbergTweag I/O DOI | ||
12:30 30mTalk | 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 30mTalk | OCaml Under The Hood: SmartPy OCaml Sebastien MondetTQ Tezos | ||
12:00 30mTalk | A Declarative Syntax Definition for OCaml OCaml Luis Eduardo de Souza AmorimDelft University of Technology, Netherlands, Eelco VisserDelft 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 MontanariUniversidad Autónoma de Madrid File Attached | ||
12:30 10mTalk | Designing a Programming Environment Based on the Program Design Recipe (Lightning Talk) Scheme Junya NoseTokyo Institute of Technology, Youyou CongTokyo Institute of Technology, Hidehiko MasuharaTokyo Institute of Technology File Attached | ||
12:40 10mTalk | On Teaching Type Systems as Macros (Lightning Talk) Scheme Youyou CongTokyo Institute of Technology, Naoya FurudonoTokyo Institute of Technology, Hidehiko MasuharaTokyo Institute of Technology File Attached | ||
12:50 10mTalk | Programming with Petri Nets to Reason about Concurrency (Lightning Talk) Scheme julien lepillerYale 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 NapoliWell-Typed LLP, Ranjit JhalaUniversity of California at San Diego, USA, Andres LöhWell-Typed LLP, Niki VazouIMDEA 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 ChalmersMyrtle.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-ZabuskyUniversity of Pennsylvania, Joachim BreitnerDFINITY Foundation, Stephanie WeirichUniversity of Pennsylvania, Yao LiUniversity of Pennsylvania | ||
16:00 20mTalk | Closing HIW Ben GamariWell-Typed LLP | ||
14:00 - 15:00 | Keynote IIOCaml at OCaml Chair(s): Chris CasinghinoDraper 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 MadhavapeddyOCaml Labs | ||
14:00 - 17:30 | |||
14:00 3h30mTutorial | Building Multi-Language Tools with Cubix Tutorials James KoppelMassachusetts Institute of Technology, USA | ||
14:30 - 16:00 | |||
14:30 30mTalk | Staged Sums of Products Haskell Matthew PickeringUniversity of Bristol, UK, Andres LöhWell-Typed LLP, Nicolas WuImperial College London, UK DOI | ||
15:00 30mTalk | Eliminating Bugs with Dependent Haskell (Experience Report) Haskell Noam ZilbersteinFacebook, USA DOI | ||
15:30 30mTalk | Stitch: The Sound Type-Indexed Type Checker (Functional Pearl) Haskell Richard A. EisenbergTweag 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 NikishkinUnaffiliated File Attached | ||
15:30 - 17:30 | RecitationOCaml at OCaml Chair(s): Chris CasinghinoDraper 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 HarrisonUniversity of Kent, UK, Steven VaroumasUniversity of Kent, Simon ThompsonUniversity of Kent, Reuben RoweUniversity College London | ||
16:00 30mTalk | OCaml-CI : A Zero-Configuration CI OCaml Thomas LeonardOCaml Labs, Craig FergusonTarides, Kate DeplaixOCaml Labs, Magnus SkjegstadTarides and OCaml Labs, Anil MadhavapeddyOCaml 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 JafferOpsian and OCaml Labs, Sudha ParimalaIIT Madras, KC SivaramakrishnanIIT Madras, Tom KellyOCaml Labs, Anil MadhavapeddyOCaml 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 | ||