ECOOP Papers¶

Papers indexed from ECOOP (European Conference on Object-Oriented Programming). ECOOP 2025 proceedings published in LIPIcs Volume 333.

2025¶

Compositional Static Value Analysis for Higher-Order Numerical Programs¶

Authors: Milla Valnet, Raphaël Monat, Antoine Miné
Venue: ECOOP 2025
Year: 2025
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2025

Presents a compositional static value analysis for higher-order programs with numerical computations, enabling modular analysis of functions passed as arguments. The abstract interpretation framework scales to practical higher-order functional programs with numeric operations.

Keywords: abstract interpretation, static analysis, higher-order programs, numerical analysis

Lightweight Diagramming for Formal Methods: A Grounded Language Design¶

Authors: Siddhartha Prasad, Ben Greenman, Tim Nelson, Shriram Krishnamurthi
Venue: ECOOP 2025
Year: 2025
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2025

Develops a lightweight diagram notation integrated with formal specification languages, making formal models easier to understand visually. The language design is grounded in user studies showing that diagram integration reduces comprehension errors for formal specifications.

Keywords: formal methods, diagramming, language design, visualization

Taming and Dissecting Recursions through Interprocedural Weak Topological Ordering¶

Authors: Jiawei Yang, Xiao Cheng, Bor-Yuh Evan Chang, Xiapu Luo, Yulei Sui
Venue: ECOOP 2025
Year: 2025
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2025

Presents interprocedural weak topological ordering to improve analysis of recursive programs by structuring the iteration order of fixpoint computations. The approach speeds up convergence and improves precision of dataflow analyses over recursive call graphs.

Keywords: static analysis, dataflow, recursion, fixpoint computation

The Algebra of Patterns¶

Authors: David Binder, Lean Ermantraut
Venue: ECOOP 2025
Year: 2025
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2025

Develops an algebraic theory of patterns in programming languages, characterizing pattern matching through algebraic laws and operations. The framework unifies various pattern forms across languages into a common algebraic structure.

Keywords: pattern matching, algebra, type theory, programming languages

A theory of (linear-time) timed monitors¶

Authors: Mouloud Amara, Giovanni Bernardi, Mohammed Aristide Foughali, Adrian Francalanza
Venue: ECOOP 2025
Year: 2025
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2025

Develops a formal theory of timed runtime monitors operating over linear-time temporal properties, establishing correctness conditions for monitors with real-time constraints. The theory clarifies when timed monitors can correctly decide property violations on infinite executions.

Keywords: runtime verification, timed monitors, temporal logic, linear time

Contrasting Deadlock-Free Session Processes¶

Authors: Juan C. Jaramillo, Jorge A. Pérez
Venue: ECOOP 2025
Year: 2025
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2025.17

Compares different approaches to ensuring deadlock freedom in session-typed process calculi, analyzing tradeoffs between expressiveness and compositional deadlock avoidance guarantees. The work clarifies the relationships between key session type disciplines for deadlock freedom.

Keywords: session types, deadlock freedom, process calculi, concurrency

Fair Termination of Asynchronous Binary Sessions¶

Authors: Luca Padovani, Gianluigi Zavattaro
Venue: ECOOP 2025
Year: 2025
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2025

Studies fair termination of asynchronous binary session-typed processes, ensuring that protocols eventually complete under fair scheduling assumptions. The work provides type-based criteria guaranteeing liveness of session communications.

Keywords: session types, fair termination, asynchronous communication, liveness

Incremental Computing by Differential Execution¶

Authors: Prashant Kumar, André Pacak, Sebastian Erdweg
Venue: ECOOP 2025
Year: 2025
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2025

Presents differential execution as a technique for incremental computation, where programs re-execute only the parts affected by input changes. The approach enables automatic incrementalization of programs without manual specification of dependencies.

Keywords: incremental computing, differential execution, program analysis, reactivity

Multiparty Asynchronous Session Types: A Mechanised Proof of Subject Reduction¶

Authors: Dawit Tirore, Jesper Bengtson, Marco Carbone
Venue: ECOOP 2025
Year: 2025
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2025

Provides a mechanized proof of subject reduction for multiparty asynchronous session types in a proof assistant, validating the type safety of this important concurrency type discipline. The mechanization covers the full MPST calculus with asynchronous communication.

Keywords: multiparty session types, mechanized proofs, subject reduction, asynchronous communication

Declarative Dynamic Object Reclassification¶

Authors: Riccardo Sieve, Eduard Kamburjan, Ferruccio Damiani, Einar Broch Johnsen
Venue: ECOOP 2025
Year: 2025
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2025

Introduces declarative dynamic object reclassification, allowing objects to change their class at runtime based on declarative rules. The approach combines active objects with reclassification to enable safe dynamic dispatch under changing object classifications.

Keywords: object reclassification, dynamic dispatch, active objects, object-oriented

Mono Types — First-Class Containers for Datalog¶

Authors: Runqing Xu, David Klopp, Sebastian Erdweg
Venue: ECOOP 2025
Year: 2025
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2025

Introduces mono types as first-class container types for Datalog, enabling Datalog programs to manipulate typed collections of facts directly. This extension increases the expressiveness of Datalog for programming language analysis tasks.

Keywords: Datalog, type systems, program analysis, containers

Monadic type-and-effect soundness¶

Authors: Francesco Dagnino, Paola Giannini, Elena Zucca
Venue: ECOOP 2025
Year: 2025
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2025

Establishes a general type-and-effect soundness theorem using monads to model computational effects, providing a unified framework for type safety across different effect systems. The monadic approach abstracts over specific effect implementations while preserving soundness.

Keywords: type and effect systems, monads, type soundness, computational effects

An Effectful Object Calculus¶

Authors: Francesco Dagnino, Paola Giannini, Elena Zucca
Venue: ECOOP 2025
Year: 2025
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2025

Develops an object calculus with effects where method calls can produce computational effects tracked in the type system. The calculus provides a formal foundation for effect-aware object-oriented programming with a sound type-and-effect system.

Keywords: object calculus, effects, type systems, object-oriented

Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness¶

Authors: Pedro Carrott, Sacha-Élie Ayoun, Azalea Raad
Venue: ECOOP 2025
Year: 2025
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2025.5

Presents a logical framework for compositional bug detection in libraries that use unsafe operations internally while exposing a safe interface. The approach uses incorrectness logic to find real bugs arising from unsoundness of FFI or unsafe code within otherwise typed programs.

Keywords: bug detection, compositional verification, incorrectness logic, unsafe code

Practical Type-Based Taint Checking and Inference¶

Authors: Nima Karimipour, Kanak Das, Manu Sridharan, Behnaz Hassanshahi
Venue: ECOOP 2025
Year: 2025
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2025

Develops a practical type-based taint analysis with type inference, reducing annotation burden while providing sound taint tracking. The system scales to real-world Java programs and identifies security vulnerabilities through automatic propagation of taint annotations.

Keywords: taint analysis, type inference, security, static analysis

Bottom-up Synthesis of Memory Mutations with Separation Logic¶

Authors: Kasra Ferdowsi, Hila Peleg
Venue: ECOOP 2025
Year: 2025
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2025

Presents a program synthesis algorithm for memory-manipulating programs using separation logic specifications, using a bottom-up enumeration strategy guided by heap constraints. The tool synthesizes pointer-manipulating code from pre/postconditions in separation logic.

Keywords: program synthesis, separation logic, memory safety, heap reasoning

IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL¶

Authors: Matt Griffin, Brijesh Dongol, Azalea Raad
Venue: ECOOP 2025
Year: 2025
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2025

Develops IsaBIL, an Isabelle/HOL framework for verifying both correctness and incorrectness properties of binary programs. The framework supports binary-level reasoning using both forward (correctness) and backward (bug-finding) program logics.

Keywords: binary verification, Isabelle/HOL, correctness, incorrectness logic

Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis¶

Authors: Mamy Razafintsialonina, David Bühler, Antoine Miné, Valentin Perrelle, Julien Signoles
Venue: ECOOP 2025
Year: 2025
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2025

Presents an incremental static analysis framework that reuses previously computed invariants and analysis caches to avoid redundant work when programs are updated. The approach provides soundness guarantees for incremental re-analysis of modified programs.

Keywords: incremental analysis, static analysis, abstract interpretation, soundness

RacerF: Lightweight Static Data Race Detection for C Code¶

Authors: Tomáš Dacík, Tomas Vojnar
Venue: ECOOP 2025
Year: 2025
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2025

Introduces RacerF, a lightweight static data race detector for C programs based on shape analysis with fractional permissions. The tool detects races without requiring programmer annotations by inferring ownership through compositional heap analysis.

Keywords: data race detection, static analysis, C, concurrency

PoTo: A Hybrid Andersen's Points-to Analysis for Python¶

Authors: Ingkarat Rak-amnouykit, Ana Milanova, Guillaume Baudart, Martin Hirzel, Julian Dolby
Venue: ECOOP 2025
Year: 2025
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2025

Presents PoTo, a hybrid points-to analysis for Python combining Andersen's static analysis with dynamic profiling for improved precision on dynamic language features. The hybrid approach achieves better recall on Python's dynamic dispatch while maintaining reasonable performance.

Keywords: points-to analysis, Python, dynamic analysis, program analysis

Pydrofoil: accelerating Sail-based instruction set simulators¶

Authors: Martin Berger, CF Bolz-Tereick, Luke Panayi, Ferdia McKeogh, Tom Spink
Venue: ECOOP 2025
Year: 2025
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2025

Pydrofoil accelerates ISA simulators derived from Sail specifications by compiling them to efficient Python using meta-tracing JIT compilation. The tool enables high-performance simulation from formal ISA specifications without sacrificing their correctness guarantees.

Keywords: instruction set simulators, Sail, JIT compilation, ISA specification

2024¶

Static Basic Block Versioning¶

Authors: Manuel Serrano, Olivier Melançon, Marc Feeley
Venue: ECOOP 2024
Year: 2024
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2024

Introduces static basic block versioning, a compilation technique that specializes code blocks based on type information available at compile time. This achieves JIT-like performance benefits through ahead-of-time specialization without runtime profiling.

Keywords: compilation, basic block versioning, type specialization, JIT

Compiling with Arrays¶

Authors: David Richter, Timon Böhler, Pascal Weisenburger, Mira Mezini
Venue: ECOOP 2024
Year: 2024
DOI: https://arxiv.org/pdf/2405.18242

Develops a compilation strategy targeting arrays as a first-class primitive, enabling efficient code generation for array-intensive programs. The approach bridges high-level functional array operations and low-level array implementations.

Keywords: compilation, arrays, code generation, functional programming

Optimizing Layout of Recursive Datatypes with Marmoset¶

Authors: Vidush Singhal, Chaitanya S. Koparkar, Joseph Zullo, Artem Pelenitsyn, Michael Vollmer, Mike Rainey, Ryan R. Newton, Milind Kulkarni
Venue: ECOOP 2024
Year: 2024
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2024.38

Marmoset is a compiler optimization system that automatically chooses memory layouts for recursive algebraic datatypes to improve cache performance. It analyses access patterns and selects among several layout strategies to minimize cache misses.

Keywords: data layout, recursive datatypes, compilation, performance

Behavioral up/down casting for statically typed languages¶

Authors: Lorenzo Bacchiani, Mario Bravetti, Marco Giunti, João Mota, António Ravara
Venue: ECOOP 2024
Year: 2024
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2024

Proposes a type-theoretic treatment of behavioral upcasting and downcasting for session-typed and class-typed languages, providing safe dynamic type conversions that preserve protocol compliance. The work extends subtyping with covariant and contravariant behavioral refinements.

Keywords: session types, subtyping, casting, behavioral types

Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency¶

Authors: Farzaneh Derakhshan, Stephanie Balzer, Yue Yao
Venue: ECOOP 2024
Year: 2024
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2024

Introduces regrading policies in session-typed languages to allow principled declassification and endorsement of information in concurrent programs. The framework integrates information flow control with linear session types.

Keywords: information flow, session types, concurrency, security types

Ozone: Fully Out-of-Order Choreographies¶

Authors: Dan Plyukhin, Marco Peressotti, Fabrizio Montesi
Venue: ECOOP 2024
Year: 2024
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2024

Ozone extends choreographic programming with out-of-order execution, allowing choreographies to specify concurrent communication patterns beyond strict sequential order. The work provides a formal model and endpoint projection for out-of-order choreographies.

Keywords: choreographic programming, concurrency, out-of-order execution, process calculi

Information Flow Control in Cyclic Process Networks¶

Authors: Bas van den Heuvel, Farzaneh Derakhshan, Stephanie Balzer
Venue: ECOOP 2024
Year: 2024
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2024

Develops information flow control for process networks with cycles, extending prior session type approaches to handle cyclic communication topologies safely. The type system prevents leakage of confidential information through cycle-forming communication paths.

Keywords: information flow, session types, cyclic processes, security

Authors: Ke Sun, Di Wang, Sheng Chen, Meng Wang, Dan Hao
Venue: ECOOP 2024
Year: 2024
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2024

Presents a formalization and mechanized proof of soundness for class-based refinement types in an object-oriented language. The approach allows class hierarchies to carry logical predicates that are checked statically, with a Coq mechanization validating the metatheory.

Keywords: refinement types, object-oriented, Coq, mechanization, verification

Pure methods for roDOT¶

Authors: Vlastimil Dort, Yufeng Li, Ondřej Lhoták, Pavel Parizek
Venue: ECOOP 2024
Year: 2024
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2024

Extends the roDOT (read-only Dependent Object Types) calculus with pure methods that have no side effects, enabling richer specifications in a DOT-based type system. The extension preserves key metatheoretic properties while allowing more expressive method contracts.

Keywords: DOT calculus, dependent object types, purity, type theory

Failure Transparency in Stateful Dataflow Systems¶

Authors: Aleksey Veresov, Jonas Spenger, Paris Carbone, Philipp Haller
Venue: ECOOP 2024
Year: 2024
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2024.42

Formalizes failure transparency for stateful dataflow systems, providing guarantees that failures are hidden from application logic through automatic recovery. The formal model captures exactly-once semantics for stateful streaming computations.

Keywords: dataflow, fault tolerance, formal semantics, distributed systems

Fair join pattern matching for actors¶

Authors: Philipp Haller, Ayman Hussein, Hernan Melgratti, Alceste Scalas, Emilio Tuosto
Venue: ECOOP 2024
Year: 2024
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2024.17

Introduces fair join pattern matching for actors, ensuring that join patterns are matched fairly among waiting actors. The approach combines join calculus with fairness properties, providing formal guarantees about liveness in actor-based concurrent programs.

Keywords: actors, join patterns, fairness, concurrency

Fearless Asynchronous Communications with Timed Multiparty Session Protocols¶

Authors: Ping Hou, Nicolas Lagaillardie, Nobuko Yoshida
Venue: ECOOP 2024
Year: 2024
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2024

Presents a Rust framework for safe asynchronous communication using timed multiparty session types. The approach enforces communication protocols and timing constraints at compile time, preventing deadlocks and timeouts in distributed systems.

Keywords: session types, multiparty protocols, Rust, timed protocols, asynchronous communication

Defining Name Accessibility using Scope Graphs¶

Authors: Aron Zwaan, Casper Bach
Venue: ECOOP 2024
Year: 2024
DOI: https://doi.org/10.48550/arXiv.2407.09320

Uses scope graphs as a formal framework to define name accessibility in programming languages, capturing shadowing, visibility rules, and module systems in a uniform graph-based model. The approach is language-agnostic and can be instantiated for different scoping disciplines.

Keywords: scope graphs, name binding, scoping, language design

Constrictor: Immutability as a Design Concept¶

Authors: Elad Kinsbruner, Shachar Itzhaky, Hila Peleg
Venue: ECOOP 2024
Year: 2024
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2024.22

Proposes Constrictor, a design framework that treats immutability as a first-class design concept rather than a type-system annotation. The approach helps programmers reason about and enforce immutability constraints at a higher level of abstraction.

Keywords: immutability, program design, object-oriented, verification

Mover Logic: A Concurrent Program Logic for Reduction and Rely-Guarantee Reasoning¶

Authors: Stephen N. Freund, Cormac Flanagan
Venue: ECOOP 2024
Year: 2024
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2024

Develops Mover Logic, a program logic for concurrent programs that combines reduction (commutativity of atomic actions) with rely-guarantee reasoning. The logic enables sound compositional verification of concurrent programs with fine-grained synchronization.

Keywords: concurrency, program logic, reduction, rely-guarantee, verification

Authors: Martin Vassor, Nobuko Yoshida
Venue: ECOOP 2024
Year: 2024
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2024

Introduces refinement types for multiparty session protocols, allowing protocols to carry data-dependent constraints. The theory is specification-agnostic, working with multiple protocol specification languages, and supports decidable protocol compliance checking.

Keywords: multiparty session types, refinement types, protocol verification, concurrency

Type Tailoring¶

Authors: Ashton Wiersdorf, Stephen Chang, Matthias Felleisen, Ben Greenman
Venue: ECOOP 2024
Year: 2024
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2024

Presents type tailoring, a meta-programming approach that allows programmers to specialize type checking for library functions. Type tailors can check domain-specific invariants beyond what the host type system provides, improving error messages and enabling deeper static checking.

Keywords: type systems, meta-programming, type tailoring, macros, Racket

Learning Gradual Typing Performance¶

Authors: Mohammad Wahiduzzaman Khan, Sheng Chen, Yi He
Venue: ECOOP 2024
Year: 2024
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2024

Develops a machine learning approach to predict performance characteristics of gradually typed programs, helping programmers choose type annotation strategies that avoid performance pitfalls. The model predicts slowdowns due to dynamic checks inserted by gradual typing.

Keywords: gradual typing, performance, machine learning, type annotations

Generalizing Shape Analysis with Gradual Types¶

Authors: Zeina Migeed, James Reed, Jason Ansel, Jens Palsberg
Venue: ECOOP 2024
Year: 2024
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2024

Extends shape analysis for tensor programs using gradual types, allowing partial shape information to be tracked statically with dynamic checks for unknown shapes. The approach improves bug detection in deep learning frameworks while supporting dynamic shape computation.

Keywords: shape analysis, gradual typing, tensors, deep learning, type systems

Inductive Predicate Synthesis Modulo Programs¶

Authors: Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler, Valentin Wüstholz, Arie Gurfinkel
Venue: ECOOP 2024
Year: 2024
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2024

Presents an algorithm for synthesizing inductive predicates for program verification that leverages existing program analyses. The approach modularly combines predicate synthesis with external tools, producing loop invariants and data structure specifications.

Keywords: program synthesis, inductive predicates, verification, invariant synthesis

Qafny: A Quantum-Program Verifier¶

Authors: Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, Xiaodi Wu
Venue: ECOOP 2024
Year: 2024
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2024

Qafny is a verification framework for quantum programs based on quantum Hoare logic and a Dafny-like assertion language. It supports automated verification of quantum circuit properties by translating quantum specifications into classical verification conditions.

Keywords: quantum computing, program verification, Hoare logic, quantum types

Tenspiler: A Verified Lifting-Based Compiler for Tensor Operations¶

Authors: Jie Qiu, Colin Cai, Sahil Bhatia, Niranjan Hasabnis, Sanjit Seshia, Alvin Cheung
Venue: ECOOP 2024
Year: 2024
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2024

Tenspiler lifts scalar programs operating on tensors into high-level tensor operation specifications, enabling verified compilation across different hardware backends. The lifting process is guided by a library of tensor algebra specifications and validated by Rosette.

Keywords: tensor operations, verified compilation, program lifting, synthesis

Compositional Symbolic Execution for Correctness and Incorrectness Reasoning¶

Authors: Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Petar Maksimović, Philippa Gardner
Venue: ECOOP 2024
Year: 2024
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2024

Presents a compositional symbolic execution framework that supports both correctness (over-approximate) and incorrectness (under-approximate) reasoning in a unified setting. The approach enables finding real bugs and proving program properties using the same symbolic execution infrastructure.

Keywords: symbolic execution, incorrectness logic, compositional verification, separation logic

Verifying Lock-free Search Structure Templates¶

Authors: Nisarg Patel, Dennis Shasha, Thomas Wies
Venue: ECOOP 2024
Year: 2024
DOI: https://doi.org/10.4230/LIPIcs.ECOOP.2024

Develops a verification methodology for parameterized lock-free data structure templates, allowing a single proof to cover many instantiations. The work uses a modular reasoning approach to verify linearizability of concurrent search structures like skiplists and BSTs.

Keywords: concurrency, lock-free, verification, linearizability, separation logic