Issue
DARTS, Volume 10, Issue 2
Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)
-
Part of:
Volume:
DARTS, Volume 10 (ECOOP 2024)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS)
Editors
Publication Details
- published at: 2024-09-12
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- DBLP: db/journals/darts/darts10
Access Numbers
- Detailed Access Statistics available here
-
Total Document Accesses (updated on a weekly basis):
0PDF Downloads
Documents
No documents found matching your filter selection.
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization
Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as
Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{evenmendoza_et_al:DARTS.10.2.0,
author = {Even-Mendoza, Karine and Monat, Rapha\"{e}l},
title = {{Front Matter, Table of Contents, Preface, Conference Organization}},
pages = {0:i--0:xii},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Even-Mendoza, Karine and Monat, Rapha\"{e}l},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.0},
URN = {urn:nbn:de:0030-drops-208982},
doi = {10.4230/DARTS.10.2.0},
annote = {Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Artifact
Runtime Instrumentation for Reactive Components (Artifact)
Abstract
Reactive software calls for instrumentation methods that uphold the reactive attributes of systems. Runtime verification sets another demand on the instrumentation, namely that the trace event sequences it reports to monitors are sound, i.e., they reflect actual executions of the system under scrutiny. Our companion paper, "Runtime Instrumentation for Reactive Components", presents RIARC, a novel decentralised instrumentation algorithm for outline monitors that meets these two demands. RIARC uses a next-hop IP routing approach to rearrange and report events soundly to monitors despite the potential trace event loss or reordering stemming from the asynchrony of reactive systems.
The companion paper shows our corresponding RIARC Erlang implementation to be correct through rigorous systematic testing. We also assess RIARC via extensive empirical experiments, subjecting it to large realistic workloads in order to ascertain its reactiveness. This artefact packages the Erlang implementation, systematic tests that demonstrate its correctness, data sets obtained from our original empirical experiments detailed in the companion paper, and the scripts to rerun and replicate these results under lower workloads.
Cite as
Luca Aceto, Duncan Paul Attard, Adrian Francalanza, and Anna Ingólfsdóttir. Runtime Instrumentation for Reactive Components (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{aceto_et_al:DARTS.10.2.1,
author = {Aceto, Luca and Attard, Duncan Paul and Francalanza, Adrian and Ing\'{o}lfsd\'{o}ttir, Anna},
title = {{Runtime Instrumentation for Reactive Components (Artifact)}},
pages = {1:1--1:4},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Aceto, Luca and Attard, Duncan Paul and Francalanza, Adrian and Ing\'{o}lfsd\'{o}ttir, Anna},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.1},
URN = {urn:nbn:de:0030-drops-208991},
doi = {10.4230/DARTS.10.2.1},
annote = {Keywords: Runtime instrumentation, decentralised monitoring, reactive systems}
}
Document
Artifact
Dynamically Generating Callback Summaries for Enhancing Static Analysis (Artifact)
Abstract
Interprocedural static analyses require a complete and precise callgraph. Since third-party libraries are responsible for large portions of the code of an app, a substantial fraction of the effort in callgraph generation is therefore spent on the library code for each app. For analyses that are oblivious to the inner workings of a library and only require the user code to be processed, the library can be replaced with a summary that allows to reconstruct the callbacks from library code back to user code. To improve performance, we propose the automatic generation and use of precise pre-computed callgraph summaries for commonly used libraries. Reflective method calls within libraries and callback-driven APIs pose further challenges for generating precise callgraphs using static analysis. Pre-computed summaries can also help analyses avoid these challenges.
We present CGMiner, an approach for automatically generating callgraph models for library code. It dynamically observes sample apps that use one or more particular target libraries. As we show, CGMiner yields more than 94% of correct edges, whereas existing work only achieves around 33% correct edges. CGMiner avoids the high false positive rate of existing tools. We show that CGMiner integrated into FlowDroid uncovers 40% more data flows than our baseline without callback summaries.
This artifact description describes how the artifacts can be build.
Cite as
Steven Arzt, Marc Miltenberger, and Julius Näumann. Dynamically Generating Callback Summaries for Enhancing Static Analysis (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 2:1-2:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{arzt_et_al:DARTS.10.2.2,
author = {Arzt, Steven and Miltenberger, Marc and N\"{a}umann, Julius},
title = {{Dynamically Generating Callback Summaries for Enhancing Static Analysis (Artifact)}},
pages = {2:1--2:5},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Arzt, Steven and Miltenberger, Marc and N\"{a}umann, Julius},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.2},
URN = {urn:nbn:de:0030-drops-209009},
doi = {10.4230/DARTS.10.2.2},
annote = {Keywords: dynamic analysis, callback detection, java, android}
}
Document
Artifact
A Language-Based Version Control System for Python (Artifact)
Abstract
We extend prior work on a language-based approach to versioned software development to support versioned programs with mutable state and evolving method interfaces. Unlike the traditional approach of mainstream version control systems, where a textual diff represents each evolution step, we treat versions as programming elements. Each evolution step, merge operation, and version relationship is represented explicitly in a multifaceted code representation. This provides static guarantees for safe code reuse from previous versions and forward and backwards compatibility between versions, allowing clients to use newly introduced code without needing to refactor their program manually. By lifting versioning to the language level, we pave the way for tools that interact with software repositories to have more insight into a system’s behavior evolution. We instantiate our work in the Python programming language and demonstrate its applicability regarding common evolution and refactoring patterns found in different versions of popular Python packages.
Cite as
Luís Carvalho and João Costa Seco. A Language-Based Version Control System for Python (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{carvalho_et_al:DARTS.10.2.3,
author = {Carvalho, Lu{\'\i}s and Costa Seco, Jo\~{a}o},
title = {{A Language-Based Version Control System for Python (Artifact)}},
pages = {3:1--3:2},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Carvalho, Lu{\'\i}s and Costa Seco, Jo\~{a}o},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.3},
URN = {urn:nbn:de:0030-drops-209017},
doi = {10.4230/DARTS.10.2.3},
annote = {Keywords: Software evolution, type theory}
}
Document
Artifact
Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency (Artifact)
Abstract
This artifact is a Docker image containing the snapshot of the source code, a built command-line binary, and an interactive demonstration of the type-checker developed for IFC language of the main paper. This article discusses its scope, contents and methods of use.
Cite as
Farzaneh Derakhshan, Stephanie Balzer, and Yue Yao. Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 4:1-4:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{derakhshan_et_al:DARTS.10.2.4,
author = {Derakhshan, Farzaneh and Balzer, Stephanie and Yao, Yue},
title = {{Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency (Artifact)}},
pages = {4:1--4:3},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Derakhshan, Farzaneh and Balzer, Stephanie and Yao, Yue},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.4},
URN = {urn:nbn:de:0030-drops-209020},
doi = {10.4230/DARTS.10.2.4},
annote = {Keywords: Regrading policies, session types, progress-sensitive noninterference}
}
Document
Artifact
Mutation-Based Lifted Repair of Software Product Lines (Artifact)
Abstract
In this work, we describe the installation, usage, and evaluation results of the tool SPLAllRepair, which is introduced by the paper "Mutation-based Lifted Repair of Software Product Lines". We provide step-by-step instructions on how to download, run, and compare the tool’s outputs to outputs described in the paper. The tool implements a novel lifted repair algorithm for program families (Software Product Lines - SPLs) based on code mutations. The inputs of our algorithm are an erroneous SPL and a specification given in the form of assertions. We use variability encoding to transform the given SPL into a single program, called family simulator, which is translated into a set of SMT formulas whose conjunction is satisfiable iff the simulator (i.e. the input SPL) violates an assertion. We use a predefined set of mutations applied to feature and program expressions of the given SPL. The algorithm repeatedly mutates the erroneous family simulator and checks if it becomes (bounded) correct. The outputs are all minimal repairs in the form of minimal number of (feature and program) expression replacements such that the repaired SPL is (bounded) correct with respect to a given set of assertions. We present the experimental results showing that our approach is able to successfully repair various interesting #ifdef-based C SPLs.
Cite as
Aleksandar S. Dimovski. Mutation-Based Lifted Repair of Software Product Lines (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 5:1-5:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{dimovski:DARTS.10.2.5,
author = {Dimovski, Aleksandar S.},
title = {{Mutation-Based Lifted Repair of Software Product Lines (Artifact)}},
pages = {5:1--5:5},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Dimovski, Aleksandar S.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.5},
URN = {urn:nbn:de:0030-drops-209036},
doi = {10.4230/DARTS.10.2.5},
annote = {Keywords: Program repair, Software Product Lines, Code mutations, Variability encoding}
}
Document
Artifact
Pure Methods for roDOT (Artifact)
Abstract
The artifact for the paper Pure methods for roDOT (ECOOP 2024) contains the Coq mechanization of the theorems appearing in the paper, and the necessary definitions and lemmata. Additionally, the artifact contains a mechanization of the roDOT calculus presented in an earlier paper Reference mutability for DOT (ECOOP 2020). We used the calculus from this paper as the baseline for our paper, but it has not been mechanized before.
The functionality of the artifact is the ability to verify the correctness of the theorems by running Coq.
Our code is based on a mechanization of a soundness proof for Field Mutable DOT.
Cite as
Vlastimil Dort, Yufeng Li, Ondřej Lhoták, and Pavel Parízek. Pure Methods for roDOT (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 6:1-6:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{dort_et_al:DARTS.10.2.6,
author = {Dort, Vlastimil and Li, Yufeng and Lhot\'{a}k, Ond\v{r}ej and Par{\'\i}zek, Pavel},
title = {{Pure Methods for roDOT (Artifact)}},
pages = {6:1--6:8},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Dort, Vlastimil and Li, Yufeng and Lhot\'{a}k, Ond\v{r}ej and Par{\'\i}zek, Pavel},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.6},
URN = {urn:nbn:de:0030-drops-209046},
doi = {10.4230/DARTS.10.2.6},
annote = {Keywords: type systems, DOT calculus, pure methods}
}
Document
Artifact
Rose: Composable Autodiff for the Interactive Web (Artifact)
Abstract
Reverse-mode automatic differentiation (autodiff) has been popularized by deep learning, but its ability to compute gradients is also valuable for interactive use cases such as bidirectional computer-aided design, embedded physics simulations, visualizing causal inference, and more. Unfortunately, the web is ill-served by existing autodiff frameworks, which use autodiff strategies that perform poorly on dynamic scalar programs, and pull in heavy dependencies that would result in unacceptable webpage sizes. This document accompanies the research paper introducing Rose, a lightweight autodiff framework for the web using a new hybrid approach to reverse-mode autodiff, blending conventional tracing and transformation techniques in a way that uses the host language for metaprogramming while also allowing the programmer to explicitly define reusable functions that comprise a larger differentiable computation. We demonstrate the value of the Rose design by porting two differentiable physics simulations, and evaluate its performance on an optimization-based diagramming application, showing Rose outperforming the state-of-the-art in web-based autodiff by multiple orders of magnitude.
Cite as
Sam Estep, Wode Ni, Raven Rothkopf, and Joshua Sunshine. Rose: Composable Autodiff for the Interactive Web (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 7:1-7:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{estep_et_al:DARTS.10.2.7,
author = {Estep, Sam and Ni, Wode and Rothkopf, Raven and Sunshine, Joshua},
title = {{Rose: Composable Autodiff for the Interactive Web (Artifact)}},
pages = {7:1--7:4},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Estep, Sam and Ni, Wode and Rothkopf, Raven and Sunshine, Joshua},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.7},
URN = {urn:nbn:de:0030-drops-209053},
doi = {10.4230/DARTS.10.2.7},
annote = {Keywords: Automatic differentiation, differentiable programming, compilers, web}
}
Document
Artifact
Fair Join Pattern Matching for Actors (Artifact)
Abstract
Join patterns provide a promising approach to the development of concurrent and distributed message-passing applications. Several variations and implementations have been presented in the literature - but various aspects remain under-explored: in particular, how to specify a suitable notion of message matching, how to implement it correctly and efficiently, and how to systematically evaluate the implementation performance.
In this work we focus on actor-based programming, and study the application of join patterns with conditional guards (i.e., the most expressive and challenging version of join patterns in literature). We formalise a novel specification of fair and deterministic join pattern matching, ensuring that older messages are always consumed if they can be matched. We present a stateful, tree-based join pattern matching algorithm and prove that it correctly implements our fair and deterministic matching specification. We present a novel Scala 3 actor library (called JoinActors) that implements our join pattern formalisation, leveraging macros to provide an intuitive API. Finally, we evaluate the performance of our implementation, by introducing a systematic benchmarking approach that takes into account the nuances of join pattern matching (in particular, its sensitivity to input traffic and complexity of patterns and guards).
Cite as
Philipp Haller, Ayman Hussein, Hernán Melgratti, Alceste Scalas, and Emilio Tuosto. Fair Join Pattern Matching for Actors (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 8:1-8:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{haller_et_al:DARTS.10.2.8,
author = {Haller, Philipp and Hussein, Ayman and Melgratti, Hern\'{a}n and Scalas, Alceste and Tuosto, Emilio},
title = {{Fair Join Pattern Matching for Actors (Artifact)}},
pages = {8:1--8:3},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Haller, Philipp and Hussein, Ayman and Melgratti, Hern\'{a}n and Scalas, Alceste and Tuosto, Emilio},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.8},
URN = {urn:nbn:de:0030-drops-209062},
doi = {10.4230/DARTS.10.2.8},
annote = {Keywords: Concurrency, join patterns, join calculus, actor model}
}
Document
Artifact
Constrictor: Immutability as a Design Concept (Artifact)
Abstract
Many object-oriented applications in algorithm design rely on objects never changing during their lifetime. This is often tackled by marking object references as read-only, e.g., using the const keyword in C++. In other languages like Python or Java where such a concept does not exist, programmers rely on best practices that are entirely unenforced. While reliance on best practices is obviously too permissive, const-checking is too restrictive: it is possible for a method to mutate the internal state while still satisfying the property we expect from an "immutable" object in this setting. We would therefore like to enforce the immutability of an object’s abstract state.
We check an object’s immutability through a view of its abstract state: for instances of an immutable class, the view does not change when running any of the class’s methods, even if some of the internal state does change. If all methods of a class are verified as non-mutating, we can deem the entire class view-immutable. We present an SMT-based algorithm to check view-immutability, and implement it in our linter/verifier, Constrictor.
We evaluate Constrictor on 51 examples of immutability-related design violations. Our evaluation shows that Constrictor is effective at catching a variety of prototypical design violations, and does so in seconds. We also explore Constrictor with two real-world case studies.
Cite as
Elad Kinsbruner, Shachar Itzhaky, and Hila Peleg. Constrictor: Immutability as a Design Concept (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 9:1-9:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{kinsbruner_et_al:DARTS.10.2.9,
author = {Kinsbruner, Elad and Itzhaky, Shachar and Peleg, Hila},
title = {{Constrictor: Immutability as a Design Concept (Artifact)}},
pages = {9:1--9:4},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Kinsbruner, Elad and Itzhaky, Shachar and Peleg, Hila},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.9},
URN = {urn:nbn:de:0030-drops-209071},
doi = {10.4230/DARTS.10.2.9},
annote = {Keywords: Immutability, Design Enforcement, SMT, Liskov Substitution Principle, Object-oriented Programming}
}
Document
Artifact
Fearless Asynchronous Communications with Timed Session Types in Rust (Artifact)
Abstract
We introduce MultiCrusty^T, a Rust toolchain designed to facilitate the implementation of safe affine timed protocols. MultiCrusty^T leverages generic types and the time library to handle timed communications, integrated with optional types for affinity. This artifact allows to evaluate our approach by running examples from the literature, real-world use cases and protocols from real-time systems, featured in the related article, showcasing the correctness by construction of our approach. We allow to see the performance of our solution by running benchmarks and generating graphs, highlighting a less than 10% compile-time and runtime overhead compared with an untimed implementation. We also demonstrate how to implement, step by step, your own timed protocols, from a very basic one with only two parties and simple interactions, to complex ones with more than three parties, choices and recursion.
Cite as
Nicolas Lagaillardie, Ping Hou, and Nobuko Yoshida. Fearless Asynchronous Communications with Timed Session Types in Rust (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 10:1-10:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{lagaillardie_et_al:DARTS.10.2.10,
author = {Lagaillardie, Nicolas and Hou, Ping and Yoshida, Nobuko},
title = {{Fearless Asynchronous Communications with Timed Session Types in Rust (Artifact)}},
pages = {10:1--10:3},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Lagaillardie, Nicolas and Hou, Ping and Yoshida, Nobuko},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.10},
URN = {urn:nbn:de:0030-drops-209084},
doi = {10.4230/DARTS.10.2.10},
annote = {Keywords: session types, affine types, \pi-calculus, asynchrony, timeouts, failures, Rust}
}
Document
Artifact
InferType: A Compiler Toolkit for Implementing Efficient Constraint-Based Type Inference (Artifact)
Abstract
Supporting automatic type inference is in demand in modern language development. It is a challenging task but without appropriate supporting toolkits. This paper presents InferType, a Java library that helps implement constraint-based type inference. A compiler writer uses InferType’s classes and methods to describe type constraints and typing rules for type inference. InferType then performs constraint solving by translation to the Z3 SMT solver. InferType is equipped with our developed optimization technique. It reduces the search space for type variables by pre-computing the structures of those type variables for mitigating the performance bottleneck of constraint solving with deeply nested types. We use InferType to implement type inference for a subset of Python, and conduct experiments to evaluate how the developed optimization technique can affect the performance of type inference. Our results show that InferType’s optimization can greatly mitigate the performance bottleneck for programs with deeply nested types, and can potentially improve the performance for large nested types.
Cite as
Senxi Li, Tetsuro Yamazaki, and Shigeru Chiba. InferType: A Compiler Toolkit for Implementing Efficient Constraint-Based Type Inference (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 11:1-11:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{li_et_al:DARTS.10.2.11,
author = {Li, Senxi and Yamazaki, Tetsuro and Chiba, Shigeru},
title = {{InferType: A Compiler Toolkit for Implementing Efficient Constraint-Based Type Inference (Artifact)}},
pages = {11:1--11:2},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Li, Senxi and Yamazaki, Tetsuro and Chiba, Shigeru},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.11},
URN = {urn:nbn:de:0030-drops-209094},
doi = {10.4230/DARTS.10.2.11},
annote = {Keywords: Domain Specific Languages, Compilation, Static Analysis, Type Inference, Constraint Solving, SMT Solver}
}
Document
Artifact
Qafny: A Quantum-Program Verifier (Artifact)
Abstract
This artifact contains the Coq theory files for the Qafny proof system, including the formalism of the Qafny syntax, semantics, type system, and proof system, with the theorem proofs of type soundness, proof system soundness and completeness. It also contains a the compiled Dafny example programs generated from our Qafny-to-Dafny prototype compiler. These example programs serve as the validations of our Qafny-to-Dafny prototype compiler mechanism. The main work is introduced in the Qafny paper, which develops a separation logic style verification framework for quantum programs.
Cite as
Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, and Xiaodi Wu. Qafny: A Quantum-Program Verifier (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 12:1-12:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{li_et_al:DARTS.10.2.12,
author = {Li, Liyi and Zhu, Mingwei and Cleaveland, Rance and Nicolellis, Alexander and Lee, Yi and Chang, Le and Wu, Xiaodi},
title = {{Qafny: A Quantum-Program Verifier (Artifact)}},
pages = {12:1--12:2},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Li, Liyi and Zhu, Mingwei and Cleaveland, Rance and Nicolellis, Alexander and Lee, Yi and Chang, Le and Wu, Xiaodi},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.12},
URN = {urn:nbn:de:0030-drops-209104},
doi = {10.4230/DARTS.10.2.12},
annote = {Keywords: Quantum Computing, Automated Verification, Separation Logic}
}
Document
Artifact
Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Artifact)
Abstract
This artifact is a companion to the paper "Compositional Symbolic Execution for Correctness and Incorrectness Reasoning". It contains the source code of the Gillian compositional symbolic execution (CSE) platform, in which we added the incorrectness reasoning capabilities, and the benchmarks used in the evaluation of the paper. It also contains a Haskell demonstrator CSE engine that directly implements the CSE engine inference rules presented in the paper.
Cite as
Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Nat Karmios, Petar Maksimović, and Philippa Gardner. Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 13:1-13:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{loow_et_al:DARTS.10.2.13,
author = {L\"{o}\"{o}w, Andreas and Nantes-Sobrinho, Daniele and Ayoun, Sacha-\'{E}lie and Cronj\"{a}ger, Caroline and Karmios, Nat and Maksimovi\'{c}, Petar and Gardner, Philippa},
title = {{Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Artifact)}},
pages = {13:1--13:2},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {L\"{o}\"{o}w, Andreas and Nantes-Sobrinho, Daniele and Ayoun, Sacha-\'{E}lie and Cronj\"{a}ger, Caroline and Karmios, Nat and Maksimovi\'{c}, Petar and Gardner, Philippa},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.13},
URN = {urn:nbn:de:0030-drops-209110},
doi = {10.4230/DARTS.10.2.13},
annote = {Keywords: separation logic, incorrectness logic, symbolic execution, bi-abduction}
}
Document
Artifact
Generalizing Shape Analysis with Gradual Types (Artifact)
Abstract
This is the artifact for the conference article below.
Cite as
Zeina Migeed and Jens Palsberg. Generalizing Shape Analysis with Gradual Types (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 14:1-14:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{migeed_et_al:DARTS.10.2.14,
author = {Migeed, Zeina and Palsberg, Jens},
title = {{Generalizing Shape Analysis with Gradual Types (Artifact)}},
pages = {14:1--14:2},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Migeed, Zeina and Palsberg, Jens},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.14},
URN = {urn:nbn:de:0030-drops-209125},
doi = {10.4230/DARTS.10.2.14},
annote = {Keywords: Gradual Types, Type Theory}
}
Document
Artifact
Verifying Lock-Free Search Structure Templates (Artifact)
Abstract
We present and verify template algorithms for lock-free concurrent search structures that cover a broad range of existing implementations based on lists and skiplists. Our linearizability proofs are fully mechanized in the concurrent separation logic Iris. The proofs are modular and cover the broader design space of the underlying algorithms by parameterizing the verification over aspects such as the low-level representation of nodes and the style of data structure maintenance. As a further technical contribution, we present a mechanization of a recently proposed method for reasoning about future-dependent linearization points using hindsight arguments. The mechanization builds on Iris' support for prophecy reasoning and user-defined ghost resources. We demonstrate that the method can help to reduce the proof effort compared to direct prophecy-based proofs.
Cite as
Nisarg Patel, Dennis Shasha, and Thomas Wies. Verifying Lock-Free Search Structure Templates (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 15:1-15:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{patel_et_al:DARTS.10.2.15,
author = {Patel, Nisarg and Shasha, Dennis and Wies, Thomas},
title = {{Verifying Lock-Free Search Structure Templates (Artifact)}},
pages = {15:1--15:2},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Patel, Nisarg and Shasha, Dennis and Wies, Thomas},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.15},
URN = {urn:nbn:de:0030-drops-209138},
doi = {10.4230/DARTS.10.2.15},
annote = {Keywords: skiplists, lock-free, separation logic, linearizability, future-dependent linearization points, hindsight reasoning}
}
Document
Artifact
Ozone: Fully Out-of-Order Choreographies (Artifact)
Abstract
Choreographic programming is a paradigm for writing distributed applications. It allows programmers to write a single program, called a choreography, that can be compiled to generate correct implementations of each process in the application. Although choreographies provide good static guarantees, they can exhibit high latency when messages or processes are delayed. This is because processes in a choreography typically execute in a fixed, deterministic order, and cannot adapt to the order that messages arrive at runtime. In non-choreographic code, programmers can address this problem by allowing processes to execute out of order - for instance by using futures or reactive programming. However, in choreographic code, out-of-order process execution can lead to serious and subtle bugs, called communication integrity violations (CIVs).
In this paper, we develop a model of choreographic programming for out-of-order processes that guarantees absence of CIVs and deadlocks. As an application of our approach, we also introduce an API for safe non-blocking communication via futures in the choreographic programming language Choral. The API allows processes to execute out of order, participate in multiple choreographies concurrently, and to handle unordered data messages. We provide an illustrative evaluation of our API, showing that out-of-order execution can reduce latency and increase throughput by overlapping communication with computation.
Cite as
Dan Plyukhin, Marco Peressotti, and Fabrizio Montesi. Ozone: Fully Out-of-Order Choreographies (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 16:1-16:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{plyukhin_et_al:DARTS.10.2.16,
author = {Plyukhin, Dan and Peressotti, Marco and Montesi, Fabrizio},
title = {{Ozone: Fully Out-of-Order Choreographies (Artifact)}},
pages = {16:1--16:2},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Plyukhin, Dan and Peressotti, Marco and Montesi, Fabrizio},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.16},
URN = {urn:nbn:de:0030-drops-209145},
doi = {10.4230/DARTS.10.2.16},
annote = {Keywords: Choreographic programming, Asynchrony, Concurrency.}
}
Document
Artifact
Tenspiler: A Verified-Lifting-Based Compiler for Tensor Operations (Artifact)
Abstract
In the related article, we described Tenspiler, a verified-lifting-based compiler that translates sequential programs to tensor operations. We further demonstrated its effectiveness by translating 69 benchmarks from into 6 different DSL targets and evaluating their performance against the baseline. This artifact includes the implementation of Tenspiler as well as files used to reproduce those results.
Cite as
Jie Qiu, Colin Cai, Sahil Bhatia, Niranjan Hasabnis, Sanjit A. Seshia, and Alvin Cheung. Tenspiler: A Verified-Lifting-Based Compiler for Tensor Operations (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 17:1-17:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{qiu_et_al:DARTS.10.2.17,
author = {Qiu, Jie and Cai, Colin and Bhatia, Sahil and Hasabnis, Niranjan and Seshia, Sanjit A. and Cheung, Alvin},
title = {{Tenspiler: A Verified-Lifting-Based Compiler for Tensor Operations (Artifact)}},
pages = {17:1--17:2},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Qiu, Jie and Cai, Colin and Bhatia, Sahil and Hasabnis, Niranjan and Seshia, Sanjit A. and Cheung, Alvin},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.17},
URN = {urn:nbn:de:0030-drops-209150},
doi = {10.4230/DARTS.10.2.17},
annote = {Keywords: Program Synthesis, Code Transpilation, Tensor DSLs, Verification}
}
Document
Artifact
Compiling with Arrays (Artifact)
Abstract
Linear algebra computations are foundational for neural networks and machine learning, often handled through arrays. While many functional programming languages feature lists and recursion, arrays in linear algebra demand constant-time access and bulk operations. To bridge this gap, some languages represent arrays as (eager) functions instead of lists. In this paper, we connect this idea to a formal logical foundation by interpreting functions as the usual negative types from polarized type theory, and arrays as the corresponding dual positive version of the function type. Positive types are defined to have a single elimination form whose computational interpretation is pattern matching. Just like (positive) product types bind two variables during pattern matching, (positive) array types bind variables with multiplicity during pattern matching. We follow a similar approach for Booleans by introducing conditionally-defined variables.
The positive formulation for the array type enables us to combine typed partial evaluation and common subexpression elimination into an elegant algorithm whose result enjoys a property we call maximal fission, which we argue can be beneficial for further optimizations. For this purpose, we present the novel intermediate representation indexed administrative normal form (A_{i}NF), which relies on the formal logical foundation of the positive formulation for the array type to facilitate maximal loop fission and subsequent optimizations. A_{i}NF is normal with regard to commuting conversion for both let-bindings and for-loops, leading to flat and maximally fissioned terms. We mechanize the translation and normalization from a simple surface language to A_{i}NF, establishing that the process terminates, preserves types, and produces maximally fissioned terms.
Cite as
David Richter, Timon Böhler, Pascal Weisenburger, and Mira Mezini. Compiling with Arrays (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 18:1-18:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{richter_et_al:DARTS.10.2.18,
author = {Richter, David and B\"{o}hler, Timon and Weisenburger, Pascal and Mezini, Mira},
title = {{Compiling with Arrays (Artifact)}},
pages = {18:1--18:7},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Richter, David and B\"{o}hler, Timon and Weisenburger, Pascal and Mezini, Mira},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.18},
URN = {urn:nbn:de:0030-drops-209168},
doi = {10.4230/DARTS.10.2.18},
annote = {Keywords: array languages, functional programming, domain-specific languages, normalization by evaluation, common subexpression elimination, polarity, positive function type, intrinsic types}
}
Document
Artifact
Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems (Artifact)
Abstract
Synchronous languages such as Lustre and Scade are used to implement safety-critical control systems; proving such programs correct and having the proved properties apply to the compiled code is therefore equally critical. We introduce Pipit, a small synchronous language embedded in F*, designed for verifying control systems and executing them in real-time. Pipit includes a verified translation to transition systems; by reusing F*’s existing proof automation, certain safety properties can be automatically proved by k-induction on the transition system. Pipit can also generate executable code in a subset of F* which is suitable for compilation and real-time execution on embedded devices. The executable code is deterministic and total and preserves the semantics of the original program.
Cite as
Amos Robinson and Alex Potanin. Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 19:1-19:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{robinson_et_al:DARTS.10.2.19,
author = {Robinson, Amos and Potanin, Alex},
title = {{Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems (Artifact)}},
pages = {19:1--19:2},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Robinson, Amos and Potanin, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.19},
URN = {urn:nbn:de:0030-drops-209177},
doi = {10.4230/DARTS.10.2.19},
annote = {Keywords: Lustre, streaming, reactive, verification}
}
Document
Artifact
Java Bytecode Normalization for Code Similarity Analysis (Artifact)
Abstract
This artifact supports the claim that different Java compilation environments can produce significantly different bytecode and that bytecode normalization applied via our tool jNorm heavily decreases the amount of compilation differences and helps boost the performance of subsequent code similarity analysis. Our artifact provides the source code of the tool jNorm and all scripts needed to reproduce the results we presented in our evaluation. Furthermore, it contains a study on the usage of different Java compilers and target levels within popular open-source projects, which showcases that the JDK compiler is by far the most relevant compiler in practice.
Cite as
Stefan Schott, Serena Elisa Ponta, Wolfram Fischer, Jonas Klauke, and Eric Bodden. Java Bytecode Normalization for Code Similarity Analysis (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 20:1-20:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{schott_et_al:DARTS.10.2.20,
author = {Schott, Stefan and Ponta, Serena Elisa and Fischer, Wolfram and Klauke, Jonas and Bodden, Eric},
title = {{Java Bytecode Normalization for Code Similarity Analysis (Artifact)}},
pages = {20:1--20:3},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Schott, Stefan and Ponta, Serena Elisa and Fischer, Wolfram and Klauke, Jonas and Bodden, Eric},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.20},
URN = {urn:nbn:de:0030-drops-209189},
doi = {10.4230/DARTS.10.2.20},
annote = {Keywords: Bytecode, Java Compiler, Code Similarity Analysis}
}
Document
Artifact
Optimizing Layout of Recursive Datatypes with Marmoset (Artifact)
Abstract
While programmers know that memory representation of data structures can have significant effects on performance, compiler support to optimize the layout of those structures is an under-explored field. Prior work has optimized the layout of individual, non-recursive structures without considering how collections of those objects in linked or recursive data structures are laid out.
This work introduces Marmoset, a compiler that optimizes the layouts of algebraic datatypes, with a special focus on producing highly optimized, packed data layouts where recursive structures can be traversed with minimal pointer chasing. Marmoset performs an analysis of how a recursive ADT is used across functions to choose a global layout that promotes simple, strided access for that ADT in memory. It does so by building and solving a constraint system to minimize an abstract cost model, yielding a predicted efficient layout for the ADT. Marmoset then builds on top of Gibbon, a prior compiler for packed, mostly-serial representations, to synthesize optimized ADTs. We show experimentally that Marmoset is able to choose optimal layouts across a series of microbenchmarks and case studies, outperforming both Gibbon’s baseline approach, as well as MLton, a Standard ML compiler that uses traditional pointer-heavy representations.
Cite as
Vidush Singhal, Chaitanya Koparkar, Joseph Zullo, Artem Pelenitsyn, Michael Vollmer, Mike Rainey, Ryan Newton, and Milind Kulkarni. Optimizing Layout of Recursive Datatypes with Marmoset (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 21:1-21:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{singhal_et_al:DARTS.10.2.21,
author = {Singhal, Vidush and Koparkar, Chaitanya and Zullo, Joseph and Pelenitsyn, Artem and Vollmer, Michael and Rainey, Mike and Newton, Ryan and Kulkarni, Milind},
title = {{Optimizing Layout of Recursive Datatypes with Marmoset (Artifact)}},
pages = {21:1--21:10},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Singhal, Vidush and Koparkar, Chaitanya and Zullo, Joseph and Pelenitsyn, Artem and Vollmer, Michael and Rainey, Mike and Newton, Ryan and Kulkarni, Milind},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.21},
URN = {urn:nbn:de:0030-drops-209199},
doi = {10.4230/DARTS.10.2.21},
annote = {Keywords: Tree traversals, Compilers, Data layout optimization, Dense data layout}
}
Document
Artifact
Formalizing, Mechanizing, and Verifying Class-Based Refinement Types (Artifact)
Abstract
This is the artifact description of an ECOOP paper. A new expressive formalization of class-based refinement types is proposed in the paper. We enrich the formalization by analyzing its meta-theory and algorithmic verification. The meta-theory and algorithmic verification have been mechanized and implemented. We discuss details of the mechanization and implementation in this document.
Cite as
Ke Sun, Di Wang, Sheng Chen, Meng Wang, and Dan Hao. Formalizing, Mechanizing, and Verifying Class-Based Refinement Types (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 22:1-22:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{sun_et_al:DARTS.10.2.22,
author = {Sun, Ke and Wang, Di and Chen, Sheng and Wang, Meng and Hao, Dan},
title = {{Formalizing, Mechanizing, and Verifying Class-Based Refinement Types (Artifact)}},
pages = {22:1--22:3},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Sun, Ke and Wang, Di and Chen, Sheng and Wang, Meng and Hao, Dan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.22},
URN = {urn:nbn:de:0030-drops-209209},
doi = {10.4230/DARTS.10.2.22},
annote = {Keywords: Refinement Types, Program Verification, Object-oriented Programming}
}
Document
Artifact
Refinements for Multiparty Message-Passing Protocols: Specification-Agnostic Theory and Implementation (Artifact)
Abstract
Multiparty message-passing protocols are notoriously difficult to design, due to interaction mismatches that lead to errors such as deadlocks. Existing protocol specification formats have been developed to prevent such errors (e.g. multiparty session types (MPST)). In order to further constrain protocols, specifications can be extended with refinements, i.e. logical predicates to control the behaviour of the protocol based on previous values exchanged. Unfortunately, existing refinement theories and implementations are tightly coupled with specification formats.
This artifact accompanies [Martin Vassor and Nobuko Yoshida, 2024]. It presents an implementation of the framework presented in this paper.
Cite as
Martin Vassor and Nobuko Yoshida. Refinements for Multiparty Message-Passing Protocols: Specification-Agnostic Theory and Implementation (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 23:1-23:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{vassor_et_al:DARTS.10.2.23,
author = {Vassor, Martin and Yoshida, Nobuko},
title = {{Refinements for Multiparty Message-Passing Protocols: Specification-Agnostic Theory and Implementation (Artifact)}},
pages = {23:1--23:5},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Vassor, Martin and Yoshida, Nobuko},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.23},
URN = {urn:nbn:de:0030-drops-209212},
doi = {10.4230/DARTS.10.2.23},
annote = {Keywords: Message-Passing Concurrency, Session Types, Specification}
}
Document
Artifact
Type Tailoring (Artifact)
Abstract
Type systems evolve too slowly to keep up with the quick evolution of libraries - especially libraries that introduce abstractions. Type tailoring offers a lightweight solution by equipping the core language with an API for modifying the elaboration of surface code into the internal language of the typechecker. Through user-programmable elaboration, tailoring rules appear to improve the precision and expressiveness of the underlying type system. Furthermore, type tailoring cooperates with the host type system by expanding to code that the host then typechecks. In the context of a hygienic metaprogramming system, tailoring rules can even harmoniously compose with one another.
Type tailoring has emerged as a theme across several languages and metaprogramming systems, but never with direct support and rarely in the same shape twice. For example, both OCaml and Typed Racket enable forms of tailoring, but in quite different ways. This paper identifies key dimensions of type tailoring systems and tradeoffs along each dimension. It demonstrates the usefulness of tailoring with examples that cover sized vectors, database queries, and optional types. Finally, it outlines a vision for future research at the intersection of types and metaprogramming.
Cite as
Ashton Wiersdorf, Stephen Chang, Matthias Felleisen, and Ben Greenman. Type Tailoring (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 24:1-24:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{wiersdorf_et_al:DARTS.10.2.24,
author = {Wiersdorf, Ashton and Chang, Stephen and Felleisen, Matthias and Greenman, Ben},
title = {{Type Tailoring (Artifact)}},
pages = {24:1--24:2},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Wiersdorf, Ashton and Chang, Stephen and Felleisen, Matthias and Greenman, Ben},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.24},
URN = {urn:nbn:de:0030-drops-209220},
doi = {10.4230/DARTS.10.2.24},
annote = {Keywords: Types, Metaprogramming, Macros, Partial Evaluation}
}
Document
Artifact
Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Artifact)
Abstract
This artifact provides a translator from Pika code to SuSLik specifications. Additionally, it contains a test suite and benchmark suite. These suites are fully automated using provided scripts. All source code is included.
Cite as
David Young, Ziyi Yang, Ilya Sergey, and Alex Potanin. Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 25:1-25:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{young_et_al:DARTS.10.2.25,
author = {Young, David and Yang, Ziyi and Sergey, Ilya and Potanin, Alex},
title = {{Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Artifact)}},
pages = {25:1--25:2},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Young, David and Yang, Ziyi and Sergey, Ilya and Potanin, Alex},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.25},
URN = {urn:nbn:de:0030-drops-209239},
doi = {10.4230/DARTS.10.2.25},
annote = {Keywords: Program Synthesis, Separation Logic, Functional Programming}
}
Document
Artifact
CtChecker: A Precise, Sound and Efficient Static Analysis for Constant-Time Programming (Artifact)
Abstract
This artifact includes the implementation of the CtChecker analysis toolchain described in the corresponding paper. We provide two options to run CtChecker, building it from source or running the pre-built tool with Docker. All evaluated benchmark source code are provided in the artifact. A walkthrough of how to reproduce the evaluation results in the paper is provided in the Appendix.
Cite as
Quan Zhou, Sixuan Dang, and Danfeng Zhang. CtChecker: A Precise, Sound and Efficient Static Analysis for Constant-Time Programming (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 26:1-26:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{zhou_et_al:DARTS.10.2.26,
author = {Zhou, Quan and Dang, Sixuan and Zhang, Danfeng},
title = {{CtChecker: A Precise, Sound and Efficient Static Analysis for Constant-Time Programming (Artifact)}},
pages = {26:1--26:5},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Zhou, Quan and Dang, Sixuan and Zhang, Danfeng},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.26},
URN = {urn:nbn:de:0030-drops-209244},
doi = {10.4230/DARTS.10.2.26},
annote = {Keywords: Information flow control, static analysis, side channel, constant-time programming}
}
Document
Artifact
Defining Name Accessibility Using Scope Graphs (Artifact)
Abstract
Many programming languages allow programmers to regulate accessibility; i.e., annotating a declaration with keywords such as export and private to indicate where it can be accessed. Despite the importance of name accessibility for, e.g., compilers, editor auto-completion and tooling, and automated refactorings, few existing type systems provide a formal account of name accessibility.
We present a declarative, executable, and language-parametric model for name accessibility, which provides a formal specification of name accessibility in Java, C#, C++, Rust, and Eiffel. We achieve this by defining name accessibility as a predicate on resolution paths through scope graphs. Since scope graphs are a language-independent model of name resolution, our model provides a uniform approach to defining different accessibility policies for different languages.
Our model is implemented in Statix, a logic language for executable type system specification using scope graphs. We evaluate its correctness on a test suite that compares it with the C#, Java, and Rust compilers, and show we can synthesize access modifiers in programs with holes accurately.
Cite as
Aron Zwaan and Casper Bach Poulsen. Defining Name Accessibility Using Scope Graphs (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 27:1-27:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
Copy BibTex To Clipboard
@Article{zwaan_et_al:DARTS.10.2.27,
author = {Zwaan, Aron and Bach Poulsen, Casper},
title = {{Defining Name Accessibility Using Scope Graphs (Artifact)}},
pages = {27:1--27:3},
journal = {Dagstuhl Artifacts Series},
ISBN = {978-3-95977-342-3},
ISSN = {2509-8195},
year = {2024},
volume = {10},
number = {2},
editor = {Zwaan, Aron and Bach Poulsen, Casper},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.27},
URN = {urn:nbn:de:0030-drops-209258},
doi = {10.4230/DARTS.10.2.27},
annote = {Keywords: access modifier, visibility, scope graph, name resolution}
}