Filter Program
Dates
Rooms
Tracks
Badges
Your Program
This program is tentative and subject to change.
Mon 24 AugDisplayed time zone: Eastern Time (US & Canada) change
Mon 24 Aug
Displayed time zone: Eastern Time (US & Canada) change
09:00 - 10:30 | |||
09:00 - 10:30 | |||
09:00 30mDay opening | Welcome PLMW @ ICFP | ||
09:30 30mOther | Icebreaker PLMW @ ICFP | ||
09:00 - 10:30 | |||
09:00 15mDay opening | Welcome from the Chairs FARM Mae Milano Princeton University | ||
09:15 45mTalk | Composition: Building Community with Arts, Math, and Code (Experience Report) FARM | ||
10:07 23mTalk | Demo: Drawing Algorithms As Modular Objects FARM Xingyu Dong University of Pennsylvania, Daniel Průša Czech Technical University, Michael Wehar Bryn Mawr College, Chen Xu | ||
09:00 - 10:30 | |||
09:00 - 10:30 | |||
09:00 5mDay opening | Opening greetings and announcements miniKanren | ||
09:05 55mTutorial | Introduction to relational programming in miniKanren miniKanren | ||
10:00 30mOther | Programming Challenge to Attendees miniKanren | ||
11:00 - 12:30 | |||
11:00 90mTalk | How to Write Papers and Give Talks that People Can Follow PLMW @ ICFP Derek Dreyer MPI-SWS | ||
11:00 - 12:30 | |||
11:00 46mTalk | CounterChoice: Counterpoint Composition in Dusa with a Firmus Foundation FARM Ahmet Yigit Erdem Institute of Science Tokyo, Middle East Technical University, Ari Prakash Northeastern University, Carlo Angiuli Indiana University, Rose Bohrer National Institute of Advanced Industrial Science and Technology (AIST), Japan, James McCann Carnegie Mellon University, Chris Martens Northeastern University, Youyou Cong Institute of Science Tokyo | ||
11:46 22mTalk | Prismriver: Formalization of Music Theory and Algorithmic Composition in Lean 4 FARM | ||
12:08 22mTalk | Demo: The Reduction of Girard's Paradox as Music FARM Isidore Mohr None | ||
11:00 - 12:30 | |||
11:00 25mTalk | Efficient Rational Unification for miniKanren miniKanren Eridan Domoratskiy Saint-Petersburg State University, Dmitri Boulytchev Saint Petersburg State University Pre-print | ||
11:25 20mOther | Discussion: Efficient Rational Unification for miniKanren miniKanren | ||
11:45 25mTalk | Lightweight Runtime Security Policy Verification Using an Embeddable C++ miniKanren miniKanren File Attached | ||
12:10 20mOther | Discussion: Lightweight Runtime Security Policy Verification Using an Embedded C++ miniKanren miniKanren | ||
14:00 - 15:30 | |||
14:00 90mTalk | Hacking Choreographic Programming in Haskell ICFP Tutorials Gan Shen University of California at Santa Cruz | ||
14:00 - 15:30 | |||
14:00 22mTalk | AGR: A Rehearsal-to-Performance Workflow for Programming Audio Gestures in Max FARM Hongshuo Fan TAMU | ||
14:22 38mTalk | The Art of Concert Programming FARM Jared Gentner None | ||
14:00 - 15:30 | |||
14:00 - 15:30 | |||
14:00 25mTalk | All for one and none forall: Compiling polymorphic relations without monomorphization miniKanren Dmitri Volkov Indiana University, Chung-chieh Shan Indiana University, Yafei Yang Indiana University Pre-print | ||
14:25 20mTalk | Discussion: All for one and none for all miniKanren | ||
14:45 25mTalk | Towards Bottom-Up Enumeration in miniKanren via Pruning and Memoization miniKanren Nikolai Kudasov Innopolis University Pre-print | ||
15:10 20mOther | Discussion: Towards Bottom-Up Enumeration in miniKanren via Pruning and Memoization miniKanren | ||
16:00 - 17:30 | |||
16:00 90mTalk | Hacking Choreographic Programming in Haskell ICFP Tutorials Gan Shen University of California at Santa Cruz | ||
16:00 - 17:30 | |||
16:00 90mPanel | Career Pathways in Programming Languages Research PLMW @ ICFP | ||
16:00 - 17:30 | |||
16:00 60mKeynote | Keynote title: TBA miniKanren | ||
17:00 30mDemonstration | Demos of Attendee Programs and Open Mic miniKanren | ||
Tue 25 AugDisplayed time zone: Eastern Time (US & Canada) change
Tue 25 Aug
Displayed time zone: Eastern Time (US & Canada) change
09:00 - 10:00 | Keynote: Edward LeeICFP Keynotes at IP126 Auditorium Chair(s): Manuel Serrano Inria; Université Côte d’Azur 50-minute talk followed by 10 minutes of questions. | ||
09:00 60mKeynote | Deterministic Concurrency ICFP Keynotes | ||
10:30 - 12:00 | Types, Testing, and Data StructuresICFP Papers at IP126 Auditorium Chair(s): Steve Zdancewic University of Pennsylvania | ||
10:30 18mTalk | Inlining as a space optimization: a simple time- and space-invariant implementation of the weak lambda-calculusRemote ICFP Papers Thibaut Balabonski LMF, CNRS, Université Paris-Saclay | ||
10:48 18mTalk | First-Class Constrained Types: Elaboration, Type Inference, Approximation, and a Characterization of Termination ICFP Papers Chun Kit Lam The Hong Kong University of Science and Technology (HKUST), Florent Ferrari-Dominguez ENS de Lyon, Lionel Parreaux HKUST (The Hong Kong University of Science and Technology) | ||
11:06 18mTalk | Programmable Property-Based Testing ICFP Papers Alperen Keles University of Maryland at College Park, Justine Frank University of Maryland, College Park, Ceren Mert University of Maryland, College Park, Harrison Goldstein University at Buffalo, SUNY, Leonidas Lampropoulos University of Maryland at College Park | ||
11:24 18mTalk | A Catenable, Splittable, Transient Sequence Data Structure ICFP Papers | ||
Wed 26 AugDisplayed time zone: Eastern Time (US & Canada) change
Wed 26 Aug
Displayed time zone: Eastern Time (US & Canada) change
09:00 - 10:00 | Keynote: Lindsey KuperICFP Keynotes at IP126 Auditorium Chair(s): Sam Tobin-Hochstadt Indiana University 50-minute talk followed by 10 minutes of questions. | ||
09:00 60mKeynote | Interpreters everywhere! ICFP Keynotes | ||
13:30 - 15:00 | |||
13:30 18mTalk | Bimodels and Biorthogonality for Abstract Machines ICFP Papers | ||
13:48 18mTalk | Let It Be Optimized: Building Multi-Stage Evaluators with Let-Insertion and Optimizations in Small Pieces (Functional Pearl) ICFP Papers | ||
14:06 18mTalk | Animated Pictures for Slide Presentations (Functional Pearl): From the Shallows to the Depths of a Domain-Specific Language ICFP Papers Oliver Flatt University of Washington, Robert Bruce Findler Northwestern University, Matthew Flatt University of Utah | ||
14:24 18mTalk | Unscanning by Möbius Inversion (Functional Pearl) ICFP Papers Keisuke Nakano Tohoku University | ||
15:30 - 17:00 | |||
Thu 27 AugDisplayed time zone: Eastern Time (US & Canada) change
Thu 27 Aug
Displayed time zone: Eastern Time (US & Canada) change
09:00 - 10:00 | Keynote: Daan LeijenICFP Keynotes at IP126 Auditorium Chair(s): Robert Bruce Findler Northwestern University 50-minute talk followed by 10 minutes of questions. | ||
09:00 60mKeynote | Efficient strong functional programming with effects and compiler guided reference counting ICFP Keynotes | ||
10:30 - 12:00 | |||
10:30 18mTalk | RunbookFX: Type- and Effect-Safe LLM Synthesis for Executable Incident Diagnosis and MitigationRemote ICFP Papers Yifan Xiao Peking University, Shijie Li China Southern Power Grid Company Limited, Yuhao Ge China Southern Power Grid Company Limited | ||
10:48 18mTalk | Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)Remote ICFP Papers Zoe Paraskevopoulou National Technical University of Athens | ||
11:06 18mTalk | Proofs Promptly: Proof-Oriented Programming with AI Agents (Experience Report) ICFP Papers Eleftherios Ioannidis Microsoft Research, Nikhil Swamy Microsoft Research, Gabriel Ebner Microsoft Research, Matthai Philipose Microsoft Research, Tahina Ramananandro Microsoft Research | ||
11:24 18mTalk | Programming Backpropagation with Reverse Handlers for Arrows ICFP Papers Takahiro Sanada Fukui Prefectural University, Keisuke Hoshino Research Institute for Mathematical Sciences, Kyoto University, Kenshin Hirai Research Institute for Mathematical Sciences, Kyoto University, Shin-ya Katsumata Kyoto Sangyo University | ||
11:42 18mTalk | On Recursion in Graded Modal Type Theory ICFP Papers Oskar Eriksson Department of Computer Science and Engineering, University of Gothenburg and Chalmers University of Technology, Gothenburg, Sweden, Andreas Abel Gothenburg University, Nils Anders Danielsson University of Gothenburg | ||
14:00 - 17:30 | |||
14:00 90mKeynote | Keynote 1 (TBA) LOPSTR+PPDP | ||
15:30 30mCoffee break | Coffee Break LOPSTR+PPDP | ||
16:00 30mTalk | Strong and NAF Negations in Answer Set Programming LOPSTR+PPDP Yuliya Lierler University of Nebraska | ||
16:30 30mTalk | From Constraints to Cognition: A Hybrid Framework for Adaptive, Explainable Scheduling LOPSTR+PPDP Stefania Costantini Dipartimento di Ingegneria e Scienze dell'Informazione eMatematica, Univ. dell'Aquila, Valentina Pitoni Univaq, Andrea Formisano Università di Perugia , Lorenzo De Lauretis Univaq | ||
17:00 30mTalk | Convenient Algebraic Programming with Coercive Subtyping LOPSTR+PPDP | ||
15:30 - 17:00 | Effects, Semantics, and Program AnalysisICFP Papers at IP126 Auditorium Chair(s): Benjamin Delaware Purdue University | ||
15:30 18mTalk | HMCFA: A Precise and Practical Big-Step Control Flow Analysis for Effect HandlersRemote ICFP Papers | ||
15:48 18mTalk | When Types Intersect and Effects Get Handled ICFP Papers Stefano Catozi LIPN, Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis, Taro Sekiyama National Institute of Informatics | ||
16:06 18mTalk | Demand-on-Demand Control-Flow Analysis ICFP Papers | ||
16:24 18mTalk | Adequacy for Predicate Transformer Semantics ICFP Papers Kazuki Watanabe National Institute of Informatics; SOKENDAI, Mirai Ikebuchi Kyoto University, Mayuko Kori Research Institute for Mathematical Sciences, Kyoto University | ||
16:42 18mTalk | Misquoted No More: Securely Extracting F* Programs with IO ICFP Papers Cezar-Constantin Andrici MPI-SP, Abigail Pribisova MPI-SP and MPI-SWS, Danel Ahman University of Tartu, Cătălin Hriţcu MPI-SP, Exequiel Rivas Tallinn University of Technology; Ahrefs, Théo Winterhalter INRIA | ||
Fri 28 AugDisplayed time zone: Eastern Time (US & Canada) change
Fri 28 Aug
Displayed time zone: Eastern Time (US & Canada) change
09:00 - 10:30 | Morning SessionHaskell at IP126 Auditorium Chair(s): Lindsey Kuper University of California, Santa Cruz | ||
09:00 5mDay opening | Welcome Haskell Lindsey Kuper University of California, Santa Cruz | ||
09:05 70mKeynote | The Next 700 Block-Based EditorsKeynote Haskell | ||
10:15 15mCoffee break | Break Haskell | ||
09:00 - 10:30 | |||
09:00 - 10:30 | |||
09:00 90mKeynote | Keynote 2 (TBA) LOPSTR+PPDP | ||
09:00 - 10:30 | |||
09:00 10mDay opening | Welcome Erlang | ||
09:10 80mKeynote | Actor Capabilities for Controlled Actor InteractionsKeynote Erlang Colin Gordon Drexel University | ||
11:00 - 12:30 | |||
11:00 30mTalk | Evaluating Shrinking (Experience Report) Haskell Alperen Keles University of Maryland at College Park, George Miao University of Maryland, College Park, Leonidas Lampropoulos University of Maryland at College Park | ||
11:30 30mTalk | Xeus-Haskell: Interactive Haskell Computing in the Browser Haskell Masaya Taniguchi RIKEN AIP | ||
12:00 30mTalk | Functional Pearl: Turning Parser Errors into Suggestions for REPL-Driven DSLs Haskell Matthías Páll Gissurarson Chalmers University of Technology, Sweden, Elisabet Lobo-Vesga Chalmers University of Technology, Sweden, Alejandro Russo Chalmers University of Technology; University of Gothenburg | ||
11:00 - 12:30 | |||
11:00 30mTalk | Elements of Logic Programming in a Concatenative Functional Language LOPSTR+PPDP Attila Egri-Nagy Akita International University | ||
11:30 30mTalk | Tempo: Reconstructing Synchronous Reactive Programming with OCaml 5 Effects LOPSTR+PPDP Frédéric Dabrowski Université d'Orléans | ||
12:00 30mTalk | Wren: A Fast Logic Programming eDSL With Host Language Garbage Collection LOPSTR+PPDP | ||
11:00 - 12:30 | |||
11:00 30mTalk | A Mechanised Semantics of Erlang's References Erlang Dániel Lukács Eötvös Loránd University, Péter Bereczky Eötvös Loránd University, Dániel Horpácsi Eötvös Loránd University | ||
11:30 30mTalk | Set-Theoretic Type Checking of Beginner Erlang Code: A Retrospective Study Erlang Albert Schimpf University of Kaiserslautern-Landau, Stefan Wehr Offenburg University of Applied Sciences, Annette Bieniusa RPTU Kaiserslautern-Landau | ||
12:00 30mTalk | Towards Exact Semantic Equivalence of Erlang BEAM constructs: Lessons from Advanced Emulation and Decompilation Erlang | ||
14:00 - 15:30 | |||
14:00 90mTalk | Metaprogramming in Rhombus ICFP Tutorials Pre-print | ||
14:00 - 15:30 | Afternoon SessionHaskell at IP126 Auditorium Chair(s): Lindsey Kuper University of California, Santa Cruz | ||
14:00 30mTalk | CloudMicroHaskell: Direct-Style Distributed Haskell via Runtime Graph Serialisation Haskell | ||
14:30 30mTalk | Tikka: An Interpreter and Debugger for a Pedagogical Subset of Haskell Haskell Alex Hobbs Department of Computer Science, University of Warwick, UK, Alex Dixon Department of Computer Science, University of Warwick, UK | ||
15:00 30m | Lightning Talk Session Haskell | ||
14:00 - 15:30 | |||
14:00 - 15:30 | |||
14:00 30mTalk | Implementing Grassroots Logic Programs with Multiagent Transition Systems and AI LOPSTR+PPDP Ehud Shapiro London School of Economics | ||
14:30 30mTalk | PAARL: An Interactive System for Policy-Aware Planning in Autonomous Agents (System Description) LOPSTR+PPDP | ||
15:00 30mTalk | Backwards Compatibility of Conditional Literals LOPSTR+PPDP Zachary Hansen Boise State University | ||
14:00 - 15:30 | |||
14:00 30mTalk | EMoL: Erlang Messaging and Monitoring over LoRa Erlang Daniel Ferenczi Eötvös Loránd University, Gergely Ruda evosoft Hungary Kft., Melinda Tóth Eötvös Loránd University | ||
14:30 30mTalk | Green Benchmarking of BEAM Languages Erlang Youssef Gharbi ELTE Eötvös Loránd University, Melinda Tóth Eötvös Loránd University, István Bozó Eötvös Loránd University | ||
15:00 30mTalk | Modern Erlang Teaching from Code Refactoring to Actor System Verification Erlang Sergey Staroletov Polzunov Altai State Technical University | ||
16:00 - 17:30 | |||
16:00 90mTalk | Metaprogramming in Rhombus ICFP Tutorials Pre-print | ||
16:00 - 17:30 | Afternoon Session 2Haskell at IP126 Auditorium Chair(s): Lindsey Kuper University of California, Santa Cruz | ||
16:00 60mTalk | Enterprise Haskell at H-E-BInvited Haskell | ||
16:00 - 17:30 | |||
16:00 30mTalk | Deconstructed Proto-Quipper: A Rational Reconstruction LOPSTR+PPDP Ryan Kavanagh Université du Québec à Montréal, Chuta Sano McGill University, Brigitte Pientka McGill University | ||
16:30 30mTalk | Deriving a Kronecker-Free Functional Quantum Simulator LOPSTR+PPDP Martin Elsman University of Copenhagen | ||
17:00 30mPanel | LOPSTR+PPDP Discussion LOPSTR+PPDP | ||
Sat 29 AugDisplayed time zone: Eastern Time (US & Canada) change
Sat 29 Aug
Displayed time zone: Eastern Time (US & Canada) change
09:00 - 10:30 | Morning SessionHaskell at IP126 Auditorium Chair(s): Lindsey Kuper University of California, Santa Cruz | ||
09:00 5mDay opening | Welcome (Day 2) Haskell Lindsey Kuper University of California, Santa Cruz | ||
09:05 70mKeynote | What have we learned about Dependently Typed Programming from Haskell?Keynote Haskell | ||
10:15 15mCoffee break | Break Haskell | ||
09:00 - 10:30 | |||
09:30 60mKeynote | Rhombus: The Non-Shrubbery Parts Scheme Matthew Flatt University of Utah | ||
09:00 - 10:30 | |||
09:00 90mKeynote | Keynote 3 (TBA) LOPSTR+PPDP | ||
09:00 - 10:30 | |||
09:30 60mKeynote | Functional Mechanical Sympathy FUNARCH | ||
11:00 - 12:30 | |||
11:00 30mTalk | A Cost-Aware Probability Monad for Liquid Haskell Haskell Pre-print | ||
11:30 30mTalk | Coercive Subtyping for Implicit Functorial Programming Haskell Ryan Doenges Boston College, Caden Parajuli Boston College, Ayden Lamparski Boston College, Ke Wu Johns Hopkins University, Aaron Stump Boston College | ||
12:00 30mTalk | Program chair's report Haskell Lindsey Kuper University of California, Santa Cruz | ||
11:00 - 12:30 | |||
11:00 30mTalk | A Call-by-push-value Scheme Scheme Max S. New University of Michigan | ||
11:30 30mTalk | Regions as Continuation Marks Scheme Paulette Koronkevich University of British Columbia, William J. Bowman University of British Columbia | ||
12:00 30mTalk | An Incremental Approach to JIT Construction Scheme Shaurya Raswan University of California at San Diego, USA, Mark Barbone University of California at San Diego, Nico Lehmann University of Chile, Joe Gibbs Politz UC San Diego | ||
11:00 - 12:30 | |||
11:00 30mTalk | A Typed and Unified Reflection for Shift and Shift0 LOPSTR+PPDP | ||
11:30 30mTalk | Combining Small-Step and Big-Step Semantics to Verify Loop Optimizations LOPSTR+PPDP David Knothe FZI Research Center for Information Technology, Oliver Bringmann FZI Research Center for Information Technology | ||
12:00 30mTalk | Certified hardware for regexp matching: A rocq library and its workflow LOPSTR+PPDP Julin Shaji Indian Institute of Technology Palakkad, Piyush Kurur Indian Institute of Technology Palakkad, Sandeep Chandran Indian Institute of Technology Palakkad | ||
11:00 - 12:30 | |||
11:00 45mTalk | From Lambda to Ledger: An Architectural Comparison of Plinth and Plutarch FUNARCH | ||
14:00 - 15:30 | |||
14:00 - 15:30 | |||
14:00 30mTalk | The R7RS-Large Roadmap Scheme Peter McGoron Georgia Institute of Technology | ||
14:30 30mTalk | An Array-Oriented Language via the Design Recipe Scheme | ||
15:00 30mTalk | Using the Design Recipe in Theory of Computation Scheme | ||
14:00 - 15:30 | |||
14:00 30mTalk | StageML: Partial Evaluation for Multi-Tenant MoE-LoRA Inference LOPSTR+PPDP | ||
14:30 30mTalk | Complex Autonomous UAV Task Execution and Decision-Making Using s(CASP) LOPSTR+PPDP Keegan Kimbrell University of Texas at Dallas, USA, Alexis R Tudor University of Texas at Dallas, Peter Vu University of Texas at Dallas, Trevor Bihl Ohio University, Doug Slattery SYBOR Tech, Inc., Gopal Gupta University of Texas at Dallas | ||
15:00 30mTalk | Vehicle with Time: Signal First-Order Logic for Closed-Loop Controller Synthesis LOPSTR+PPDP Gusts Gustavs Grīnbergs IT University of Copenhagen, Alessandro Bruni IT University of Copenhagen, Matthew L. Daggitt University of Western Australia | ||
14:00 - 15:30 | |||
14:00 45mExperience report | Local-First Distributed Configuration (Experience Report) FUNARCH Michael Sperber Active Group GmbH | ||
14:45 45mTalk | Functional State Machines in Rust: Typestate and Newtype Patterns (Experience Report) FUNARCH Leon Heuer NORDAKADEMIE gAG Hochschule der Wirtschaft, Falk Woldmann Lu Otto GmbH & Co. KGaA, Jan Haase NORDAKADEMIE gAG Hochschule der Wirtschaft | ||
16:00 - 17:30 | |||
16:00 - 17:30 | |||
16:00 90mPanel | Coding Agents: New opportunities for formal methods? LOPSTR+PPDP | ||
16:00 - 17:30 | |||