POPL 2026
2026-01-11..2026-01-17
Rennes, France
POPL ·
[POPL 2021, POPL 2022, POPL 2022 Virtual Workshop, POPL 2023, POPL 2023 SRC, POPL 2024, POPL 2025, POPL 2026]
who it's for
programming language researchers, type system designers, formal verification engineers, program synthesis researchers, compiler engineers, proof assistant developers, systems verification engineers, Rust developers
topics
contextual System F type inference; separation logic for cryptography; quantum separation logic; probabilistic program k-induction; recurrence sets for weak memory; MLIR abstract transformers; undefined-behavior detection for Rust (Miri); DSL-guided synthesis optimization; vectorized probabilistic inference; verification of message-passing concurrency (DafnyMPI); network change validation with NetKAT; resource-aware circuit description languages
| title | author | length |
|---|---|---|
| Local Contextual Type Inference | Xu Xue, Chen Cui, Shengyi Jiang | 24m |
Presents a principled redesign of local type inference that embeds contextual typing into a variant of System F called Contextual System F (Fc), gives a… | ||
| U-Turn: Enhancing Incorrectness Analysis by Reversing Direction | Flavio Ascari, Roberto Bruni, Roberta Gori, Azalea Raad | 24m |
Combines forward Incorrectness Logic derivations with backward Sufficient Incorrectness Logic by instrumenting backward proof rules with the forward derivation… | ||
| Counting and Sampling Traces in Regular Languages | Alexis de Colnet, Kuldeep S. Meel, Umang Mathur | 25m |
Problem: count Mazurkiewicz traces of length n that intersect a regular language presented as an m‑state automaton; hardness: exact counting is #P‑hard already… | ||
| RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing | Yusuke Matsushita, Kengo Hirata, Ryo Wakizaka, Emanuele D'Osualdo | 26m |
RapunSL presents a program logic that adds linear combination (scalar multiply and plus) and a separate mixing connective to quantum separation logic, so… | ||
| Bounded Sort Polymorphism with Elimination Constraints | Johann Rosain, Tomas Diaz, Kenji Maillard, Matthieu Sozeau, Nicolas Tabareau, Éric Tanter, Théo Winterhalter | 23m |
Extends sort polymorphism with elimination constraints that record which sorts may eliminate into which, implements the system in the Rocq prover, and proves… | ||
| Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks | Michael Lee, Ningning Xie, Oleg Kiselyov, Jeremy Yallop | 24m |
Compares three concrete dynamic checks—lazy vs eager and a new Cause-for-Concern (C4C) check—and gives a formal calculus for evaluating them with effect… | ||
| Accelerating Syntax-Guided Program Synthesis by Optimizing Domain-Specific Languages | Zhentao Ye, Ruyi Ji, Yingfei Xiong, Xin Zhang | 17m |
AMaze automatically refines DSLs to cut synthesis time by estimating enumeration cost instead of running the solver, computing a feature component rank for… | ||
| Determination Problems for Orbit Closures and Matrix Groups | Rida Ait El Manssour, George Kenison, Mahsa Shirmohammadi, Anton Varonka, James Worrell | 30m |
Gives a concrete algorithm: a polynomial-space procedure that decides, given an algebraic variety and a number s, whether the variety equals the orbit closure… | ||
| Cryptis: Cryptographic Reasoning in Separation Logic | Arthur Azevedo de Amorim, Amal Ahmed, Marco Gaboardi | 26m |
Cryptis extends Iris separation logic with a symbolic-cryptography model and gives protocol specs that actually exchange separation-logic resources so proofs… | ||
| Di- is for Directed: First-Order Directed Type Theory via Dinaturality | Andrea Laretto, Fosco Loregian, Niccolò Veltri | 25m |
Proposes a first-order directed type theory interpreting types as categories, terms as functors, predicates as dipresheaves, and entailments as dinatural… | ||
| Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Models | Thomas Haas, Roland Meyer, Hernán Ponce de León, Andrés Lomelí Garduño | 27m |
Generalizes recurrence sets from states to execution-based recurrence sets over axiomatic weak-memory execution graphs, proves soundness for all practical… | ||
| The Ghosts of Empires: Extracting Modularity from Interleaving-Based Proofs | Frank Schüssele, Matthias Zumkeller, Miriam Lagunes-Rochin, Dominik Klumpp | 21m |
Converts interleaving-based certificates produced by Ultimate Automizer into compact Owicki–Gries thread-modular proofs by synthesizing ghost variables… | ||
| A Lazy, Concurrent Convertibility Checker | Nathanaëlle Courant, Xavier Leroy | 25m |
A convertibility algorithm that interleaves evaluation and comparison using lazy channels and concurrent processes, representing lazy values as channels and… | ||
| An Equational Axiomatization of Dynamic Threads via Algebraic Effects: Presheaves on(…) | Ohad Kammar, Jack Liell-Cock, Sam Lindley, Cristina Matache, Sam Staton | 24m |
Paper gives a concrete equational axiomatization for dynamic threads: a parameterized algebraic theory (using presheaves and strong monads) that encodes… | ||
| Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by(…) | Marcus Rossel, Rudi Schneider, Thomas Kœhler, Michel Steuwer, Andrés Goens | 24m |
Presents a Lean tactic that translates theorems into conditional rewrite rules, runs equality saturation with egg on an e-graphs representation, and… | ||
| Higher-Order Behavioural Conformances via Fibrations | Henning Urbat | 27m |
Categorical framework defines an abstract higher-order specification (AHOS) for big-step semantics and models program conformance via fibrations; behavioural… | ||
| Parametrised Verification of Intel-x86 Programs | Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan | 25m |
Proves that k‑alternation bounded reachability for Intel eTSO is decidable even when the number of identical threads is unbounded, overcoming the need to refer… | ||
| Medium-scale automation for proof assistants | Damien Pous | 01h 10m |
Shows that medium-scale automation produces concise, convincing, robust formal proofs for relation algebra and monoidal category theorems by combining… | ||
| An Expressive Assertion Language for Quantum Programs | Bonan Su, Yuan Feng, Mingsheng Ying, Li Zhou | 27m |
Defines an assertion language that represents quantum predicates as quasi-probability distributions of generalized Pauli operators and proves constructively… | ||
| ChopChop: A Programmable Framework for Semantically Constraining the Output of Language(…) | Shaan Nagy, Timothy Zhou, Nadia Polikarpova, Loris D'Antoni | 26m |
ChopChop constructs constrained decoders that decide whether a token prefix has a completion satisfying a semantic spec by building prefix spaces and solving a… | ||
| Piecewise Analysis of Probabilistic Programs via k-Induction | Tengshun Yang, Shenghua Feng, Hongfei Fu, Naijun Zhan, Jingyu Ke, Shiyang Wu | 26m |
Proposes a method that extracts region splits from k-induction operators and combines them with the Optional Stopping Theorem to synthesize piecewise… | ||
| Handling Higher-Order Effectful Operations with Judgemental Monadic Laws | Zhixuan Yang, Nicolas Wu | 25m |
Presents a core calculus for higher-order effectful operations with higher-kinded impredicative polymorphism and optional recursion, where handlers live in… | ||
| Will it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage(…) | Alexandre Moine, Arthur Charguéraud, François Pottier | 23m |
IrisFit is a separation logic, formalized in Coq on top of the Iris framework, that uses space credits to bound heap usage for a concurrent call-by-value… | ||
| Classical Notions of Computation and the Hasegawa-Thielecke Theorem | Éléonore Mangel, Paul-André Melliès, Guillaume Munch-Maccagnoni | 24m |
Defines a polarized effect calculus called linear classical L-calculus and shows composition can fail associativity when call-by-value and call-by-name… | ||
| Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof(…) | Neta Elad, Adithya Murali, Sharon Shoham | 23m |
Main claim: the common fold/unfold proof steps are sound and — for the quantifier‑free, theory‑free fragment — complete for a weaker semantics called Weak… | ||
| Characterizing Sets of Theories That Can Be Disjointly Combined | Benjamin Przybocki, Guilherme V. Toledo, Yoni Zohar | 25m |
Proves an exact characterization of which decidable first‑order theories over disjoint signatures can be disjointly combined, showing Nelson–Oppen’s stable… | ||
| Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling | Doyoon Lee, Woosuk Lee, Kwangkeun Yi | 23m |
Paper proposes a lightweight meta-analysis, feasibility square analysis, that predicts when forward/backward abstract interpretation will prune a partial… | ||
| The Simple Essence of Boolean-Algebraic Subtyping: Semantic Soundness for Algebraic(…) | Chun Yin Chau, Lionel Parreaux | 26m |
Distills BAS to five families of characteristic Boolean homomorphisms and uses them to give a direct semantic soundness proof that subtyping never equates… | ||
| Consistent Updates for Scalable Microservices | Devora Chait-Roth, Kedar S. Namjoshi, Thomas Wies | 25m |
Presents a formal framework and the first algorithms that guarantee atomic-looking live updates for rolling microservice upgrades by routing requests based on… | ||
| From Semantics to Syntax: A Type Theory for Comprehension Categories | Niyousha Najmaei, Niels van der Weide, Benedikt Ahrens, Paige Randall North | 23m |
Defines a syntax CCT that internalizes the previously unused vertical morphisms of comprehension categories and proves that any comprehension category with the… | ||
| Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures | C. Aiswarya, Pascal Baumann, Prakash Saivasan, Lia Schütze, Georg Zetzsche | 24m |
Proves that the word languages of MSO-definable bounded-stw = multiple context-free languages by translating bounded-treewidth run graphs to tree automata and… | ||
| ArchSem: Reusable Rigorous Semantics of Relaxed Architectures | Thibaut Pérami, Thomas Bauereiss, Brian Campbell, Zongyuan Liu, Nils Lauermann, Alasdair Armstrong, Peter Sewell | 26m |
A reusable framework composes ISA pseudo-code from Sail with concurrency interpreters in Rock via a freemonad of 15 algebraic effects, ingesting the full ARM… | ||
| A Relational Separation Logic for Effect Handlers | Paulo Emílio de Vilhena, Simcha van Collem, Ines Wright, Robbert Krebbers | 25m |
Presents blaze, the first mechanised relational separation logic for effect handlers, implemented on Rocq/Iris and proved inside Coq; key idea is a refinement… | ||
| Fuzzing Guided by Bayesian Program Analysis | Yifan Zhang, Xin Zhang | 24m |
Redefines Bayesian program analysis so each alarm gets a probability of being reachable by exploitation fuzzing (99% threshold in evaluation), uses per-target… | ||
| Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers | Xuanyu Peng, Dominic Kennedy, Yuyou Fan, Ben Greenman, John Regehr, Loris D'Antoni | 25m |
Automates generation of MLIR integer abstract transformers by synthesizing small SSA programs (cut-style MCMC search) and composing them with… | ||
| A Synthetic Reconstruction of Multiparty Session Types | David Castro-Perez, Francisco Ferreira, Sung-Shik Jongmans | 23m |
New approach types processes directly against a global labelled transition system, claiming no projection and restoring compositionality while matching the… | ||
| Security Reasoning via Substructural Dependency Tracking | Hemant Gouni, Frank Pfenning, Jonathan Aldrich | 23m |
A new type system flips substructural resource reasoning from inputs to outputs and implements a suspended computation connective so effects are produced when… | ||
| Normalisation for First-Class Universe Levels | Nils Anders Danielsson, Naïm Camille Favier, Ondřej Kubánek | 30m |
Proves normalization for a dependent type theory with first-class universe levels and derives decidable equality, decidable type-checking and canonicity; shows… | ||
| Endangered by the Language But Saved by the Compiler: Robust Safety via Semantic(…) | Niklas Mück, Aina Linn Georges, Derek Dreyer, Deepak Garg, Michael Sammler | 26m |
Shows a hardening compiler that makes a C‑like source (Rec) robustly safe only after compilation to a CHERI‑style capability machine (Cap); proves a separation… | ||
| Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and(…) | Noam Zilberstein, Alexandra Silva, Joseph Tassarotti | 23m |
Introduces Probabilistic Concurrent Outcome Logic (pcOL) that composes concurrent separation logic, probabilistic separation logic, and Outcome Logic to prove… | ||
| A Logic for the Imprecision of Abstract Interpretations | Marco Campion, Mila Dalla Preda, Roberto Giacobazzi, Caterina Urban | 25m |
Introduces a program logic, Error Propagation Logic, that produces an explicit bounding function mapping concrete-input imprecision to an upper bound on… | ||
| A Complementary Approach to Incorrectness Typing | Celia Mengyue Li, Sophie Pull, Steven Ramsay | 30m |
A two-sided type system treats types as sets of normal forms rather than values and introduces a complement operator that behaves like logical negation on… | ||
| TypeDis: A Type System for Disentanglement | Alexandre Moine, Stephanie Balzer, Alex Xu, Sam Westrick | 24m |
TypeDis is a type system that guarantees any well-typed program is disentangled and so permits task-local, synchronization-free garbage collection; it… | ||
| Quantum Circuits Are Just a Phase | Chris Heunen, Louis Lemonnier, Christopher McNally, Alex Rice | 27m |
Defines a tiny language with a single numerical primitive pH(theta) (global phase) plus a quantum pattern match iflet that picks bases via patterns as… | ||
| Let Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded(…) | Joseph A. Zullo | 23m |
Claims practical procedures for equational generalization in arbitrary Boolean rings and for boolean semi-unification decidable via Baz’s method, enabling… | ||
| Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach | Yiyun Liu, Stephanie Weirich | 26m |
Shows that reduce-and-compare becomes decidable again with surjective pairing by restricting transitivity to a syntactically defined SN good set of strongly… | ||
| DafnyMPI: A Dafny Library for Verifying Message-Passing Concurrent Programs | Aleksandr Fedchin, Antero Mejr, Hari Sundar, Jeffrey S. Foster | 26m |
DafnyMPI is a pure Dafny library that verifies MPI programs by requiring a statically declared communication topology and unique message tags so preconditions… | ||
| A Modular Static Cost Analysis for GPU Warp-Level Parallelism | Gregory Blike, Hannah Zicarelli, Udaya Sathiyamoorthy, Julien Lange, Tiago Cogumbreiro | 25m |
Claims a new static, relational-cost analysis that translates warp semantics into a sequential cost program and is parametric on resource metric and relation… | ||
| Coco: Corecursion with Compositional Heterogeneous Productivity | Jaewoo Kim, Yeonwoo Nam, Chung-Kil Hur | 25m |
CHP claims it computes Compositional Heterogeneous Productivity relations that quantify how many outputs a component produces given input-level requirements… | ||
| Canonicity for Indexed Inductive-Recursive Types | András Kovács | 27m |
Proves canonicity for Martin-Löf type theory with a countable universe hierarchy where every universe supports indexed inductive-recursive types. Method is two… | ||
| Probabilistic Programming with Vectorized Programmable Inference | McCoy R. Becker, Mathieu Huot, George Matheos, Xiaoyan Wang, Karen Chung, Colin Smith, Sam Ritchie, Rif A. Saurous, Alexander K. Lew, Martin C. Rinard, Vikash K. Mansinghka | 23m |
GenJAX is a Python-embedded language and compiler that integrates JAX and exposes a vmap vectorization transformation to vectorize probabilistic traces… | ||
| Quotient Polymorphism | Brandon Hewer, Graham Hutton | 28m |
Adds choice polymorphism for quotiented types to stop repeating equivalent functions and to accept valid-but-rejected code, implemented in Quotient Haskell on… | ||
| Miri: Practical Undefined Behavior Detection for Rust | Ralf Jung, Benjamin Kimock, Christian Poveda, Eduardo Sánchez Muñoz, Oli Scherer, Qian Wang | 25m |
Miri is an interpreter of Rust’s abstract machine that tracks per-byte initialization and pointer provenance, enforces Rust type representations, detects data… | ||
| Dependent Coeffects for Local Sensitivity Analysis | Victor Sannier, Patrick Baillot | 24m |
Introduces Local Fuzz, a type system using dependent coeffects that computes upper bounds on local sensitivity (sensitivity at point x within radius k), giving… | ||
| The Relative Monadic Metalanguage | Jack Liell-Cock, Zev Shirazi, Sam Staton | 27m |
Generalises the monadic metalanguage to a relative setting and gives a complete semantics using a new definition of strong relative monads. Builds a… | ||
| Optimising Density Computations in Probabilistic Programs via Automatic Loop Vectorisation | Sangho Lim, Hyoungjin Lim, Wonyeol Lee, Xavier Rival, Hongseok Yang | 26m |
Automatic vectorisation translates imperative PPL loops into a tensor-ready target with a Pyro implementation that runs loop iterations via speculative… | ||
| A Verified High-Performance Composable Object Library for Remote Direct Memory Access | Guillaume Ambal, George Hodgkins, Mark Madler, Gregory Chockler, Brijesh Dongol, Joseph Izraelevitz, Azalea Raad, Viktor Vafeiadis | 23m |
LOCO is a verified C++ RDMA object library that implements ring buffers, barriers and a key‑value store atop a single-thread manager for hardware completion… | ||
| AdapTT: Functoriality for Dependent Type Casts | Arthur Adjedj, Meven Lennon-Bertrand, Thibaut Benjamin, Kenji Maillard | 25m |
A new type theory AdapTT formalizes adapters as external morphisms that form a category and lets every type former act functorially on those adapters so casts… | ||
| Stateful Differential Operators for Incremental Computing | Runqing Xu, Sebastian Erdweg | 26m |
Presents a formal specification for stateful differential operators that lets operators store and update custom state, proves correctness in Rocq, and extracts… | ||
| Parameterized Verification of Quantum Circuits | Parosh Aziz Abdulla, Yu-Fang Chen, Michal Hečko, Lukáš Holík, Ondřej Lengál, Jyun-Ao Lin, Ramanathan S. Thinniyam | 27m |
Presents a fully automatic framework that verifies relational properties of size‑parameterized quantum programs by modeling infinite families of quantum states… | ||
| Oriented Metrics for Bottom-Up Enumerative Synthesis | Roland Meyer, Jakob Tepe | 28m |
Introduces an oriented metric that is asymmetric except at zero, lifts it from strings/bitvectors to programs, and uses it to prune (ball radius 100 in… | ||
| Typing Strictness | Daniel Sainati, Joseph W. Cutler, Benjamin C. Pierce, Stephanie Weirich | 27m |
Proposes a refinement of strictness called intentional strictness and encodes it as a type-and-effect system for call-by-name and call-by-push-value, with a… | ||
| Parameterized Infinite-State Reactive Synthesis | Benedikt Maderbacher, Roderick Bloem | 27m |
A counterexample‑guided loop synthesizes a single parameterized infinite‑state reactive program and a proof by: (1) enumerating small concrete parameter… | ||
| Bayesian Separation Logic | Shing Hin Ho, Nicolas Wu, Azalea Raad | 23m |
Introduces a separation logic that actually models Bayesian updating and scoring, proving an internal Bayes' theorem by invoking the Rokhlin‑Simmons… | ||
| Compiling to Linear Neurons | Joey Velez-Ginorio, Nada Amin, Konrad Kording, Steve Zdancewic | 23m |
Claims a typed linear language called Cajal compiles discrete programs into linear neurons by translating conditionals into soft branching linear maps, with a… | ||
| Verifying Almost-Sure Termination for Randomized Distributed Algorithms | Constantin Enea, Rupak Majumdar, Harshit Jitendra Motwani, V.R. Sathiyanarayana | 24m |
Presents a sound proof rule that combines martingale-based arguments with reasoning about weak fairness and produces SMT-based proofs for almost-sure… | ||
| Abstraction Functions as Types | Harrison Grodin, Runming Li, Robert Harper | 26m |
Encodes abstraction functions inside types by adding a single new proposition (an abstract phase) to univalent dependent type theory, then uses a gluing… | ||
| The Complexity of Testing Message-Passing Concurrency | Zheng Shi, Lasse Møldrup, Umang Mathur, Andreas Pavlogiannis | 25m |
Characterizes channel-consistency as a parameterized complexity landscape: consistency checking is NP-hard even for single-valued or capacity‑one channels, and… | ||
| Rows and Capabilities as Modal Effects | Wenhao Tang, Sam Lindley | 25m |
Claims a uniform framework that encodes row-based (Koka-style) and capability-based (Eff-style) effect systems into a modal-effect core, using modalities… | ||
| Context-Free-Language Reachability for Almost-Commuting Transition Systems | Nikhil Pimpalkhare, Zachary Kincaid, Thomas Reps | 23m |
Proves that the Parikh-image machinery extends to an almost-commuting monoid, giving a polynomial-time procedure that produces a Presburger formula describing… | ||
| Arbitration-Free Consistency Is Available (and Vice Versa) | Hagit Attiya, Constantin Enea, Enrique Román-Calvo | 24m |
Claims a tight iff theorem: a storage specification admits an available implementation under partitions exactly when it is arbitration-free — no requirement… | ||
| Hardware-Software Contracts for High Assurance with Applications to Side-Channel Security | Caroline Trippel | 01h 13m |
Presents three concrete hardware–software contracts and their implementations: the ASP execution contract plus compiler passes form Cerberus, a software-only… | ||
| Tropical Mathematics and the Lambda-Calculus II: Tropical Geometry of Probabilistic(…) | Davide Barbarossa, Paolo Pistone | 27m |
Claims that each closed higher-order probabilistic bool program maps to a finite tropical degree and an associated minimal Newton polytope that encode its… | ||
| Generating Compilers for Qubit Mapping and Routing | Abtin Molavi, Amanda Xu, Ethan Cecchetti, Swamit Tannu, Aws Albarghouthi | 26m |
A system generates qubit mapping and routing compilers from a compact specification and a device graph, using an Amara language frontend and a parametric… | ||
| Lazy Linearity for a Core Functional Language | Rodrigo Mesquita, Bernardo Toninho | 22m |
Linear Core statically accepts Haskell-style lazy semantic linearity and proves soundness by an instrumented big-step semantics that tracks runtime resource… | ||
| Hyperfunctions: Communicating Continuations | Donnacha Oisín Kidney, Nicolas Wu | 25m |
Identifies a recurring type — the hyperfunction — that actually implements communication between continuations and concurrent processes, shows it appears in… | ||
| Network Change Validation with Relational NetKAT | Han Xu, Zachary Kincaid, Ratul Mahajan, David Walker | 25m |
Relational NetKAT is a specification language for change-by-trace: programs describe a trace relation R and compile it to NetKAT transducers and automata so… | ||
| What Is a Monoid? | Paul Blain Levy, Morgan Rogers | 31m |
Proposes a two-stage generalization of multicategories that actually makes sequencing and relative-monad examples into monoids: first left-skew multicategory… | ||
| Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation(…) | Clément Allain, Gabriel Scherer | 25m |
Zoo delivers a transpiler plus proof framework that translates OCaml 5 into a limited ZooLang fragment embedded via a deep embedding in Rocq, where programs… | ||
| ChiSA: Static Analysis for Lightweight Chisel Verification | Jiacai Cui, Qinlin Chen, Zhongsheng Zhan, Tian Tan, Yue Li | 26m |
ChiSA gives a formal core calculus lambda_C and a synchronized fixed‑point solver for hardware value flow analysis (HVFA), plus a 30K+ LoC analyzer and an 11M+… | ||
| Foundational Multi-Modal Program Verifiers | Vladimir Gladshtein, George Pîrlea, Qiyuan Zhao, Vitaly Kurin, Ilya Sergey | 24m |
Paper presents a framework implemented in Lean implementation that provides a library of monad transformers for state, divergence, exceptions and… | ||
| Extensible Data Types with Ad-Hoc Polymorphism | Matthew Toohey, Yanning Chen, Ara Jamalzadeh, Ningning Xie | 27m |
Combines row polymorphism and type classes to let rows carry constraints like all constraint and to fold over fields with a new primitive end induction, while… | ||
| Encode the Cake and Eat It Too: Controlling Computation in Type Theory, Locally | Yann Leray, Théo Winterhalter | 27m |
Claims a type theory LRTT that adds local rewrite rules via prenex abstraction over computation rules and a prototype implemented as a Rocq extension with all… | ||
| All for One and One for All: Program Logics for Exploiting Internal Determinism in(…) | Alexandre Moine, Sam Westrick, Joseph Tassarotti | 25m |
Defines schedule-independent safety: showing one terminating execution is safe suffices to guarantee safety for all schedules. Introduces separation logic… | ||
| Domain-Theoretic Semantics for Functional Logic Programming | Eddie Jones, Samson Main, Celia Mengyue Li, Jonathan Marriott, G. A. Kavvos | 26m |
Reconstructs a typed FLP core calculus as call-by-push-value with algebraic effects, implements an abstract machine that performs weak head narrowing using… | ||
| Formal Verification for JavaScript Regular Expressions: A Proven Mechanized Semantics(…) | Aurèle Barrière, Victor Deng, Clément Pit-Claudel | 25m |
Paper presents a mechanized, ECMAScript‑faithful semantics for JavaScript regexes in the Rocq proof assistant, equating a concise 21 inductive rules semantics… | ||
| Qudit Quantum Programming with Projective Cliffords | Jennifer Paykin, Sam Winnick | 26m |
Claims a lambda calculus called LambdaPC that encodes projective Cliffords as functions P ↦ UPU† for qudits of any dimension and proves expressiveness: every… | ||
| Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment | David M. Kahn, Jan Hoffmann, Runming Li | 25m |
Extends big-step semantics with a nondeterministic big-stop rule schema that captures every finite prefix of diverging small-step runs, proving equivalence to… | ||
| On Circuit Description Languages, Indexed Monads, and Resource Analysis | Ken Sakayori, Andrea Colledan, Ugo Dal Lago | 25m |
Presents a monad-based denotational semantics for Proto-Quipper variants that cleanly separates returned values from the circuits a term generates, using a… | ||
| nothing matches | ||