Search Results

Documents authored by Potanin, Alex


Document
Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems

Authors: Amos Robinson and Alex Potanin

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)


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. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 34:1-34:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{robinson_et_al:LIPIcs.ECOOP.2024.34,
  author =	{Robinson, Amos and Potanin, Alex},
  title =	{{Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{34:1--34:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.34},
  URN =		{urn:nbn:de:0030-drops-208836},
  doi =		{10.4230/LIPIcs.ECOOP.2024.34},
  annote =	{Keywords: Lustre, streaming, reactive, verification}
}
Document
Higher-Order Specifications for Deductive Synthesis of Programs with Pointers

Authors: David Young, Ziyi Yang, Ilya Sergey, and Alex Potanin

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)


Abstract
Synthetic Separation Logic (SSL) is a formalism that powers SuSLik, the state-of-the-art approach for the deductive synthesis of provably-correct programs in C-like languages that manipulate heap-based linked data structures. Despite its expressivity, SSL suffers from two shortcomings that hinder its utility. First, its main specification component, inductive predicates, only admits first-order definitions of data structure shapes, which leads to the proliferation of "boiler-plate" predicates for specifying common patterns. Second, SSL requires concrete definitions of data structures to synthesise programs that manipulate them, which results in the need to change a specification for a synthesis task every time changes are introduced into the layout of the involved structures. We propose to significantly lift the level of abstraction used in writing Separation Logic specifications for synthesis - both simplifying the approach and making the specifications more usable and easy to read and follow. We avoid the need to repetitively re-state low-level representation details throughout the specifications - allowing the reuse of different implementations of the same data structure by abstracting away the details of a specific layout used in memory. Our novel high-level front-end language called Pika significantly improves the expressiveness of SuSLik. We implemented a layout-agnostic synthesiser from Pika to SuSLik enabling push-button synthesis of C programs with in-place memory updates, along with the accompanying full proofs that they meet Separation Logic-style specifications, from high-level specifications that resemble ordinary functional programs. Our experiments show that our tool can produce C code that is comparable in its performance characteristics and is sometimes faster than Haskell.

Cite as

David Young, Ziyi Yang, Ilya Sergey, and Alex Potanin. Higher-Order Specifications for Deductive Synthesis of Programs with Pointers. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 45:1-45:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{young_et_al:LIPIcs.ECOOP.2024.45,
  author =	{Young, David and Yang, Ziyi and Sergey, Ilya and Potanin, Alex},
  title =	{{Higher-Order Specifications for Deductive Synthesis of Programs with Pointers}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{45:1--45:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.45},
  URN =		{urn:nbn:de:0030-drops-208946},
  doi =		{10.4230/LIPIcs.ECOOP.2024.45},
  annote =	{Keywords: Program Synthesis, Separation Logic, Functional Programming}
}
Document
Artifact
Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems (Artifact)

Authors: Amos Robinson and Alex Potanin

Published in: DARTS, Volume 10, Issue 2, Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)


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
Higher-Order Specifications for Deductive Synthesis of Programs with Pointers (Artifact)

Authors: David Young, Ziyi Yang, Ilya Sergey, and Alex Potanin

Published in: DARTS, Volume 10, Issue 2, Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)


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
A Capability-Based Module System for Authority Control (Artifact)

Authors: Darya Melicher, Yangqingwei Shi, Alex Potanin, and Jonathan Aldrich

Published in: DARTS, Volume 3, Issue 2, Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017)


Abstract
This artifact is intended to demonstrate the module system of the Wyvern programming language and consists of a Linux virtual machine with a snapshot of the Wyvern programming language's codebase. The Wyvern codebase contains a test suite that corresponds to the code examples in the paper accompanying the artifact. In addition, the artifact contains a document describing how to compile and run Wyvern programs.

Cite as

Darya Melicher, Yangqingwei Shi, Alex Potanin, and Jonathan Aldrich. A Capability-Based Module System for Authority Control (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@Article{melicher_et_al:DARTS.3.2.2,
  author =	{Melicher, Darya and Shi, Yangqingwei and Potanin, Alex and Aldrich, Jonathan},
  title =	{{A Capability-Based Module System for Authority Control (Artifact)}},
  pages =	{2:1--2:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2017},
  volume =	{3},
  number =	{2},
  editor =	{Melicher, Darya and Shi, Yangqingwei and Potanin, Alex and Aldrich, Jonathan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.2},
  URN =		{urn:nbn:de:0030-drops-72838},
  doi =		{10.4230/DARTS.3.2.2},
  annote =	{Keywords: language-based security, capabilities, authority, modules}
}
Document
Evil Pickles: DoS Attacks Based on Object-Graph Engineering (Artifact)

Authors: Jens Dietrich, Kamil Jezek, Shawn Rasheed, Amjed Tahir, and Alex Potanin

Published in: DARTS, Volume 3, Issue 2, Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017)


Abstract
This artefact demonstrates the effects of the serialisation vulnerabilities described in the companion paper. It is composed of three components: scripts, including source code, for Java, Ruby and C# serialisation-vulnerabilities, two case studies that demonstrate attacks based on the vulnerabilities, and a contracts-based mitigation strategy for serialisation-based attacks on Java applications. The artefact allows users to witness how the serialisation-based vulnerabilities result in behavior that can be used in security attacks. It also supports the repeatability of the case study experiments and the benchmark for the mitigation measures proposed in the paper. Instructions for running the tasks are provided along with a description of the artefact setup.

Cite as

Jens Dietrich, Kamil Jezek, Shawn Rasheed, Amjed Tahir, and Alex Potanin. Evil Pickles: DoS Attacks Based on Object-Graph Engineering (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 13:1-13:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@Article{dietrich_et_al:DARTS.3.2.13,
  author =	{Dietrich, Jens and Jezek, Kamil and Rasheed, Shawn and Tahir, Amjed and Potanin, Alex},
  title =	{{Evil Pickles: DoS Attacks Based on Object-Graph Engineering (Artifact)}},
  pages =	{13:1--13:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2017},
  volume =	{3},
  number =	{2},
  editor =	{Dietrich, Jens and Jezek, Kamil and Rasheed, Shawn and Tahir, Amjed 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.3.2.13},
  URN =		{urn:nbn:de:0030-drops-72944},
  doi =		{10.4230/DARTS.3.2.13},
  annote =	{Keywords: serialisation, denial of service, degradation of service, Java, C#, JavaScript, Ruby, vulnerabilities, library design, collection libraries}
}
Document
Evil Pickles: DoS Attacks Based on Object-Graph Engineering

Authors: Jens Dietrich, Kamil Jezek, Shawn Rasheed, Amjed Tahir, and Alex Potanin

Published in: LIPIcs, Volume 74, 31st European Conference on Object-Oriented Programming (ECOOP 2017)


Abstract
In recent years, multiple vulnerabilities exploiting the serialisation APIs of various programming languages, including Java, have been discovered. These vulnerabilities can be used to devise in- jection attacks, exploiting the presence of dynamic programming language features like reflection or dynamic proxies. In this paper, we investigate a new type of serialisation-related vulnerabilit- ies for Java that exploit the topology of object graphs constructed from classes of the standard library in a way that deserialisation leads to resource exhaustion, facilitating denial of service attacks. We analyse three such vulnerabilities that can be exploited to exhaust stack memory, heap memory and CPU time. We discuss the language and library design features that enable these vulnerabilities, and investigate whether these vulnerabilities can be ported to C#, Java- Script and Ruby. We present two case studies that demonstrate how the vulnerabilities can be used in attacks on two widely used servers, Jenkins deployed on Tomcat and JBoss. Finally, we propose a mitigation strategy based on contract injection.

Cite as

Jens Dietrich, Kamil Jezek, Shawn Rasheed, Amjed Tahir, and Alex Potanin. Evil Pickles: DoS Attacks Based on Object-Graph Engineering. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 10:1-10:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{dietrich_et_al:LIPIcs.ECOOP.2017.10,
  author =	{Dietrich, Jens and Jezek, Kamil and Rasheed, Shawn and Tahir, Amjed and Potanin, Alex},
  title =	{{Evil Pickles: DoS Attacks Based on Object-Graph Engineering}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{10:1--10:32},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{M\"{u}ller, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.10},
  URN =		{urn:nbn:de:0030-drops-72606},
  doi =		{10.4230/LIPIcs.ECOOP.2017.10},
  annote =	{Keywords: serialisation, denial of service, degradation of service, Java, C#, JavaScript, Ruby, vulnerabilities, library design, collection libraries}
}
Document
A Capability-Based Module System for Authority Control

Authors: Darya Melicher, Yangqingwei Shi, Alex Potanin, and Jonathan Aldrich

Published in: LIPIcs, Volume 74, 31st European Conference on Object-Oriented Programming (ECOOP 2017)


Abstract
The principle of least authority states that each component of the system should be given authority to access only the information and resources that it needs for its operation. This principle is fundamental to the secure design of software systems, as it helps to limit an application's attack surface and to isolate vulnerabilities and faults. Unfortunately, current programming languages do not provide adequate help in controlling the authority of application modules, an issue that is particularly acute in the case of untrusted third-party extensions. In this paper, we present a language design that facilitates controlling the authority granted to each application module. The key technical novelty of our approach is that modules are first-class, statically typed capabilities. First-class modules are essentially objects, and so we formalize our module system by translation into an object calculus and prove that the core calculus is type-safe and authority-safe. Unlike prior formalizations, our work defines authority non-transitively, allowing engineers to reason about software designs that use wrappers to provide an attenuated version of a more powerful capability. Our approach allows developers to determine a module's authority by examining the capabilities passed as module arguments when the module is created, or delegated to the module later during execution. The type system facilitates this by identifying which objects provide capabilities to sensitive resources, and by enabling security architects to examine the capabilities passed into and out of a module based only on the module's interface, without needing to examine the module's implementation code. An implementation of the module system and illustrative examples in the Wyvern programming language suggest that our approach can be a practical way to control module authority.

Cite as

Darya Melicher, Yangqingwei Shi, Alex Potanin, and Jonathan Aldrich. A Capability-Based Module System for Authority Control. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 20:1-20:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


Copy BibTex To Clipboard

@InProceedings{melicher_et_al:LIPIcs.ECOOP.2017.20,
  author =	{Melicher, Darya and Shi, Yangqingwei and Potanin, Alex and Aldrich, Jonathan},
  title =	{{A Capability-Based Module System for Authority Control}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{20:1--20:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{M\"{u}ller, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.20},
  URN =		{urn:nbn:de:0030-drops-72709},
  doi =		{10.4230/LIPIcs.ECOOP.2017.20},
  annote =	{Keywords: Language-based security, capabilities, authority, modules}
}
Document
A Theory of Tagged Objects (Artifact)

Authors: Joseph Lee, Jonathan Aldrich, Troy Shaw, Alex Potanin, and Benjamin Chung

Published in: DARTS, Volume 1, Issue 1, Special Issue of the 29th European Conference on Object-Oriented Programming (ECOOP 2015)


Abstract
A compiler and interpreter for Wyvern programming language written in Java and hosted on http://github.com/wyvernlang/wyvern and some sample programs (.wyv) including the main example from the paper in borderedwindow.wyv. We also include an extract of all the unit tests of which a large number may be designed to fail -- therefore they are best run using JUnit which can be done by checking out the source tree from the GitHub project link above.

Cite as

Joseph Lee, Jonathan Aldrich, Troy Shaw, Alex Potanin, and Benjamin Chung. A Theory of Tagged Objects (Artifact). In Special Issue of the 29th European Conference on Object-Oriented Programming (ECOOP 2015). Dagstuhl Artifacts Series (DARTS), Volume 1, Issue 1, pp. 3:1-3:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@Article{lee_et_al:DARTS.1.1.3,
  author =	{Lee, Joseph and Aldrich, Jonathan and Shaw, Troy and Potanin, Alex and Chung, Benjamin},
  title =	{{A Theory of Tagged Objects (Artifact)}},
  pages =	{3:1--3:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2015},
  volume =	{1},
  number =	{1},
  editor =	{Lee, Joseph and Aldrich, Jonathan and Shaw, Troy and Potanin, Alex and Chung, Benjamin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.1.1.3},
  URN =		{urn:nbn:de:0030-drops-55121},
  doi =		{10.4230/DARTS.1.1.3},
  annote =	{Keywords: objects, classes, tags, nominal and structural types}
}
Document
A Theory of Tagged Objects

Authors: Joseph Lee, Jonathan Aldrich, Troy Shaw, and Alex Potanin

Published in: LIPIcs, Volume 37, 29th European Conference on Object-Oriented Programming (ECOOP 2015)


Abstract
Foundational models of object-oriented constructs typically model objects as records with a structural type. However, many object-oriented languages are class-based; statically-typed formal models of these languages tend to sacrifice the foundational nature of the record-based models, and in addition cannot express dynamic class loading or creation. In this paper, we explore how to model statically-typed object-oriented languages that support dynamic class creation using foundational constructs of type theory. We start with an extensible tag construct motivated by type theory, and adapt it to support static reasoning about class hierarchy and the tags supported by each object. The result is a model that better explains the relationship between object-oriented and functional programming paradigms, suggests a useful enhancement to functional programming languages, and paves the way for more expressive statically typed object-oriented languages. In that vein, we describe the design and implementation of the Wyvern language, which leverages our theory.

Cite as

Joseph Lee, Jonathan Aldrich, Troy Shaw, and Alex Potanin. A Theory of Tagged Objects. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 174-197, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


Copy BibTex To Clipboard

@InProceedings{lee_et_al:LIPIcs.ECOOP.2015.174,
  author =	{Lee, Joseph and Aldrich, Jonathan and Shaw, Troy and Potanin, Alex},
  title =	{{A Theory of Tagged Objects}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{174--197},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-86-6},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{37},
  editor =	{Boyland, John Tang},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2015.174},
  URN =		{urn:nbn:de:0030-drops-52305},
  doi =		{10.4230/LIPIcs.ECOOP.2015.174},
  annote =	{Keywords: objects, classes, tags, nominal and structural types}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail