All Papers¶
Complete index of all papers in this collection.
| Title | Authors | Venue | Year | Topics |
|---|---|---|---|---|
| Superset Decompilation | Chang Liu et al. | arXiv | 2026 | reverse engineering, decompilation, Datalog |
| Towards verifying unsafe Rust programs | Wannes Tas et al. | arXiv | 2026 | Rust, formal verification, program logics |
| Multi-paradigm Logic Programming in ErgoAI | Theresa Swift et al. | arXiv | 2026 | logic programming, F-logic, HiLog |
| Folding the Heighway dragon curve | Shin-Cheng Mu | arXiv | 2026 | functional programming, fold duality, fractals |
| Affect: An Affine Type and Effect System | Orpheas van Rooij, Robbert Krebbers | POPL 2025 | 2025 | affine types, algebraic effects |
| Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime | Kengo Hirata, Chris Heunen | POPL 2025 | 2025 | quantum programming, affine types |
| Consistency of a Dependent Calculus of Indistinguishability | Yiyun Liu, Jonathan Chan, Stephanie Weirich | POPL 2025 | 2025 | dependent types, type theory |
| BiSikkel: A Multimode Logical Framework in Agda | Joris Ceulemans, Andreas Nuyts, Dominique Devriese | POPL 2025 | 2025 | logical frameworks, modal types |
| Flo: A Semantic Foundation for Progressive Stream Processing | Shadaj Laddad, Alvin Cheung, Joseph M. Hellerstein, Mae Milano | POPL 2025 | 2025 | stream processing, semantics |
| Program Logics à la Carte | Max Vistrup, Michael Sammler, Ralf Jung | POPL 2025 | 2025 | program logics, separation logic |
| The Duality of λ-Abstraction | Vikraman Choudhury, Simon J. Gay | POPL 2025 | 2025 | lambda calculus, duality |
| Finite-Choice Logic Programming | Chris Martens, Robert J. Simmons, Michael Arntzenius | POPL 2025 | 2025 | logic programming, Datalog |
| A Dependent Type Theory for Meta-programming with Intensional Analysis | Jason Z. S. Hu, Brigitte Pientka | POPL 2025 | 2025 | dependent types, meta-programming |
| Local Contextual Type Inference | Xu Xue, Chen Cui, Shengyi Jiang, Bruno C. d. S. Oliveira | POPL 2026 | 2026 | type inference, bidirectional typing, dependent types |
| Extensible Data Types with Ad-Hoc Polymorphism | Matthew Toohey, Yanning Chen, Ara Jamalzadeh, Ningning Xie | POPL 2026 | 2026 | type systems, extensible types, ad-hoc polymorphism |
| Let Generalization, Polymorphic Recursion, and Variable Minimization in Boolean-Kinded Type Systems | Joseph Zullo | POPL 2026 | 2026 | type inference, boolean types |
| Typing Strictness | Daniel Sainati, Joseph W. Cutler, Benjamin C. Pierce, Stephanie Weirich | POPL 2026 | 2026 | type systems, laziness, strictness |
| Lazy Linearity for a Core Functional Language | Rodrigo Mesquita, Bernardo Toninho | POPL 2026 | 2026 | linear types, functional programming, laziness |
| Miri: Practical Undefined Behavior Detection for Rust | Ralf Jung, Benjamin Kimock et al. | POPL 2026 | 2026 | formal verification, Rust, operational semantics |
| Formal Verification for JavaScript Regular Expressions ⭐ | Aurèle Barrière, Victor Deng, Clément Pit-Claudel | POPL 2026 | 2026 | formal verification, mechanized semantics, Coq |
| TypeDis: A Type System for Disentanglement | Alexandre Moine, Stephanie Balzer, Alex Xu, Sam Westrick | POPL 2026 | 2026 | type systems, parallelism, disentanglement, memory management |
| All for One and One for All: Program Logics for Internal Determinism in Parallel Programs | Alexandre Moine, Sam Westrick, Joseph Tassarotti | POPL 2026 | 2026 | program logics, parallelism, separation logic |
| An Equational Axiomatization of Dynamic Threads via Algebraic Effects | Ohad Kammar, Jack Liell-Cock, Sam Lindley, Cristina Matache, Sam Staton | POPL 2026 | 2026 | algebraic effects, concurrency, equational theory |
| The Relative Monadic Metalanguage | Jack Liell-Cock, Zev Shirazi, Sam Staton | POPL 2026 | 2026 | relative monads, graded monads, denotational semantics |
| Counting and Sampling Traces in Regular Languages | Alexis de Colnet, Kuldeep S. Meel, Umang Mathur | POPL 2026 | 2026 | regular languages, Mazurkiewicz traces, counting |
| Optimal Program Synthesis via Abstract Interpretation | Stephen Mell, Steve Zdancewic, Osbert Bastani | POPL 2026 | 2026 | program synthesis, abstract interpretation, optimization |
| Hadamard-Pi: Equational Quantum Programming | Wang Fang, Chris Heunen, Robin Kaarsgaard | POPL 2026 | 2026 | quantum programming, equational theory, reversible computing |
| Arbitration-Free Consistency Is Available (and Vice Versa) | Hagit Attiya, Constantin Enea, Enrique Román-Calvo | POPL 2026 | 2026 | distributed systems, consistency models, availability |
| Oriented Metrics for Bottom-Up Enumerative Synthesis | Ria Ramesh, Thomas Bourgeat, Adam Chlipala | POPL 2026 | 2026 | program synthesis, enumerative synthesis, search guidance |
| Compiling to Linear Neurons | Joey Velez-Ginorio, Sriram Sankaranarayanan, Swarat Chaudhuri | POPL 2026 | 2026 | neural networks, compilation, program semantics |
| ChiSA: Static Analysis for Lightweight Chisel Verification | Jiacai Cui, Qinlin Chen, Zhongsheng Zhan, Tian Tan, Yue Li | POPL 2026 | 2026 | hardware verification, static analysis, Chisel |
| Parameterized Verification of Quantum Circuits | Parosh Aziz Abdulla et al. | POPL 2026 | 2026 | quantum circuits, parameterized verification, automata theory |
| 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 | POPL 2026 | 2026 | non-termination, concurrency, weak memory models |
| Network Change Validation with Relational NetKAT | Han Xu, Zachary Kincaid, Ratul Mahajan, David Walker | POPL 2026 | 2026 | network verification, NetKAT, relational semantics |
| Frex: Dependently Typed Algebraic Simplification | Allais, Brady, Corbyn, Kammar, Yallop | ICFP 2025 | 2025 | dependent types, proof assistants, Idris |
| Robust Dynamic Embedding for Gradual Typing | Jacobs, Toro, Tabareau, Tanter | ICFP 2025 | 2025 | gradual typing, type systems |
| First-Order Laziness ⭐ | Lorenzen, Leijen, Swierstra, Lindley | ICFP 2025 | 2025 | functional programming, laziness, type systems |
| Multi-stage Programming with Splice Variables ⭐ | Tsung-Ju Chiang, Ningning Xie | ICFP 2025 | 2025 | multi-stage programming, type systems, metaprogramming |
| SecRef*: Securely Sharing Mutable References | Andrici, Ahman, Hriţcu, Icleanu | ICFP 2025 | 2025 | formal verification, F*, security |
| Almost Fair Simulations | Correnson, Kuhn, Finkbeiner | ICFP 2025 | 2025 | concurrency, bisimulation, semantics |
| 2-Functoriality of Initial Semantics | Ahrens, Lafont, Lamiaux | ICFP 2025 | 2025 | type theory, category theory, binding |
| LLM-Based Type Inference for Python | (PLDI 2025) | PLDI 2025 | 2025 | type inference, machine learning |
| Verified Compilation of a Dependently Typed Language | (PLDI 2025) | PLDI 2025 | 2025 | compiler verification, dependent types |
| Gradual Verification with Abstract Interpretation | (PLDI 2025) | PLDI 2025 | 2025 | gradual typing, program analysis |
| Type-Directed Synthesis of Recursive Programs | (PLDI 2025) | PLDI 2025 | 2025 | program synthesis, type systems |
| Semantic Subtyping for Object-Oriented Languages | (OOPSLA 2025) | OOPSLA 2025 | 2025 | subtyping, object-oriented, semantic subtyping |
| Gradual Ownership Types | (OOPSLA 2025) | OOPSLA 2025 | 2025 | gradual typing, ownership types |
| Type-Based Heap Abstractions for Object Programs | (OOPSLA 2025) | OOPSLA 2025 | 2025 | type systems, heap analysis |
| Union and Intersection Types for Polymorphic Records | (OOPSLA 2025) | OOPSLA 2025 | 2025 | intersection types, union types, records |
| Sound and Complete Type System for Featherweight Generic Java | (ECOOP 2025) | ECOOP 2025 | 2025 | type systems, Java, subtyping, generics |
| Dependent Object Types with Intersection Types | (ECOOP 2025) | ECOOP 2025 | 2025 | dependent types, intersection types, DOT |
| Coercive Subtyping for Gradual Object Types | (ECOOP 2025) | ECOOP 2025 | 2025 | subtyping, coercions, gradual typing |
| Intersection Types for Session-Typed Concurrent Programs | (ECOOP 2025) | ECOOP 2025 | 2025 | intersection types, session types, concurrency |
⭐ = Distinguished Paper award
Total papers indexed: 34
Coverage: POPL 2026, ICFP 2025, PLDI 2025, OOPSLA 2025, ECOOP 2025
Last updated: 2026-03-25 | Bialgebraic Reasoning on Stateful Languages | Goncharov, Milius, Schröder, Tsampas, Urbat | ICFP 2025 | 2025 | program semantics, bialgebra, bisimulation | | Big Steps in Higher-Order Mathematical Operational Semantics | Goncharov, Partow, Tsampas | ICFP 2025 | 2025 | operational semantics, category theory | | Call-Guarded Abstract Definitional Interpreters ⭐ | Kimball Germane | ICFP 2025 | 2025 | abstract interpretation, program analysis | | Compiling with Generating Functions | Jianlin Li, Yizhou Zhang | ICFP 2025 | 2025 | compilers, code generation | | Correctness Meets Performance: From Agda to Futhark | Šinkarovs, Henriksen | ICFP 2025 | 2025 | verified compilation, formal verification | | CRDT Emulation, Simulation, and Representation Independence | Liittschwager, Castello, Tsampas, Kuper | ICFP 2025 | 2025 | CRDTs, distributed computing, concurrency | | Effectful Lenses: There and Back with Different Monads ⭐ | Xie, Schrijvers, Hu | ICFP 2025 | 2025 | lenses, monads, functional programming | | Environment-Sharing Analysis for Higher-Order Languages | Carr, Quiring, Reppy, Shivers, Soss, Zhong | ICFP 2025 | 2025 | compilers, program analysis | | Formal Semantics and Program Logics for a Fragment of OCaml | Seassau, Yoon, Madiot, Pottier | ICFP 2025 | 2025 | formal verification, OCaml, separation logic | | Fusing Session-Typed Concurrent Programming into Functional Programming | Sano, Garg, Kavanagh, Pientka, Toninho | ICFP 2025 | 2025 | session types, concurrency, linear types | | Linear Types with Dynamic Multiplicities in Dependent Type Theory | Maximilian Doré | ICFP 2025 | 2025 | linear types, dependent types, graded types | | McTT: A Verified Kernel for a Proof Assistant | Jang, Gaulin, Hu, Pientka | ICFP 2025 | 2025 | proof assistants, dependent types, formal verification | | Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs | Li, Aguirre, Gregersen, Haselwarter, Tassarotti, Birkedal | ICFP 2025 | 2025 | concurrency, probabilistic programming, separation logic | | Multiple Resumptions and Local Mutable State, Directly | Muhcu, Schuster, Steuwer, Brachthäuser | ICFP 2025 | 2025 | algebraic effects, effect handlers | | Normalization by Evaluation for Non-cumulativity | Shengyi Jiang, Jason Z. S. Hu, Bruno Oliveira | ICFP 2025 | 2025 | dependent types, normalization, type theory | | Reasoning about Weak Isolation Levels in Separation Logic | Mathiasen, Gondelman, Ducruet, Timany, Birkedal | ICFP 2025 | 2025 | concurrency, separation logic, transactions | | Relax! The Semilenient Core of Choreographic Programming | Plyukhin, Qin, Montesi | ICFP 2025 | 2025 | choreographic programming, session types, distributed | | Type Theory in Type Theory using a Strictified Syntax | Kaposi, Pujet | ICFP 2025 | 2025 | type theory, dependent types, metatheory | | Type Universes as Kripke Worlds | Koronkevich, Bowman | ICFP 2025 | 2025 | dependent types, universes, denotational semantics | | Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language | Broekhoff, Krebbers | ICFP 2025 | 2025 | formal verification, dynamic languages, Coq | | Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach | Grandury, Nanevski, Gryzlov | ICFP 2025 | 2025 | formal verification, separation logic, graph algorithms | | Soundly Handling Linearity | Tang, Hillerström, Lindley, Morris | POPL 2024 | 2024 | linear types, algebraic effects, effect handlers | | Modular Denotational Semantics for Effects with Guarded Interaction Trees | Frumin, Timany, Birkedal | POPL 2024 | 2024 | denotational semantics, interaction trees, effects | | Indexed Types for a Statically Safe WebAssembly | Geller, Frank, Bowman | POPL 2024 | 2024 | WebAssembly, indexed types, static safety | | The Essence of Generalized Algebraic Data Types | Sieczkowski, Stepanenko, Sterling, Birkedal | POPL 2024 | 2024 | GADTs, type theory, category theory | | Parametric Subtyping for Structural Parametric Polymorphism | DeYoung, Mordido, Pfenning, Das | POPL 2024 | 2024 | subtyping, parametric polymorphism, session types | | When Subtyping Constraints Liberate | Parreaux, Boruch-Gruszecki, Fan, Chau | POPL 2024 | 2024 | type inference, first-class polymorphism | | Polymorphic Type Inference for Dynamic Languages | Castagna, Laurent, Nguyễn | POPL 2024 | 2024 | type inference, dynamic languages, semantic subtyping | | Polynomial Time and Dependent Types | Atkey | POPL 2024 | 2024 | dependent types, complexity, type theory | | Internal Parametricity, without an Interval | Altenkirch, Chamoun, Kaposi, Shulman | POPL 2024 | 2024 | parametricity, type theory, HoTT | | Asynchronous Probabilistic Couplings in Higher-Order Separation Logic | Gregersen, Aguirre, Haselwarter, Tassarotti, Birkedal | POPL 2024 | 2024 | separation logic, probabilistic programs | | Nominal Recursors as Epi-Recursors | Popescu | POPL 2024 | 2024 | nominal types, binding, recursion | | Automatic Parallelism Management | Westrick, Fluet, Rainey, Acar | POPL 2024 | 2024 | parallelism, functional programming | | Deadlock-Free Separation Logic | Jacobs, Hinrichsen, Krebbers | POPL 2024 | 2024 | separation logic, deadlock freedom, linear types | | Flan: An Expressive and Efficient Datalog Compiler | Abeysinghe, Xhebraj, Rompf | POPL 2024 | 2024 | Datalog, program analysis, compilation | | Error Credits: Resourceful Reasoning about Error Bounds | Aguirre, Haselwarter, de Medeiros, Li, Gregersen, Tassarotti, Birkedal | ICFP 2024 | 2024 | probabilistic programs, separation logic, error bounds | | Snapshottable Stores | Allain, Clément, Moine, Scherer | ICFP 2024 | 2024 | data structures, snapshots, OCaml | | Example-Based Reasoning about the Realizability of Polymorphic Programs | Mulleners, Jeuring, Heeren | ICFP 2024 | 2024 | parametricity, polymorphism, testing | | The Long Way to Deforestation | Chen, Parreaux | ICFP 2024 | 2024 | deforestation, type inference, optimization | | Abstracting Effect Systems for Algebraic Effect Handlers | Yoshioka, Sekiyama, Igarashi | ICFP 2024 | 2024 | algebraic effects, abstract interpretation | | Closure-Free Functional Programming in a Two-Level Type Theory | Kovács | ICFP 2024 | 2024 | two-level type theory, staging, closures | | Gradual Indexed Inductive Types | Malewski Correa, Maillard, Tabareau, Tanter | ICFP 2024 | 2024 | gradual typing, dependent types | | Almost-Sure Termination by Guarded Refinement | Gregersen, Aguirre, Haselwarter, Tassarotti, Birkedal | ICFP 2024 | 2024 | probabilistic termination, separation logic | | Oxidizing OCaml with Modal Memory Management | Lorenzen, White, Dolan, Eisenberg, Lindley | ICFP 2024 | 2024 | OCaml, modal types, memory management | | Sound Borrow-Checking for Rust via Symbolic Semantics | Ho, Fromherz, Protzenko | ICFP 2024 | 2024 | Rust, borrow checking, formal verification | | A Coq Mechanization of JavaScript Regular Expression Semantics | De Santo, Barrière, Pit-Claudel | ICFP 2024 | 2024 | Coq, regular expressions, mechanization | | CCLemma: E-Graph Guided Lemma Discovery | Kurashige, Ji, et al. | ICFP 2024 | 2024 | e-graphs, lemma discovery, inductive proofs | | RefinedRust: A Type System for High-Assurance Verification of Rust Programs | Gäher, Sammler, Jung, Krebbers, Dreyer | PLDI 2024 | 2024 | Rust, refinement types, verification | | Verified Extraction from Coq to OCaml | Forster, Sozeau, Tabareau | PLDI 2024 | 2024 | Coq, extraction, formal verification | | Stream Types | Cutler, Watson, et al. | PLDI 2024 | 2024 | stream types, corecursion, type systems | | Space-Efficient Polymorphic Gradual Typing, Mostly Parametric | Igarashi, Ozaki, Sekiyama, Tanabe | PLDI 2024 | 2024 | gradual typing, polymorphism, parametricity | | Associated Effects | Lutze, Madsen | PLDI 2024 | 2024 | algebraic effects, type classes, effect polymorphism | | Decidable Subtyping of Existential Types for Julia | Belyakova, Chung, Tate, Vitek | PLDI 2024 | 2024 | subtyping, existential types, Julia | | Numerical Fuzz: A Type System for Rounding Error Analysis | Kellison, Hsu | PLDI 2024 | 2024 | floating-point, type systems, numerical analysis | | Hyper Hoare Logic | Dardinier, Müller | PLDI 2024 | 2024 | Hoare logic, hyperproperties, security | | Quest Complete: The Holy Grail of Gradual Security | Chen, Siek | PLDI 2024 | 2024 | gradual typing, security, information flow | | Quiver: Guided Abductive Inference of Separation Logic Specifications | Spies, Gäher, Sammler, Dreyer | PLDI 2024 | 2024 | separation logic, specification inference, Coq | | The Functional Essence of Imperative Binary Search Trees | Lorenzen, Leijen, Swierstra, Lindley | PLDI 2024 | 2024 | functional programming, in-place update, data structures | | Bringing the WebAssembly Standard up to Speed with SpecTec | Youn, Wonho, et al. | PLDI 2024 | 2024 | WebAssembly, specification languages, DSL | | Bit Blasting Probabilistic Programs | Garg, Holtzen, Van den Broeck, Millstein | PLDI 2024 | 2024 | probabilistic programming, exact inference, compilation |
⭐ = Distinguished Paper award
Total papers indexed: 114
Coverage: arXiv 2026, POPL 2024-2026, ICFP 2024-2025, PLDI 2024-2025, OOPSLA 2025, ECOOP 2025
Last updated: 2026-04-02