POPL 2024
2024-01-14..2024-01-20
London, United Kingdom
POPL ·
[POPL 2021, POPL 2022, POPL 2022 Virtual Workshop, POPL 2023, POPL 2023 SRC, POPL 2024, POPL 2025, POPL 2026]
as the organisers put it
Welcome to the website of the 51st ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2024). POPL 2024 will take place in the Institution of Engineering and Technology (IET), Savoy Place, London The annual Symposium on Principles of Programming Languages is a forum for the discussion of all aspects of programming languages and programming systems. Both theoretical and experimental papers are welcome on topics ranging from formal frameworks to experience reports. We seek submissions that make principled, enduring contributions to the theory, design, understanding, implementa ...
| title | author | length |
|---|---|---|
| Welcome To POPL 2024 | Philippa Gardner | 08m |
Announcements cover health precautions with hand sanitizers around and a request to take care after recent COVID cases, plus exact catering logistics: two… | ||
| A New Perspective on Commutativity in Verification | Azadeh Farzan | 58m |
Argues that commutativity becomes a primary search dimension so verification can find an easier-to-prove program and carry results back soundly, formalizes… | ||
| Implementation and Synthesis of Math Library Functions | Ian Briggs, Yash Lad, Pavel Panchekha | 20m |
A domain specific language called MegaLibm implements, tests, and tunes exp sin log etc by embedding semantic types and semantic wellformedness checks that… | ||
| Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipu... | Yuantian Ding, Xiaokang Qiu | 19m |
DryadSynth implements a concrete pipeline that combines term-graph-based enumeration, example-guided filtration, LLM-prioritized components, and a bottom-up… | ||
| Efficient Bottom-Up Synthesis for Programs with Local Variables | Xiang Li, Xiangyu Zhou, Rui Dong, Yihong Zhang, Xinyu Wang | 17m |
Introduces lifted interpretation, an algorithm that evaluates all grammar programs simultaneously to enumerate binding contexts and collapse equivalent… | ||
| Optimal Program Synthesis via Abstract Interpretation | Stephen Mell, Steve Zdancewic, Osbert Bastani | 20m |
The paper presents a synthesis framework that finds numerically parameterized programs optimally by enumerating generalized partial programs and running A… | ||
| Generating Well-Typed Terms that are not "Useless" | Justin Frank, Benjamin Quiring, Leonidas Lampropoulos | 20m |
Generates well typed lambda terms that intentionally delay choosing argument types by introducing extension variables and an extensible application rule… | ||
| Indexed Types for a Statically Safe WebAssembly | Adam T. Geller, Justin Frank, William J. Bowman | 18m |
Wasm-prechk extends Wasmtime with an indexed-type system and a new memory-load-precheck instruction that lets the compiler remove per-access dynamic bounds… | ||
| The Essence of Generalized Algebraic Data Types | Filip Sieczkowski, Sergei Stepanenko, Jonathan Sterling, Lars Birkedal | 18m |
Presents a minimal core calculus—System Fω+μ with internalized type equalities and injective constant constructors—that directly encodes GADTs, proves… | ||
| Ill-Typed Programs Don't Evaluate | Steven Ramsay, Charlie Walpole | 19m |
Introduces two-sided type systems as a sequent-style typing calculus with left rules, a top type for "all values", and a new necessity function type that… | ||
| An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Dedu... | Neta Elad, Oded Padon, Sharon Shoham | 19m |
Proposes a finite, machine-checkable representation of certain infinite first-order models called symbolic structures and encodes model checking into linear… | ||
| Mostly Automated Verification of Liveness Properties for Distributed Protocols w... | Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh | 19m |
LVR reduces liveness to a set of safety checks plus a termination proof: synthesize a nonnegative integer ranking function that strictly decreases on every… | ||
| Decision and Complexity of Dolev-Yao Hyperproperties | Itsaka Rakotonirina, Gilles Barthe, Clara Schneidewind | 21m |
Provides the first decision procedure for Dolev–Yao hyperproperties under a bounded number of sessions and subterm-convergent equational theories, proving… | ||
| Soundly Handling Linearity | Wenhao Tang, Daniel Hillerström, Sam Lindley, J. Garrett Morris | 16m |
This work introduces control-flow linearity, formalizes it in a System F-style core calculus Feff∘ with linear types and effect handlers, and gives a… | ||
| Answer Refinement Modification: Refinement Type System for Algebraic Effects and... | Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi | 23m |
Proposes a refinement type system that tracks how delimited-continuation effects change return types via answer refinement modification, formalizes ATM/ARM… | ||
| Effectful Software Contracts | Cameron Moy, Christos Dimoulas, Matthias Felleisen | 21m |
Presents a formal design that lets contracts perform effects while proving they do not change successful runs: an erasure theorem showing contract checks… | ||
| Algebraic Effects Meet Hoare Logic in Cubical Agda | Donnacha Oisín Kidney, Zhixuan Yang, Nicolas Wu | 22m |
Library formalises algebraic effects with equations in Cubical Agda using quotient types instead of setoids, provides a free model plus concrete models, and… | ||
| An Iris Instance for Verifying CompCert C Programs | William Mansky, Ke Du | 19m |
Rebuilds VST’s program logic inside Iris to verify C as defined by CompCert, providing an Iris instance of CompCert C with a custom shared-value algebra that… | ||
| The Logical Essence of Well-Bracketed Control Flow | Amin Timany, Armaël Guéneau, Lars Birkedal | 19m |
First Hoare-style separation logic for well-bracketed control flow that proves the closure-from-example always returns one when called with a function that… | ||
| Asynchronous Probabilistic Couplings in Higher-Order Separation Logic | Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal | 20m |
Provides a new higher-order relational separation logic called Clutch that proves contextual refinement for a language with impredicative polymorphism… | ||
| Thunks and Debits in Separation Logic with Time Credits | François Pottier, Armaël Guéneau, Jacques-Henri Jourdan, Glen Mével | 20m |
Machine‑checked reconstruction of Okasaki’s debit reasoning implemented in Iris$, with proofs and reusable artifacts (Zenodo/GitLab). Formalizes the missing… | ||
| Parikh's Theorem Made Symbolic | Matthew Hague, Artur Jez, Anthony W. Lin | 18m |
Construction converts symbolic automata and parametric symbolic grammars into compact numeric abstractions: an algorithm computes polynomial-time existential… | ||
| Efficient Matching of Regular Expressions with Lookaround Assertions | Konstantinos Mamouras, Agnishom Chattopadhyay | 21m |
States a formal semantics for lookaround, gives an algorithm that matches regexes with lookaround in O(m·n) time by evaluating assertions bottom-up, and… | ||
| The Complex(ity) Landscape of Checking Infinite Descent | Liron Cohen, Adham Jabarin, Andrei Popescu, Reuben N. S. Rowe | 18m |
Two new decision procedures for Infinite Descent appear: an automata-based variant that encodes sloped relations so the trace automaton is exponential only in… | ||
| Positive Almost-Sure Termination – Complexity and Proof Rules | Rupak Majumdar, V.R. Sathiyanarayana | 19m |
Shows that Positive Almost-Sure Termination (PAST) for an imperative language with rational variables, bounded nondeterministic choice and discrete… | ||
| EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers ... | Pu Sun, Fu Song, Yuqi Chen, Taolue Chen | 20m |
A domain-specific language EasyBC encodes block ciphers and automatically generates MILP models to bound the maximum expected differential characteristic… | ||
| A Core Calculus for Documents: Or, Lambda: The Ultimate Document | Will Crichton, Shriram Krishnamurthi | 20m |
Presents a formal core calculus that classifies document languages into eight levels (string vs. article domains × four constructors), proves each level as an… | ||
| Validation of Modern JSON Schema: Formalization and Complexity | Lyes Attouche, Mohamed-Amine Baazizi, Dario Colazzo, Giorgio Ghelli, Carlo Sartiani, Stefanie Scherzinger | 19m |
Paper formalizes Modern JSON Schema syntax and proves data validation is PSPACE-complete, pinpointing the blowup to dynamic references (Draft 2020‑12) while… | ||
| Shoggoth - A Formal Foundation for Strategic Rewriting | Xueying Qin, Liam O'Connor, Rob van Glabbeek, Peter Hoefner, Ohad Kammar, Michel Steuwer | 18m |
Provides a formal denotational semantics for System S and a big-step operational semantics that explicitly models divergence, proves computational soundness… | ||
| A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verifie... | Prasad Jayanti, Siddhartha Jayanti, Ugur Y. Yavuz, Lizzie Hernandez | 21m |
Introduces a forward-only proof method called possibility tracking that is claimed to be universal, sound, and complete for proving linearizability, with a… | ||
| Predictive Monitoring against Pattern Regular Languages | Zhendong Ang, Umang Mathur | 19m |
Shows a conditional hardness result: predictive monitoring against regular languages requires at least O(n^α) lower bound time under fine-grained assumptions… | ||
| Commutativity Simplifies Proofs of Parameterized Programs | Azadeh Farzan, Dominik Klumpp, Andreas Podelski | 19m |
Extends commutativity-based reductions to parameterized programs and encodes each reduction by transforming the thread template into another parameterized… | ||
| Coarser Equivalences for Causal Concurrency | Azadeh Farzan, Umang Mathur | 20m |
Proves a linear space lower bound for deciding causal concurrency under the fullest reads‑from style relaxation, shows classic trace/commutativity lets the… | ||
| On Model-Checking Higher-Order Effectful Programs | Ugo Dal Lago, Alexis Ghyselen | 21m |
Paper shows higher-order effectful programs map to ordinary higher-order recursion schemes via a CPS transformation and recovers classic model-checking… | ||
| Explicit Effects and Effect Constraints in ReML | Martin Elsman | 21m |
ReML is a Standard ML dialect that makes memory and other effects explicit while staying backwards compatible; it integrates region-polymorphic inference with… | ||
| Decalf: A Directed, Effectful Cost-Aware Logical Framework | Harrison Grodin, Yue Niu, Jonathan Sterling, Robert Harper | 18m |
Decalf is a directed, effectful, cost-aware logical framework implemented in Agda that equips every type with an intrinsic preorder so a cost bound can itself… | ||
| Modular Denotational Semantics for Effects with Guarded Interaction Trees | Dan Frumin, Amin Timany, Lars Birkedal | 21m |
Introduces guarded interaction trees as a denotational domain for higher-order effects, fully formalized in Coq/Iris formalization with reusable artifacts… | ||
| Semantic Code Refactoring for Abstract Data Types | Shankara Pailoor, Yuepeng Wang, Işıl Dillig | 19m |
Automates ADT refactoring by taking an original implementation, a new data layout and a relational representation invariant, then synthesizing each method via… | ||
| API-driven Program Synthesis for Testing Static Typing Implementations | Thodoris Sotiropoulos, Stefanos Chaliasos, Zhendong Su | 19m |
Thalia synthesizes small, type‑intensive client programs from real libraries by building an API graph and enumerating typing sequences that drive… | ||
| Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Progr... | Kevin Batz, Tom Jannik Biskup, Joost-Pieter Katoen, Tobias Winkler | 17m |
Shows a semi-automatic method that synthesizes memoryless deterministic (MD) strategies for probabilistic imperative programs by transforming guards via… | ||
| A Case for Synthesis of Recursive Quantum Unitary Programs | Haowei Deng, Runzhou Tao, Yuxiang Peng, Xiaodi Wu | 23m |
QSynth synthesizes recursive unitary programs by combining an inductive quantum language with a fixed‑point rule, a hypothesis‑amplitude input/output… | ||
| Quotient Haskell: Lightweight Quotient Types for All | Brandon Hewer, Graham Hutton | 21m |
Quotient Haskell extends Liquid Haskell to add quotient types whose proof obligations are decidable by an SMT solver, so functions are automatically checked… | ||
| Focusing on Refinement Typing (TOPLAS) | Dimitrios J. Economou, Neel Krishnaswami, Jana Dunfield | 19m |
A logically principled system that combines value-determined indices, focalized call-by-push-value, bidirectional typing and polarized subtyping generates SMT… | ||
| Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in ... | Guannan Wei, Oliver Bračevac, Songlin Jia, Yuyan Bao, Tiark Rompf | 18m |
Introduces a new freshness qualifier (diamond) that marks allocations whose reachability may materialize later, and designs two calculi (λ✦ and F✦ calculi)… | ||
| Capturing Types (TOPLAS) | Aleksander Boruch-Gruszecki, Martin Odersky, Edward Lee, Ondřej Lhoták, Jonathan Immanuel Brachthäuser | 20m |
A minimal calculus called CC<:◻ capture calculus extends System F<: with capture sets so types record which capability-like free variables values may retain… | ||
| Probabilistic programming interfaces for random graphs: Markov categories, graph... | Nate Ackerman, Cameron E. Freer, Younesse Kaddar, Jacek Karwowski, Sean K. Moss, Daniel Roy, Sam Staton, Hongseok Yang | 19m |
Proves an equivalence: a well-behaved implementation of an abstract graph type (vertices, new, edge) corresponds exactly to a graphon. Uses Markov categories… | ||
| Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures | Francesca Randone, Luca Bortolussi, Emilio Incerto, Mirco Tribastone | 20m |
Presents Gaussian Semantics: approximate a bounded probabilistic program’s exact distribution by Gaussian mixtures whose parameters are set by matching moments… | ||
| Higher Order Bayesian Networks, Exactly | Claudia Faggian, Daniele Pautasso, Gabriele Vanoni | 16m |
A higher-order lambda-calculus is defined that is sound and complete for Bayesian networks: every Bayesian network encodes as a term and every well-typed… | ||
| Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants f... | Julian Müllner, Marcel Moosbrugger, Laura Kovács | 22m |
Proves that computing the strongest polynomial invariant for single‑path loops with polynomial assignments is Skolem-hard, and that point‑to‑point reachability… | ||
| With a Few Square Roots, Quantum Computing is as Easy as Pi | Jacques Carette, Chris Heunen, Robin Kaarsgaard, Amr Sabry | 20m |
Extending rig groupoids with two distinguished maps and three coherence equations yields a computationally universal model of unitary quantum computing: one… | ||
| Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-Determinis... | Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, Gabriele Tedeschi | 19m |
Introduces lqCCS (an asynchronous linear quantum CCS) and shows that unconstrained contexts can perform impossible non-deterministic choices on quantum data… | ||
| SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog Co... | Yuxiang Peng, Jacob Young, Pengyu Liu, Xiaodi Wu | 22m |
SimuQ implements a full pipeline: a Hamiltonian Modeling Language for target systems, an abstract analog instruction set (AAIS) and AAIS Specification Language… | ||
| Enriched Presheaf Model of Quantum FPC | Takeshi Tsukada, Kazuyuki Asada | 20m |
Extends Selinger’s superoperator model to higher-order programs by building modules over superoperators (equivalently enriched presheaves) and carving a… | ||
| How Hard is Weak-Memory Testing? | Soham Chakraborty, Shankara Narayanan Krishna, Umang Mathur, Andreas Pavlogiannis | 20m |
Paper proves that consistency testing for many weak-memory models is NP-complete even with bounded threads, memory locations, and values, ruling out… | ||
| An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: T... | Angus Hammond, Zongyuan Liu, Thibaut Pérami, Peter Sewell, Lars Birkedal, Jean Pichon-Pharabod | 19m |
Claims a new separation logic AxSL for the Arm‑A user‑mode axiomatic model that lets relaxed reads/writes transfer resources when they induce ordering… | ||
| Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intension... | Amin Timany, Simon Oddershede Gregersen, Leo Stefanesco, Jonas Kastberg Hinrichsen, Léon Gondelman, Abel Nieto, Lars Birkedal | 20m |
Introduces Trillium as a language-agnostic separation-logic framework that proves intensional refinements between program traces and labeled transition models… | ||
| Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-O... | Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers | 20m |
LinearActris is a linear concurrent separation logic that claims to give deadlock and leak freedom for message-passing programs by design. The adequacy proof… | ||
| Polyregular functions on unordered trees of bounded height | Mikołaj Bojańczyk, Bartek Klin | 20m |
Proves that equivalence of injective first‑order interpretations (polyregular functions) on unordered trees of fixed height is decidable by normalizing to a… | ||
| Solving Infinite-State Games via Acceleration | Philippe Heim, Rayna Dimitrova | 19m |
Presents a new symbolic semi-algorithm that uses acceleration lemmas to force convergence of attractor fixpoint computations that otherwise diverge on… | ||
| Ramsey Quantifiers in Linear Arithmetics | Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin, Georg Zetzsche | 19m |
Proves an elimination procedure for Ramsey quantifiers over Linear Integer, Real, and mixed arithmetic (LIA, LRA, LIRA) that, for existential input formulas… | ||
| Reachability in Continuous Pushdown VASS | A. R. Balasubramanian, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche | 25m |
Proves reachability and even coverability for pushdown VASS with continuous semantics (counters are rationals scaled by any factor in (0,1]) is… | ||
| Pipelines and Beyond: Graph Types for ADTs with Futures | Francis Rinaldi, june wunder, Arthur Azevedo de Amorim, Stefan K. Muller | 20m |
Extends graph types to let futures live inside recursive ADTs by indexing datatypes with a codata vertex structures that supply unique vertex names, proving… | ||
| Disentanglement with Futures, State, and Interaction | Jatin Arora, Stefan K. Muller, Umut A. Acar | 20m |
Formalizes disentanglement for a language with futures, I/O, and mutable references and proves that purely functional programs are disentangled; extends to… | ||
| DisLog: A Separation Logic for Disentanglement | Alexandre Moine, Sam Westrick, Stephanie Balzer | 17m |
Claims a first static program logic that proves disentanglement for fork‑join programs and gives a high‑level variant that yields disentanglement for race‑free… | ||
| Automatic Parallelism Management | Sam Westrick, Matthew Fluet, Mike Rainey, Umut A. Acar | 25m |
Fine-grained Fork–Join Parallel ML gets a nearly zero-cost call convention that adds two return addresses and copies the stack frame so a continuation can be… | ||
| SIGPLAN Awards, PC Chair's Report, and Business Meeting | Philippa Gardner | 01h 23m |
Conference report gives concrete numbers and decisions: 319 submissions with 93 accepted, a single flat 86‑member PC, and adoption of full double blind review… | ||
| Extraordinary Meeting: The Publicity Chairs Reflect on the Peer-Review Process | Alastair F. Donaldson, John Wickerson | 05m |
A reflective, often comic diagnosis of peer review that names concrete pain points and behavior not just ideals It highlights workload pressures with numbers… | ||
| The Network is the Computer: A Programming Language Perspective | Nate Foster | 01h 08m |
Argues that making switches programmable with the P4 language lets operators push filtering, caching and tiny distributed services into the data plane; shows a… | ||
| Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis | John Cyphert, Zachary Kincaid | 20m |
Generates loop summaries that abstractions arbitrary loop bodies into a solvable polynomial ideal and then applies a proven complete solver (a generalization… | ||
| On-The-Fly Static Analysis via Dynamic Bidirected Dyck Reachability | Krishna Shankaranarayanan, Aniket Lal, Andreas Pavlogiannis, Omkar Tuppe | 17m |
Provides a dynamic algorithm for bidirected Dyck reachability with worst-case O(n·α(n)) per update (beating the prior O(n2) worst case), implements it, and… | ||
| Monotonicity and the Precision of Program Analysis | Marco Campion, Mila Dalla Preda, Roberto Giacobazzi, Caterina Urban | 21m |
Paper proves that if a program is monotone (non‑decreasing or non‑increasing) on a bounded input space and yields a convex numeric output over a non‑relational… | ||
| Flan: An Expressive and Efficient Datalog Compiler for Program Analysis | Supun Abeysinghe, Anxhelo Xhebraj, Tiark Rompf | 19m |
Flan compiles a high‑level Datalog interpreter written in Scala via Lightweight Modular Staging to generate specialized C code, keeping the interpreter’s… | ||
| Internal parametricity, without an interval | Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, Michael Shulman | 19m |
Presents a compact type theory extending Martin-Löf with a few new type and term formers that internalises parametricity without introducing an interval… | ||
| Internal and Observational Parametricity for Cubical Agda | Antoine Van Muylder, Andreas Nuyts, Dominique Devriese | 19m |
An implementation called Agda --bridges adds internal parametricity to cubical Agda, successfully type checks the cubical library and mechanizes key results… | ||
| Internalizing Indistinguishability with Dependent Types | Yiyun Liu, Jonathan Chan, Jessica Shi, Stephanie Weirich | 20m |
DCOI (Dependent Calculus of Indistinguishability) internalizes indistinguishability as definitional equality and adds an observer-indexed identity type so… | ||
| Polynomial Time and Dependent types | Robert Atkey | 20m |
Combines two concrete implicit‑P approaches — a cons‑free linear system that bans construction of iterable data, and an LFPL style diamond payment system that… | ||
| Guided Equality Saturation | Thomas Kœhler, Andrés Goens, Siddharth Bhat, Tobias Grosser, Phil Trinder, Michel Steuwer | 21m |
Guided equality saturation splits a hard e-graph search into sequences of smaller equality-saturation runs guided by human-provided intermediate sketches… | ||
| Fusing Direct Manipulations into Functional Programs | Xing Zhang, Ruifeng Xie, Guanchen Guo, Xiao He, Tao Zan, Zhenjiang Hu | 18m |
Operation-based system defines a small composable Delta language DM for edits (add, mul, tuple, list-fold, constraints) and a fusion algorithm that propagates… | ||
| Inference of Robust Reachability Constraints | Yanis Sellami, Guillaume Girol, Frédéric Recoules, Damien Couroussé, Sébastien Bardin | 19m |
Proposes an algorithm that uses theory-agnostic abduction to infer predicates on uncontrolled inputs that guarantee a property is robustly reachable… | ||
| Nominal Recursors as Epi-Recursors | Andrei Popescu | 21m |
Identifies nominal recursion schemes as instances of an abstract epi-recursors pattern and builds a categorical framework that compares expressiveness by… | ||
| When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-C... | Lionel Parreaux, Aleksander Boruch-Gruszecki, Andong Fan, Chun Yin Chau | 22m |
Introduces a declarative system F{≤} and an algorithm SuperF that uses multi‑bounded polymorphism to infer first‑class polymorphic types, encoding… | ||
| Parametric Subtyping for Structural Parametric Polymorphism | Henry DeYoung, Andreia Mordido, Frank Pfenning, Ankush Das | 18m |
Paper proves structural subtyping is undecidable for recursive type constructors and defines parametric subtyping as a decidable fragment that enforces… | ||
| Unboxed data constructors -- or, how cpp decides a halting problem | Nicolas Chataing, Stephen Dolan, Gabriel Scherer, Jeremy Yallop | 20m |
Adds selective unboxing to OCaml with a prototype compiler and a static check that rejects unboxings that would create overlapping representations, yielding up… | ||
| Polymorphic Type Inference for Dynamic Languages | Giuseppe Castagna, Mickaël Laurent, Kim Nguyen | 21m |
Claims a type system that combines first‑order polymorphism with intersection, union and semantic subtyping and proves safety; it gives unannotated functions… | ||
| Efficient CHAD | Tom J. Smeding, Matthijs I. L. Vákár | 19m |
Claims that Combinatory Homomorphic AD (CHAD) can be optimized to achieve the expected reverse‑mode complexity with only constant overhead, backed by an Agda… | ||
| ReLU Hull Approximation | Zhongkui Ma, Jiaying Li, Guangdong Bai | 18m |
Proposes WraLU, a fast algorithm that builds a convex polytope wrapping the ReLU hull by reusing the two linear pieces as lower faces and constructs upper… | ||
| On Learning Polynomial Recursive Programs | Alex Buna-Marginean, Vincent Cheval, Mahsa Shirmohammadi, James Worrell | 19m |
Introduces P-finite automata, a generalisation of weighted automata whose transition weights are polynomials in the input position and which over a unary… | ||
| Programming-by-Demonstration for Long-Horizon Robot Tasks | Noah Patton, Kia Rahmani, Meghana Missula, Joydeep Biswas, Işıl Dillig | 21m |
PROLEX synthesizes robot control programs by turning demonstrations into regex-like sketches, completing holes with an LLM-guided search, and pruning… | ||
| Mechanizing Refinement Types | Michael H. Borkowski, Niki Vazou, Ranjit Jhala | 20m |
Introduces λRF, a core calculus that actually combines semantic subtyping with parametric polymorphism and proves soundness; develops two mechanizations: one… | ||
| VST-A: A Foundationally Sound Annotation Verifier | Litao Zhou, Jianxing Qin, Qinshi Wang, Andrew W. Appel, Qinxiang Cao | 19m |
VST-A is an annotation verifier that parses C into control‑flow graphs, splits functions into paths (four paths for the linked‑list reverse example) and… | ||
| Fully Composable and Adequate Verified Compilation with Direct Refinements betwe... | Ling Zhang, Yuting Wang, Jinhua Wu, Jérémie Koenig, Zhong Shao | 20m |
Claims a Kripke Memory Relation (called NGP) that is transitive and absorbs per-pass rely/guarantee conditions so a single direct refinement relates Clight… | ||
| A Formalization of Core Why3 in Coq | Joshua M. Cohen, Philip Johnson-Freyd | 18m |
Formalization of Why3's core logic as a machine-checked denotational semantics in Coq maps Why3 types to Coq sets, builds explicit encodings for recursive… | ||
| Securing Verified IO Programs Against Unverified Code in F* | Cezar-Constantin Andrici, Ștefan Ciobâcă, Cătălin Hriţcu, Guido Martínez, Exequiel Rivas, Éric Tanter, Théo Winterhalter | 21m |
A verified secure compilation pipeline for F programs that perform IO, called SCIO, compiles verified code to a smaller F target and enforces assumptions at… | ||
| Sound Gradual Verification with Symbolic Execution | Conrad Zimmerman, Jenna DiVincenzo, Jonathan Aldrich | 18m |
Provides a formal, machine-checked semantics for symbolic execution and for optimized runtime-check generation, proves that gradual verification implemented… | ||
| Type-based Gradual Typing Performance Optimization | John Peter Campora III, Mohammad Wahiduzzaman Khan, Sheng Chen | 18m |
Implements discriminative typing that infers per-function types, duplicates each function into an optimized and a safe version, and uses variational typing… | ||
| Total Type Error Localization and Recovery with Holes | Eric Zhao, Raef Maroof, Anand Dukkipati, Andrew Blinn, Zhiyi Pan, Cyrus Omar | 21m |
Defines a marked lambda calculus that makes every program meaningful by inserting error marks as nonempty holes, gives a total marking procedure (every… | ||
| Orthologic with Axioms | Simon Guilloud, Viktor Kuncak | 20m |
Presents orthologic extended with axioms and proves a generalized cut‑elimination and subformula property that yields a concrete decision procedure… | ||
| Deciding Asynchronous Hyperproperties for Recursive Programs | Jens Oliver Gutsfeld, Markus Müller-Olm, Christoph Ohrem | 20m |
Paper introduces a new asynchronous hyperlogic that adds fixpoints, non-atomic tests (trace formulas with CARET-style call/return inspection), and a simpler… | ||
| Calculational Design of [In]Correctness Transformational Program Logics by Abstr... | Patrick Cousot | 26m |
Claims that transformational correctness and incorrectness logics are abstract interpretation of the relational semantics’ right-image transformer, covering… | ||
| Concluding Remarks | Philippa Gardner | 04m |
Conference closes with thanks to Eric Drer for long‑running PC leadership, the AV team for fixing recurring integration hiccups, and the student volunteers who… | ||
| nothing matches | ||