Filter Program
Dates
Rooms
Tracks
Badges
Your Program
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 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 | ||
09:00 - 10:30 | |||
09:00 30mDay opening | Welcome PLMW @ ICFP | ||
09:30 60mOther | 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 DOI | ||
10:07 23mTalk | AGR: A Rehearsal-to-Performance Workflow for Programming Audio Gestures in Max FARM Hongshuo Fan TAMU DOI | ||
09:00 - 10:30 | |||
09:00 30mTalk | Teaching Effect Handlers in the WildFPW (Paris)Remote HOPE Jiřà Beneš University of Tübingen | ||
09:30 30mTalk | Experience Report: Graph Rewriting with Lexical Effect HandlersFPW (Paris)Remote HOPE Marvin Borner University of Tübingen | ||
10:00 30mTalk | Higher-order fork, modallyFPW (Paris)Remote HOPE Aghilas Boussaa École normale supérieure - PSL, Wenhao Tang The University of Edinburgh, Sam Lindley University of Edinburgh | ||
09:40 - 10:30 | |||
09:40 25mTalk | JSON parsing in OxCaml: fast, but not too fast (Watch Party) OCaml Artem Pianykh Facebook London | ||
10:05 25mTalk | A new implementation of Short-paths (Watch Party) OCaml | ||
11:00 - 12:30 | |||
11:00 30mTalk | Towards Bottom-Up Enumeration in miniKanren via Pruning and MemoizationRemote miniKanren Nikolai Kudasov Innopolis University Pre-print | ||
11:30 15mOther | Discussion: Towards Bottom-Up Enumeration in miniKanren via Pruning and Memoization miniKanren | ||
11:45 30mTalk | Lightweight Runtime Security Policy Verification Using an Embeddable C++ miniKanren miniKanren File Attached | ||
12:15 15mOther | Discussion: Lightweight Runtime Security Policy Verification Using an Embedded C++ miniKanren miniKanren | ||
11:00 - 11:50 | |||
11:00 25mTalk | Towards a Benchmarking Service for OCaml (Watch Party) OCaml | ||
11:25 25mTalk | First Class Docs in OCaml (Watch Party) OCaml Jonathan Ludlam University of Cambridge | ||
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 DOI | ||
11:46 22mTalk | Prismriver: Formalization of Music Theory and Algorithmic Composition in Lean 4 FARM DOI | ||
12:08 22mTalk | Demo: The Reduction of Girard’s Paradox as Music FARM Isidore Mohr None DOI | ||
11:00 - 12:30 | |||
11:00 30mTalk | Practical Extensions for Graded Monads HOPE | ||
11:30 30mTalk | Towards Light-Weight Operational Reasoning for Languages with Binders, Categorically HOPE Sergey Goncharov University of Birmingham | ||
12:00 30mTalk | Orbifoldr: Classifying Wallpaper Groups via Functional Image Analysis in HaskellRemote HOPE | ||
14:00 - 15:30 | |||
14:00 30mTalk | 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:30 15mTalk | Discussion: All for one and none for all miniKanren | ||
14:45 30mTalk | Efficient Rational Unification for miniKanrenRemote miniKanren Eridan Domoratskiy Saint-Petersburg State University, Dmitri Boulytchev Saint Petersburg State University Pre-print File Attached | ||
15:15 15mOther | Discussion: Efficient Rational Unification for 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 45mTalk | Writing Makes the Researcher: The First Audience Is You PLMW @ ICFP Benjamin Delaware Purdue University | ||
14:45 45mTalk | Reduction Semantics and How to Read Them PLMW @ ICFP Robert Bruce Findler Northwestern University | ||
14:00 - 15:00 | |||
14:00 22mTalk | Demo: Drawing Algorithms as Modular Objects: A Framework for Procedurally Generated Visual Arts and Music FARM Xingyu Dong University of Pennsylvania, Daniel Průša Czech Technical University, Michael Wehar Bryn Mawr College, Chen Xu DOI | ||
14:22 38mTalk | The Art of Concert Programming FARM Jared Gentner None DOI | ||
14:00 - 15:30 | |||
14:00 30mTalk | Modular Storage Mode Analysis HOPE Martin Elsman University of Copenhagen | ||
14:30 30mTalk | Synthesizing Runners Using Copatterns HOPE | ||
15:00 30mTalk | A Logical Perspective on Capturing TypesRecorded HOPE Yichen Xu EPFL | ||
15:30 5mTalk | Closing HOPE | ||
16:00 - 17:30 | |||
16:00 60mKeynote | A Lean, Mean, miniKanren Machine miniKanren Jason Hemann Seton Hall University | ||
17:00 30mDemonstration | Demos of Attendee Programs and Open Mic 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 Derek Dreyer MPI-SWS, Joomy Korkut Bloomberg, Sam Tobin-Hochstadt Indiana University, Conrad Watt Nanyang Technological University, Mae Milano Princeton University | ||
19:30 - 21:00 | |||
19:30 45mKeynote | Sonification as (vs.) Program Music (Keynote) FARM Stephen A. Taylor University of Illinois Urbana-Champaign DOI | ||
20:15 5m | Girard's Paradox: Progression FARM Isidore Mohr None | ||
20:25 5m | Algorithmic Composition in Prismriver FARM | ||
20:30 10m | Shadows' Resonance FARM Hongshuo Fan TAMU | ||
20:40 5m | Untitled 23 FARM Dmitri Volkov Indiana University | ||
20:45 9m | Oscillectics FARM | ||
20:54 6m | Kaleidophone in Digital for Algorithmic Composition and Visualization FARM | ||
Tue 25 AugDisplayed time zone: Eastern Time (US & Canada) change
Tue 25 Aug
Displayed time zone: Eastern Time (US & Canada) change
08:55 - 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. | ||
08:55 5mMeeting | Welcome ICFP Keynotes Sam Tobin-Hochstadt Indiana University | ||
09:00 60mKeynote | Deterministic Concurrency ICFP Keynotes | ||
17:00 - 17:15 | |||
17:00 15mIndustry talk | Industrial Sponsor Introductions ICFP Papers | ||
17:30 - 21:30 | |||
17:30 4hSocial Event | Poster Reception and Exhibits ICFP Papers | ||
19:30 - 21:30 | |||
19:30 2hDinner | Women in PL Dinner Diversity, Equity, and Inclusion | ||
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 | ||
12:00 - 13:30 | |||
12:00 90mLunch | LGBTQ@ICFP Lunch Diversity, Equity, and Inclusion | ||
13:30 - 14:45 | |||
13:30 18mTalk | Bimodels and Biorthogonality for Abstract Machines ICFP Papers DOI | ||
13:48 18mTalk | Let It Be Optimized: Building Multi-Stage Evaluators with Let-Insertion and Optimizations in Small Pieces (Functional Pearl) ICFP Papers DOI | ||
14:07 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 DOI | ||
14:26 18mTalk | Unscanning by Möbius Inversion (Functional Pearl)Remote ICFP Papers Keisuke Nakano Tohoku University DOI | ||
14:45 - 15:15 | |||
14:45 6mPoster | Better Safe and Sorry: Tabular Types for Dynamic Languages ICFP SRC Vincent H. Chan University at Buffalo, SUNY, MatÃas Toro University of Chile, Qianchuan Ye University at Buffalo, SUNY | ||
14:51 6mPoster | Coverage Types Modulo Equivalences ICFP SRC | ||
14:57 6mPoster | JavaScript Regular Expression Matching is PSPACE-Complete ICFP SRC | ||
15:03 6mPoster | QuickerChick ICFP SRC Ivan Mladenov University of Maryland, College Park, Alperen Keles University of Maryland at College Park, Leonidas Lampropoulos University of Maryland at College Park | ||
15:09 6mPoster | Incremental Property-Based Testing ICFP SRC | ||
15:45 - 17:15 | |||
15:45 10mMeeting | GC report ICFP Papers Sam Tobin-Hochstadt Indiana University | ||
15:55 10mMeeting | PC-chair report ICFP Papers Manuel Serrano Inria; Université Côte d’Azur | ||
16:05 10mMeeting | Most Influential Paper Award: ICFP 2016 ICFP Papers Sam Tobin-Hochstadt Indiana University | ||
16:15 10mMeeting | SIGPLAN Achievement Award ICFP Papers Sam Tobin-Hochstadt Indiana University | ||
16:25 10mMeeting | SRC awards ICFP Papers Kimball Germane Brigham Young University | ||
16:35 5mMeeting | JFP@ICFP ICFP Papers Derek Dreyer MPI-SWS | ||
16:40 10mMeeting | ICFP 2027 announcement ICFP Papers | ||
16:50 25mMeeting | Programming Contest report and winners ICFP Papers | ||
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:48 - 12:00 | |||
10:48 18mTalk | Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report) ICFP Papers Zoe Paraskevopoulou National Technical University of Athens DOI | ||
11:06 18mTalk | Proofs Promptly: Proof-Oriented Programming with AI Agents (Experience Report)Remote ICFP Papers Eleftherios Ioannidis Microsoft Research, Nikhil Swamy Microsoft Research, Gabriel Ebner Microsoft Research, Matthai Philipose Microsoft Research, Tahina Ramananandro Microsoft Research DOI | ||
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 DOI | ||
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 DOI | ||
12:00 - 13:30 | |||
12:00 90mLunch | URM@ICFP Lunch Diversity, Equity, and Inclusion | ||
13:55 - 15:00 | Thursday Afternoon SessionLOPSTR+PPDP at HO221 Presidents Room Chair(s): William E. Byrd University of Alabama at Birmingham, Theresa Swift Johns Hopkins Applied Physics Laboratory | ||
13:55 5mDay opening | Opening Greetings and Announcements (Day 1) LOPSTR+PPDP Theresa Swift Johns Hopkins Applied Physics Laboratory, William E. Byrd University of Alabama at Birmingham | ||
14:00 60mKeynote | Functional / Logic Programming in VerseKeynote LOPSTR+PPDP Stephanie Weirich University of Pennsylvania | ||
15:30 - 17:30 | Thursday Afternoon Session 2LOPSTR+PPDP at HO221 Presidents Room Chair(s): Kyle Dewey California State University, Northridge | ||
15:30 30mTalk | From Constraints to Cognition: A Hybrid Framework for Adaptive, Explainable SchedulingRemoteBest Paper Award 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 | ||
16:00 30mTalk | Strong and NAF Negations in Answer Set ProgrammingRemote LOPSTR+PPDP Yuliya Lierler University of Nebraska | ||
16:30 30mTalk | Convenient Algebraic Programming with Coercive Subtyping LOPSTR+PPDP | ||
15:30 - 17:00 | Effects, Semantics, and Program AnalysisICFP Papers at IP126 Auditorium Chair(s): Ben Greenman University of Utah | ||
15:30 18mTalk | HMCFA: A Precise and Practical Big-Step Control Flow Analysis for Effect HandlersRemote ICFP Papers DOI | ||
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 DOI | ||
16:06 18mTalk | Demand-on-Demand Control-Flow Analysis ICFP Papers DOI | ||
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 DOI | ||
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 DOI | ||
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 Editors (Keynote)Keynote Haskell DOI | ||
10:15 15mCoffee break | Break Haskell | ||
09:00 - 10:30 | |||
09:00 5mDay opening | Welcome and Opening Remarks ML Family Sam Westrick New York University | ||
09:05 55mKeynote | The Rhombus Programming LanguageKeynote ML Family Matthew Flatt University of Utah | ||
09:00 - 10:30 | Morning SessionLOPSTR+PPDP at IP137 Kelley Chair(s): William E. Byrd University of Alabama at Birmingham, Theresa Swift Johns Hopkins Applied Physics Laboratory | ||
09:00 5mDay opening | Opening Greetings and Announcements (Day 2) LOPSTR+PPDP Theresa Swift Johns Hopkins Applied Physics Laboratory, William E. Byrd University of Alabama at Birmingham | ||
09:05 60mKeynote | What Is "Quantum" About Quantum Computing?Keynote LOPSTR+PPDP Amr Sabry Indiana University | ||
09:00 - 10:30 | |||
09:00 10mDay opening | Welcome Erlang | ||
09:10 80mKeynote | Actor Capabilities for Controlled Actor Interactions (Keynote)Keynote Erlang Colin S. Gordon Drexel University DOI | ||
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 DOI | ||
11:30 30mTalk | Xeus-Haskell: Interactive Haskell Computing in the Browser Haskell Masaya Taniguchi RIKEN AIP | ||
12:00 30mTalk | Turning Parser Errors into Suggestions for REPL-Driven DSLs (Functional Pearl) 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 DOI | ||
11:00 - 12:30 | |||
11:30 30mTalk | Testing Incomplete Programs in OCaml ML Family | ||
12:00 30mTalk | Self-Tagging Numbers ML Family John Reppy University of Chicago, Ben Wakefield University of Chicago, Byron Zhong University of Chicago | ||
11:00 - 12:30 | |||
11:00 30mTalk | Elements of Logic Programming in a Concatenative Functional LanguageRemote LOPSTR+PPDP Attila Egri-Nagy Akita International University | ||
11:30 30mTalk | Tempo: Reconstructing Synchronous Reactive Programming with OCaml 5 EffectsRemoteRecorded 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 ReferencesRemote 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 Link to publication DOI File Attached | ||
11:30 30mTalk | Set-Theoretic Type Checking of Beginner Erlang Code: A Retrospective StudyRemote Erlang Albert Schimpf University of Kaiserslautern-Landau, Stefan Wehr Offenburg University of Applied Sciences, Annette Bieniusa RPTU Kaiserslautern-Landau DOI | ||
12:00 30mTalk | Towards Exact Semantic Equivalence of Erlang BEAM Constructs: Lessons from Advanced Emulation and DecompilationRemote Erlang Link to publication DOI File Attached | ||
14:00 - 15:30 | |||
14:00 90mTalk | Metaprogramming in Rhombus ICFP Tutorials Pre-print | ||
14:00 - 15:30 | |||
14:00 30mTalk | CloudMicroHaskell: Direct-Style Distributed Haskell via Runtime Graph Serialisation Haskell DOI | ||
14:30 30mTalk | Tikka: An Interpreter and Debugger for a Pedagogical Subset of HaskellRemote Haskell Alex Hobbs Department of Computer Science, University of Warwick, UK, Alex Dixon Department of Computer Science, University of Warwick, UK DOI | ||
15:00 10mTalk | Lightning Talk: Modern Haskell profiling with Haskell Inspector Haskell Luite Stegeman ICAN Group | ||
15:10 10mTalk | Lightning Talk: Prefix Matching using Classes that Count Haskell Jan-Willem Maessen Nectry Inc. | ||
14:00 - 15:30 | |||
14:00 30mTalk | Functional Programming with Serialized DataInvited Talk ML Family Michael Vollmer University of Kent | ||
14:30 30mTalk | Language Support for Property-Based TestingInvited Talk ML Family Harrison Goldstein University at Buffalo, SUNY | ||
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 LoRaRemote Erlang Daniel Ferenczi Eötvös Loránd University, Gergely Ruda evosoft Hungary Kft., Melinda Tóth Eötvös Loránd University DOI | ||
14:30 30mTalk | Green Benchmarking of BEAM LanguagesRemote Erlang Youssef Gharbi 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 Link to publication DOI File Attached | ||
15:00 30mTalk | Modern Erlang Teaching from Code Refactoring to Actor System VerificationRemote Erlang Sergey Staroletov Polzunov Altai State Technical University DOI | ||
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 35mTalk | Arbiter: Distributed Job Queues using Haskell and PostgreSQLInvited Haskell | ||
16:35 10mTalk | Lightning Talk: Fixen: A Fixed-Point Generator for Haskell Haskell Michael D. Adams National University of Singapore | ||
16:45 10mTalk | Lightning Talk: What's Next with Freer Arrows? Haskell Yao Li Portland State University | ||
16:55 10mTalk | Lightning Talk: Could coapplicatives contain comonads? Haskell J. A. Carr University of Chicago | ||
17:05 10mTalk | Lightning Talk: Morphosyntactic Programming: Case, Mood, and Type-Directed Disambiguation for Turkish-Like Syntax Haskell Joomy Korkut Bloomberg | ||
17:15 10mTalk | Lightning Talk: Sticks: A (wiki) tool for semantic thought (keywords: hakyll pandoc typst linguistics come to my talk pls) Haskell JJ University of British Columbia | ||
16:00 - 17:30 | |||
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 Pre-print | ||
17:00 30mPanel | LOPSTR+PPDP Discussion LOPSTR+PPDP | ||
16:00 - 17:30 | |||
16:00 30mTalk | Reactor Under the Hood: Building a Graph-Based Saga Orchestrator in Elixir Erlang James Harton Alembic | ||
16:30 30mTalk | Silica: A functional systems language for modern chips, modern tools, and honest boundaries Erlang | ||
17:00 10mDay closing | Closing remarks Erlang | ||
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)Keynote Haskell DOI | ||
10:15 15mCoffee break | Break Haskell | ||
09:00 - 10:30 | |||
09:30 60mKeynote | Rhombus: The Non-shrubbery Parts (Keynote) Scheme Matthew Flatt University of Utah DOI | ||
09:00 - 10:30 | Morning SessionLOPSTR+PPDP at IP137 Kelley Chair(s): William E. Byrd University of Alabama at Birmingham, Theresa Swift Johns Hopkins Applied Physics Laboratory | ||
09:00 5mDay opening | Opening Greetings and Announcements (Day 3) LOPSTR+PPDP Theresa Swift Johns Hopkins Applied Physics Laboratory, William E. Byrd University of Alabama at Birmingham | ||
09:05 60mKeynote | Proof-Carrying Code For the Age of AI: Machine-Checked Guarantees from Specifications to ExecutablesKeynote LOPSTR+PPDP Zoe Paraskevopoulou National Technical University of Athens | ||
09:30 - 10:30 | |||
09:30 60mKeynote | Functional Mechanical Sympathy (Keynote)Remote FUNARCH DOI | ||
11:00 - 12:30 | |||
11:00 30mTalk | A Cost-Aware Probability Monad for Liquid HaskellRemote Haskell DOI 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 DOI | ||
12:00 10mTalk | Lightning Talk: Formalizing explicit alpha-equivalence Haskell Aaron Stump Boston College | ||
12:10 10mTalk | Lightning Talk: Programming with Extensible Recursive Datatypes Haskell J. Garrett Morris University of Iowa | ||
12:20 10mTalk | Lightning Talk: Testing smart contracts with QuickCheck Haskell John Hughes Chalmers University of Technology, Sweden | ||
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 DOI | ||
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 DOI | ||
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 OptimizationsRemote 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 workflowRemote 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 45mExperience report | Local-First Distributed Configuration (Experience Report)Remote FUNARCH Michael Sperber Active Group GmbH DOI | ||
14:00 - 15:30 | Afternoon SessionHaskell at IP126 Auditorium Chair(s): Lindsey Kuper University of California, Santa Cruz | ||
14:00 20mTalk | Program chair's report Haskell Lindsey Kuper University of California, Santa Cruz | ||
14:20 70m | Unconferencing session Haskell | ||
14:00 - 15:30 | |||
14:00 30mTalk | The R7RS-Large Roadmap (Invited Talk) Scheme Peter McGoron Georgia Institute of Technology DOI | ||
14:30 30mTalk | An Array-Oriented Language via the Design Recipe Scheme DOI | ||
15:00 30mTalk | Using the Design Recipe in Theory of Computation Scheme DOI | ||
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 45mTalk | From Lambda to Ledger: An Architectural Comparison of Plinth and Plutarch FUNARCH DOI | ||
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 DOI | ||
16:00 - 17:30 | |||
16:00 - 17:30 | Afternoon Session 2LOPSTR+PPDP at IP137 Kelley Chair(s): William E. Byrd University of Alabama at Birmingham, Theresa Swift Johns Hopkins Applied Physics Laboratory | ||
16:00 90mPanel | Coding Agents: New opportunities for formal methods? LOPSTR+PPDP | ||
16:00 - 17:30 | |||
16:00 25mTalk | Functional Architecture is Algebraic Architecture FUNARCH Jeffrey Young Canonical | ||
16:30 25mTalk | The Future of FUNARCH (2026 edition) FUNARCH Jeffrey Young Canonical | ||