LOPSTR+PPDP 2026
2026-08-27..2026-08-29
Indianapolis, United States
as the organisers put it
The 2026 Joint International Symposium: LOPSTR+PPDP brings together two long-established and important conferences in symbolic AI: The 36th Annual Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR), and The 28th International Symposium on Principles and Practice of Declarative Programming (PPDP). This Joint Symposium will provides a forum for the communities of both conferences to present new research and discover new perspectives. The Joint Symposium will take place over 2 1/2 days, from August 27-29, 2026 in Indianapolis, Indiana, USA. It is co-located with {\em The ...
| title | author | length |
|---|---|---|
| Elements of Logic Programming in a Concatenative Functional Language | Attila Egri-Nagy | 28m |
A minimal concatenative functional language called Con-Cat implements a free-monoid syntax and exposes programs as semigroupoid objects so algebraic… | ||
| Complex Autonomous UAV Task Execution and Decision-Making Using s(CASP) | Keegan Kimbrell, Alexis R Tudor, Peter Vu, Trevor Bihl, Doug Slattery, Gopal Gupta | 26m |
A symbolic UAV agent called VEXERA uses s(CASP) with AirSim on Unreal Engine 5 to execute navigation, search, debris detection, precision spraying, transport… | ||
| Coding Agents: New opportunities for formal methods? | Zach Hansen | 01h 16m |
Panel shows coding agents accelerate theorem proving but create new verification and tooling work. Agents generate huge artifacts (one project yields a… | ||
| Wren: A Fast Logic Programming eDSL With Host Language Garbage Collection | Kyle Dewey, Mehmet Emre | 30m |
Wren is a Scala LP eDSL that reworks term representation and execution to piggyback on host language garbage collection, using typed terms/goals so unification… | ||
| PAARL: An Interactive System for Policy-Aware Planning in Autonomous Agents(…) | Vineel Tummala, Daniela Inclezan | 26m |
PAARL implements an interactive AAA loop using Answer Set Programming with Clingo and a Python controller plus GUI to plan under authorization/obligation… | ||
| LOPSTR+PPDP Discussion | 24m | |
Combining LOPSTR and PPDP with ICFP is described as an experiment to boost submissions and visibility; registrations for the colocated ICFP year drop by about… | ||
| Vehicle with Time: Signal First-Order Logic for Closed-Loop Controller Synthesis | Gusts Gustavs Grīnbergs, Alessandro Bruni, Matthew L. Daggitt | 31m |
Vehicle extends the Vehicle DSL with a Time type, discrete-time bounded operators (□,[a,b], ◇,[a,b], U_[a,b]), an @dynamics annotation and a rollout primitive… | ||
| StageML: Partial Evaluation for Multi-Tenant MoE-LoRA Inference | Xavier Adettu, Tian Zhao | 27m |
StageML applies partial evaluation to multi-tenant MoE+LoRA serving, using a binding-time lattice to decide what can be precomputed at deployment or adapter… | ||
| Convenient Algebraic Programming with Coercive Subtyping | Henry Blanchette, Aaron Stump | 30m |
System automatically inserts the roll/unroll and catamorphism coercions so algebraic programs typecheck without manual coercive subtyping annotations, claiming… | ||
| Tempo: Reconstructing Synchronous Reactive Programming with OCaml 5 Effects | Frédéric Dabrowski | 23m |
Tempo reconstructs synchronous reactive semantics as an OCaml 5 library using OCaml 5 effects and deep handlers, reifying continuations into scheduler tasks… | ||
| From Constraints to Cognition: A Hybrid Framework for Adaptive, Explainable(…) | Stefania Costantini, Valentina Pitoni, Andrea Formisano, Lorenzo De Lauretis | 30m |
A hybrid pipeline compiles grounded Answer Set Programming schedules into an epistemic layer (L-DINF) via a named tau translation that turns baseline atoms… | ||
| Implementing Grassroots Logic Programs with Multiagent Transition Systems and AI | Ehud Shapiro | 30m |
Claims a deterministic multiagent semantics madGLP implements maGLP by replacing shared variable pairs with local pairs linked by global links and proving… | ||
| Deriving a Kronecker-Free Functional Quantum Simulator | Martin Elsman | 33m |
Derives a Kronecker-free interpreter that evaluates an n‑qubit circuit on a 2^n state vector without first building the 2^n×2^n unitary by using the… | ||
| Functional / Logic Programming in Verse | Stephanie Weirich | 01h 05m |
Verse claims a tight integration of functional and logic programming with a working prototype and a fresh denotational story: choices and failures are… | ||
| Combining Small-Step and Big-Step Semantics to Verify Loop Optimizations | David Knothe, Oliver Bringmann | 26m |
A practical method integrates coinductive big-step semantics with existing small-step CompCert passes, inserting a big-step Cminor stage mid-pipeline, proving… | ||
| Certified hardware for regexp matching: A rocq library and its workflow | Julin Shaji, Piyush Kurur, Sandeep Chandran | 27m |
A rocq library implements a certified synthesize function that turns a regular expression DSL into a Haskell matcher, uses clash to generate VERILOG, and runs… | ||
| A Typed and Unified Reflection for Shift and Shift0 | Yui Tamura, Kenichi Asai | 29m |
Establishes a typed, unified reflection for both shift and shift0 by deriving a two-CPS interpreter and a colon translation that yields a CPS target without… | ||
| What Is "Quantum" About Quantum Computing? | Amr Sabry | 01h 01m |
Starts from a sound, complete reversible classical language and proves that adding three concrete ingredients — a square root of NOT operator, a finite clock… | ||
| Proof-Carrying Code For the Age of AI: Machine-Checked Guarantees from(…) | Zoe Paraskevopoulou | 01h 17m |
Claims a practical pipeline: a Lean framework called EquiVM proves that deployed EVM bytecode refines a high‑level spec, and LLM agents autonomously complete… | ||
| nothing matches | ||