Issue
DARTS, Volume 4, Issue 3
Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018)
-
Part of:
Volume:
DARTS, Volume 4 (ECOOP 2018)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS)
Editors
Publication Details
- published at: 2018-07-05
- Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
- DBLP: db/journals/darts/darts4
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 - ECOOP 2018 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee
Abstract
Front Matter - ECOOP 2018 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee
Cite as
Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@Article{christakis_et_al:DARTS.4.3.0,
author = {Christakis, Maria and Haller, Philipp and Rapoport, Marianna and Rapoport, Marianna},
title = {{Front Matter - ECOOP 2018 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee}},
pages = {0:i--0:xii},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2018},
volume = {4},
number = {3},
editor = {Christakis, Maria and Haller, Philipp and Rapoport, Marianna and Rapoport, Marianna},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.4.3.0},
URN = {urn:nbn:de:0030-drops-92327},
doi = {10.4230/DARTS.4.3.0},
annote = {Keywords: Front Matter - ECOOP 2018 Artifacts, Table of Contents, Preface, Artifact Evaluation Committee}
}
Document
Dependent Types for Class-based Mutable Objects (Artifact)
Abstract
This artifact is based on DOL, a Dependent Object-oriented Language
featuring dependent types, mutable objects and class-based inheritance with
subtyping. The typechecker written in Xtend, a flexible and expressive
dialect of Java, is a direct implementation of the algorithmic type system
described in the companion paper. It uses a direct interface to Z3 theorem
prover via its API for Java. The artifact ships with an IDE developed as an
Eclipse plugin based on the Xtext framework.
Cite as
Joana Campos and Vasco T. Vasconcelos. Dependent Types for Class-based Mutable Objects (Artifact). In Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@Article{campos_et_al:DARTS.4.3.1,
author = {Campos, Joana and Vasconcelos, Vasco T.},
title = {{Dependent Types for Class-based Mutable Objects (Artifact)}},
pages = {1:1--1:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2018},
volume = {4},
number = {3},
editor = {Campos, Joana and Vasconcelos, Vasco T.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.4.3.1},
URN = {urn:nbn:de:0030-drops-92337},
doi = {10.4230/DARTS.4.3.1},
annote = {Keywords: dependent types, index refinements, mutable objects, type systems}
}
Document
Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates (Artifact)
Abstract
This artifact supports Legato, an at-most-once analysis. An
at-most-once analysis ensures that an application never observes
inconsistent versions of its environment by checking that every
value depends on at most one access of every external resource used
by the application. We have applied this general analysis to the
problem of finding errors in applications that support dynamic
configuration updates (DCU), i.e., configuration updates that are
applied immediately without program restart. When configurations may
change at any point during execution, the enforcing the at-most-once
condition for each configuration option guarantees that the program
never observes inconsistent versions of configuration options. This
artifact recreates our experiments, which applied Legato to 10
applications that support DCU and found several bugs across 9 of the
10 programs.
Cite as
John Toman and Dan Grossman. Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates (Artifact). In Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@Article{toman_et_al:DARTS.4.3.2,
author = {Toman, John and Grossman, Dan},
title = {{Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates (Artifact)}},
pages = {2:1--2:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2018},
volume = {4},
number = {3},
editor = {Toman, John and Grossman, Dan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.4.3.2},
URN = {urn:nbn:de:0030-drops-92342},
doi = {10.4230/DARTS.4.3.2},
annote = {Keywords: Static Analysis, Dynamic Configuration Updates}
}
Document
Static Typing of Complex Presence Constraints in Interfaces (Artifact)
Abstract
This artifact is based on TypeScriptIPC, a statically typed programming language with interfaces in which complex presence constraints can be defined.
This enables developers to express inter-property constraints on interface properties.
The need for these inter-property constraints stems from web APIs, which often impose a complex "dependency logic" between properties.
For example, some properties may be mutually exclusive, or the presence of a property may depend on the presence of others, etc.
TypeScriptIPC is a variant of TypeScript, in which interfaces are extended to express constraints over multiple properties, using propositional logic.
This artifact contains documentation on how to build and run TypeScriptIPC, such that the code snippets from the paper can be run.
Cite as
Nathalie Oostvogels, Joeri De Koster, and Wolfgang De Meuter. Static Typing of Complex Presence Constraints in Interfaces (Artifact). In Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@Article{oostvogels_et_al:DARTS.4.3.3,
author = {Oostvogels, Nathalie and De Koster, Joeri and De Meuter, Wolfgang},
title = {{Static Typing of Complex Presence Constraints in Interfaces (Artifact)}},
pages = {3:1--3:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2018},
volume = {4},
number = {3},
editor = {Oostvogels, Nathalie and De Koster, Joeri and De Meuter, Wolfgang},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.4.3.3},
URN = {urn:nbn:de:0030-drops-92422},
doi = {10.4230/DARTS.4.3.3},
annote = {Keywords: type system, interfaces, dependency logic}
}
Document
ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions (Artifact)
Abstract
This artifact provides the Scala, Haskell, and Purescript
implementations of ContextWorkflow, an embedded domain-specific
language for interruptible and compensable executions, and
demonstrates the maze search example described in the companion
paper. The Haskell and Purescript implementations provide the core
language constructs including \texttt{checkpoint} for partial aborts
and \texttt{sub} for sub-workflows and show that ContextWorkflow can
be embedded in eager and lazy languages as described in the
companion paper. The Scala implementation does not only provide
user-friendly syntax of ContextWorkflow but also gives the maze
search example as an interactive GUI application.
Cite as
Hiroaki Inoue, Tomoyuki Aotani, and Atsushi Igarashi. ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions (Artifact). In Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@Article{inoue_et_al:DARTS.4.3.4,
author = {Inoue, Hiroaki and Aotani, Tomoyuki and Igarashi, Atsushi},
title = {{ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions (Artifact)}},
pages = {4:1--4:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2018},
volume = {4},
number = {3},
editor = {Inoue, Hiroaki and Aotani, Tomoyuki and Igarashi, Atsushi},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.4.3.4},
URN = {urn:nbn:de:0030-drops-92356},
doi = {10.4230/DARTS.4.3.4},
annote = {Keywords: workflow, asynchronous exception, checkpoint, monad, embedded domain specific language}
}
Document
The Essence of Nested Composition (Artifact)
Abstract
The artifact contains the Coq formalization of \name, a simple calculus with
disjoint intersection types supporting nested subtyping and composition, as described in the companion paper.
Cite as
Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. The Essence of Nested Composition (Artifact). In Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 5:1-5:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@Article{bi_et_al:DARTS.4.3.5,
author = {Bi, Xuan and Oliveira, Bruno C. d. S. and Schrijvers, Tom},
title = {{The Essence of Nested Composition (Artifact)}},
pages = {5:1--5:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2018},
volume = {4},
number = {3},
editor = {Bi, Xuan and Oliveira, Bruno C. d. S. and Schrijvers, Tom},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.4.3.5},
URN = {urn:nbn:de:0030-drops-92363},
doi = {10.4230/DARTS.4.3.5},
annote = {Keywords: nested composition, family polymorphism, intersection types, coherence}
}
Document
CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs (Artifact)
Abstract
In this artefact, we present CrySL, an extensible approach to validating the
correct usage of cryptographic APIs. The artefact contains executables
for CogniCrypt_{SAST}, the analysis CrySL-based analysis, along with the CrySL rules we used in in the original paper's experiments. We also provide scripts to re-run the experiments. We finally include a tutorial to showcase the CogniCrypt_{SAST} on a small Java target program.
Cite as
Stefan Krüger, Johannes Späth, Karim Ali, Eric Bodden, and Mira Mezini. CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs (Artifact). In Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 6:1-6:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@Article{kruger_et_al:DARTS.4.3.6,
author = {Kr\"{u}ger, Stefan and Sp\"{a}th, Johannes and Ali, Karim and Bodden, Eric and Mezini, Mira},
title = {{CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs (Artifact)}},
pages = {6:1--6:4},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2018},
volume = {4},
number = {3},
editor = {Kr\"{u}ger, Stefan and Sp\"{a}th, Johannes and Ali, Karim and Bodden, Eric 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.4.3.6},
URN = {urn:nbn:de:0030-drops-92371},
doi = {10.4230/DARTS.4.3.6},
annote = {Keywords: cryptography, domain-specific language, static analysis}
}
Document
Definite Reference Mutability (Artifact)
Abstract
Related paper "Definite Reference Mutability" presents
ReM (Re[ference] M[utability]), a type system
that separates mutable references into (1) definitely mutable,
and (2) maybe mutable, i.e., references whose mutability is due to inherent
approximation. We have implemented ReM and applied it on a large benchmark
suite. Results show that ~ 86\% of mutable references
are definitely mutable.
This article describes the tool artifact from the related paper. The purpose of
the article and artifact is to allow researchers to reproduce our results, as well as build new type systems upon our code.
Cite as
Ana Milanova and Wei Huang. Definite Reference Mutability (Artifact). In Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 7:1-7:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@Article{milanova_et_al:DARTS.4.3.7,
author = {Milanova, Ana and Huang, Wei},
title = {{Definite Reference Mutability (Artifact)}},
pages = {7:1--7:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2018},
volume = {4},
number = {3},
editor = {Milanova, Ana and Huang, Wei},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.4.3.7},
URN = {urn:nbn:de:0030-drops-92382},
doi = {10.4230/DARTS.4.3.7},
annote = {Keywords: reference immutability, type inference, CFL-reachability}
}
Document
Type Regression Testing to Detect Breaking Changes in Node.js Libraries (Artifact)
Abstract
This artifact provides an implementation of a novel technique, type regression testing, to automatically determine whether an update of a npm library implementation affects the types of its public interface, according to how the library is being used by other npm packages. Type regression testing is implemented in the tool NoRegrets. A run of NoRegrets is parameterized with a pre-update and post-update version of the library, and it consists of three fully automatic phases. First, NoRegrets fetches a list of clients that depend upon the pre-update library, and that have a test suite that succeeds on the pre-update version. Second, NoRegrets uses an ECMAScript 6 proxy instrumentation to generate the API model of both the pre-update and post-update libraries, based on observations of how the client test suites interact with the library. Third, the two models are compared, and inconsistencies are reported as type regressions.
This artifact contains the source code and an installation of NoRegrets, with a guide for how to use the tool and reproduce the experimental results presented in the paper.
Cite as
Gianluca Mezzetti, Anders Møller, and Martin Toldam Torp. Type Regression Testing to Detect Breaking Changes in Node.js Libraries (Artifact). In Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 8:1-8:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@Article{mezzetti_et_al:DARTS.4.3.8,
author = {Mezzetti, Gianluca and M{\o}ller, Anders and Torp, Martin Toldam},
title = {{Type Regression Testing to Detect Breaking Changes in Node.js Libraries (Artifact)}},
pages = {8:1--8:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2018},
volume = {4},
number = {3},
editor = {Mezzetti, Gianluca and M{\o}ller, Anders and Torp, Martin Toldam},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.4.3.8},
URN = {urn:nbn:de:0030-drops-92394},
doi = {10.4230/DARTS.4.3.8},
annote = {Keywords: JavaScript, semantic versioning, dynamic analysis}
}
Document
Typed First-Class Traits (Artifact)
Abstract
This artifact contains the prototype Haskell implementation of SEDEL, with
support for first-class traits, as described in the companion paper. This artifact
also contains the source code of the case study on "Anatomy of Programming
Languages", illustrating how effective SEDEL is in terms of modularizing
programming language features. For comparison, it also includes a vanilla Haskell implementation of the case study without any code reuse.
Cite as
Xuan Bi and Bruno C. d. S. Oliveira. Typed First-Class Traits (Artifact). In Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 9:1-9:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@Article{bi_et_al:DARTS.4.3.9,
author = {Bi, Xuan and Oliveira, Bruno C. d. S.},
title = {{Typed First-Class Traits (Artifact)}},
pages = {9:1--9:2},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2018},
volume = {4},
number = {3},
editor = {Bi, Xuan and Oliveira, Bruno C. d. S.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.4.3.9},
URN = {urn:nbn:de:0030-drops-92407},
doi = {10.4230/DARTS.4.3.9},
annote = {Keywords: traits, extensible designs}
}
Document
KafKa: Gradual Typing for Objects (Artifact)
Abstract
A wide range of gradual type systems have been proposed, providing many
languages with the ability to mix typed and untyped code. However, hiding
under language details, these gradual type systems have fundamentally
different ideas of what it means to be typed. In this paper, we show that
four of the most common gradual type systems provide distinct guarantees,
and we give a formal framework for comparing gradual type systems for
object-oriented languages. First, we show that the different gradual type
systems are practically distinguishable via a three-part litmus test. Then,
we present a formal framework for defining and comparing gradual type
systems. Within this framework, different gradual type systems become
translations between a common source and target language, allowing for
direct comparison of semantics and guarantees.
Cite as
Benjamin Chung, Paley Li, Francesco Zappa Nardelli, and Jan Vitek. KafKa: Gradual Typing for Objects (Artifact). In Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 10:1-10:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
Copy BibTex To Clipboard
@Article{chung_et_al:DARTS.4.3.10,
author = {Chung, Benjamin and Li, Paley and Nardelli, Francesco Zappa and Vitek, Jan},
title = {{KafKa: Gradual Typing for Objects (Artifact)}},
pages = {10:1--10:3},
journal = {Dagstuhl Artifacts Series},
ISSN = {2509-8195},
year = {2018},
volume = {4},
number = {3},
editor = {Chung, Benjamin and Li, Paley and Nardelli, Francesco Zappa and Vitek, Jan},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.4.3.10},
URN = {urn:nbn:de:0030-drops-92411},
doi = {10.4230/DARTS.4.3.10},
annote = {Keywords: Gradual typing, object-orientation, language design, type systems}
}