Search Results

Documents authored by Thiemann, Peter

Document
DOI: 10.4230/LIPIcs.ECOOP.2024.3
A Dynamic Logic for Symbolic Execution for the Smart Contract Programming Language Michelson

Authors: Barnabas Arvay, Thi Thu Ha Doan, and Peter Thiemann

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

Abstract
Verification of smart contracts is an important topic in the context of blockchain technology. We study an approach to verification that is based on symbolic execution. As a formal basis for symbolic execution, we design a dynamic logic for Michelson, the smart contract language of the Tezos blockchain, and prove its soundness in the proof assistant Agda. Towards the soundness proof we formalize the concrete semantics as well as its symbolic counterpart in a unified setting. The logic encompasses single contract runs as well as inter-contract runs chained in a single transaction.
Cite as

Barnabas Arvay, Thi Thu Ha Doan, and Peter Thiemann. A Dynamic Logic for Symbolic Execution for the Smart Contract Programming Language Michelson. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 3:1-3:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{arvay_et_al:LIPIcs.ECOOP.2024.3,
  author =	{Arvay, Barnabas and Doan, Thi Thu Ha and Thiemann, Peter},
  title =	{{A Dynamic Logic for Symbolic Execution for the Smart Contract Programming Language Michelson}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{3:1--3: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.3},
  URN =		{urn:nbn:de:0030-drops-208529},
  doi =		{10.4230/LIPIcs.ECOOP.2024.3},
  annote =	{Keywords: Smart Contract, Blockchain, Formal Verification, Symbolic Execution}
}
Document
DOI: 10.4230/DagRep.14.1.108
Next Generation Protocols for Heterogeneous Systems (Dagstuhl Seminar 24051)

Authors: Stephanie Balzer, Marco Carbone, Roland Kuhn, and Peter Thiemann

Published in: Dagstuhl Reports, Volume 14, Issue 1 (2024)

Abstract
The emergence of new computing systems, like cloud computing, blockchains, and Internet of Things (IoT), replaces the traditional monolithic software hardware stack with a distributed heterogeneous model. This change poses new demands on the programming languages for developing such systems: compositionality, allowing decomposition of a system into smaller, possibly heterogeneous, parts and composition of the individually verified parts into a verified whole, security, asserting end-to-end integrity and confidentiality, quantitative reasoning methods, accounting for timing and probabilistic events, and, as a cross-cutting concern, certification of asserted properties in terms of independently verifiable, machine-checked proofs. Characteristics of this emerging computation model are distribution of the participating entities and message passing as the primary means of communication. Message passing is also the communication model underlying behavioral types and programming languages, making them uniquely fitted for this new application domain. Behavioral types explicitly capture the protocols of message exchange and have a strong theoretical foundation. Recent applications of behavioral types include smart contract languages, information flow control, and machine-checked proofs of safety properties. Although these early explorations are promising, the current state of the art of behavioral types and programming languages lacks a comprehensive account of the above-mentioned demands. This Dagstuhl Seminar aims to gather experts from academia and industry to discuss the use of programming languages tailored to tackle the challenges posed by today’s emerging distributed and heterogeneous computing platforms, e.g., by making use of behavioral types. It will focus on static and possibly dynamic mechanisms to support compositionality, security, quantitative reasoning, and certification.
Cite as

Stephanie Balzer, Marco Carbone, Roland Kuhn, and Peter Thiemann. Next Generation Protocols for Heterogeneous Systems (Dagstuhl Seminar 24051). In Dagstuhl Reports, Volume 14, Issue 1, pp. 108-129, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{balzer_et_al:DagRep.14.1.108,
  author =	{Balzer, Stephanie and Carbone, Marco and Kuhn, Roland and Thiemann, Peter},
  title =	{{Next Generation Protocols for Heterogeneous Systems (Dagstuhl Seminar 24051)}},
  pages =	{108--129},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{14},
  number =	{1},
  editor =	{Balzer, Stephanie and Carbone, Marco and Kuhn, Roland and Thiemann, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.1.108},
  URN =		{urn:nbn:de:0030-drops-204930},
  doi =		{10.4230/DagRep.14.1.108},
  annote =	{Keywords: behavioural types, concurrency, programming languages, session types}
}
Document
Artifact
DOI: 10.4230/DARTS.8.2.18
Global Type Inference for Featherweight Generic Java - Prototype Implementation (Artifact)

Authors: Andreas Stadelmeier, Martin Plümicke, and Peter Thiemann

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
We implemented a prototype of the type inference algorithm described in the paper "Global Type Inference for Featherweight Generic Java". Our type inference algorithm for Featherweight Generic Java (GFJ) is able to calculate the missing types in a Typeless Featherweight Generic Java (FGJ-GT) program. Inserting those types generates a valid GFJ program. We demonstrate this with a prototype implementation. The prototype is a web application which accepts GFJ-GT programs as input and shows the respective GFJ program after the type inference.
Cite as

Andreas Stadelmeier, Martin Plümicke, and Peter Thiemann. Global Type Inference for Featherweight Generic Java - Prototype Implementation (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 18:1-18:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{stadelmeier_et_al:DARTS.8.2.18,
  author =	{Stadelmeier, Andreas and Pl\"{u}micke, Martin and Thiemann, Peter},
  title =	{{Global Type Inference for Featherweight Generic Java - Prototype Implementation (Artifact)}},
  pages =	{18:1--18:4},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Stadelmeier, Andreas and Pl\"{u}micke, Martin and Thiemann, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.2.18},
  URN =		{urn:nbn:de:0030-drops-162165},
  doi =		{10.4230/DARTS.8.2.18},
  annote =	{Keywords: type inference, Java, subtyping, generics}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.28
Global Type Inference for Featherweight Generic Java

Authors: Andreas Stadelmeier, Martin Plümicke, and Peter Thiemann

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
Java’s type system mostly relies on type checking augmented with local type inference to improve programmer convenience. We study global type inference for Featherweight Generic Java (FGJ), a functional Java core language. Given generic class headers and field specifications, our inference algorithm infers all method types if classes do not make use of polymorphic recursion. The algorithm is constraint-based and improves on prior work in several respects. Despite the restricted setting, global type inference for FGJ is NP-complete.
Cite as

Andreas Stadelmeier, Martin Plümicke, and Peter Thiemann. Global Type Inference for Featherweight Generic Java. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 28:1-28:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{stadelmeier_et_al:LIPIcs.ECOOP.2022.28,
  author =	{Stadelmeier, Andreas and Pl\"{u}micke, Martin and Thiemann, Peter},
  title =	{{Global Type Inference for Featherweight Generic Java}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{28:1--28:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.28},
  URN =		{urn:nbn:de:0030-drops-162560},
  doi =		{10.4230/LIPIcs.ECOOP.2022.28},
  annote =	{Keywords: type inference, Java, subtyping, generics}
}
Document
Short Paper
DOI: 10.4230/OASIcs.FMBC.2021.5
Towards Contract Modules for the Tezos Blockchain (Short Paper)

Authors: Thi Thu Ha Doan and Peter Thiemann

Published in: OASIcs, Volume 95, 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)

Abstract
Programmatic interaction with a blockchain is often clumsy. Many interfaces handle only loosely structured data, often in JSON format, that is inconvenient to handle and offers few guarantees. Contract modules provide a statically checked interface to interact with contracts on the Tezos blockchain. A module specification provides all types as well as information about potential failure conditions of the contract. The specification is checked against the contract implementation using symbolic execution. An OCaml module is generated that contains a function for each entry point of the contract. The types of these functions fully describe the interface including the failure conditions and guarantee type-safe and sometimes fail-safe invocation of the contract on the blockchain.
Cite as

Thi Thu Ha Doan and Peter Thiemann. Towards Contract Modules for the Tezos Blockchain (Short Paper). In 3rd International Workshop on Formal Methods for Blockchains (FMBC 2021). Open Access Series in Informatics (OASIcs), Volume 95, pp. 5:1-5:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{doan_et_al:OASIcs.FMBC.2021.5,
  author =	{Doan, Thi Thu Ha and Thiemann, Peter},
  title =	{{Towards Contract Modules for the Tezos Blockchain}},
  booktitle =	{3rd International Workshop on Formal Methods for Blockchains (FMBC 2021)},
  pages =	{5:1--5:9},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-209-9},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{95},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2021.5},
  URN =		{urn:nbn:de:0030-drops-154294},
  doi =		{10.4230/OASIcs.FMBC.2021.5},
  annote =	{Keywords: contract API, modules, static checking}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2016.9
LJGS: Gradual Security Types for Object-Oriented Languages

Authors: Luminous Fennell and Peter Thiemann

Published in: LIPIcs, Volume 56, 30th European Conference on Object-Oriented Programming (ECOOP 2016)

Abstract
LJGS is a lightweight Java core calculus with a gradual security type system. The calculus guarantees secure information flow for sequential, class-based, typed object-oriented programming with mutable objects and virtual method calls. An LJGS program is composed of fragments that are checked either statically or dynamically. Statically checked fragments adhere to a security type system so that they incur no run-time penalty whereas dynamically checked fragments rely on run-time security labels. The programmer marks the boundaries between static and dynamic checking with casts so that it is always clear whether a program fragment requires run-time checks. LJGS requires security annotations on fields and methods. A field annotation either specifies a fixed static security level or it prescribes dynamic checking. A method annotation specifies a constrained polymorphic security signature. The types of local variables in method bodies are analyzed flow-sensitively and require no annotation. The dynamic checking of fields relies on a static points-to analysis to approximate implicit flows. We prove type soundness and non-interference for LJGS.
Cite as

Luminous Fennell and Peter Thiemann. LJGS: Gradual Security Types for Object-Oriented Languages. In 30th European Conference on Object-Oriented Programming (ECOOP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 56, pp. 9:1-9:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{fennell_et_al:LIPIcs.ECOOP.2016.9,
  author =	{Fennell, Luminous and Thiemann, Peter},
  title =	{{LJGS: Gradual Security Types for Object-Oriented Languages}},
  booktitle =	{30th European Conference on Object-Oriented Programming (ECOOP 2016)},
  pages =	{9:1--9:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-014-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{56},
  editor =	{Krishnamurthi, Shriram and Lerner, Benjamin S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2016.9},
  URN =		{urn:nbn:de:0030-drops-61031},
  doi =		{10.4230/LIPIcs.ECOOP.2016.9},
  annote =	{Keywords: gradual typing, security typing, Java, hybrid information flow control}
}
Document
DOI: 10.4230/DARTS.2.1.4
LJGS: Gradual Security Types for Object-Oriented Languages (Artifact)

Authors: Luminous Fennell and Peter Thiemann

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

Abstract
JGS-check is the accompanying artifact to "LJGS: Gradual Security Types for Object-Oriented Languages". LJGS is a Java-like language with gradual security typing. It features a constraint based information flow type system that includes a type dynamic and type casts. Dynamically typed fragments are liberally accepted by the type checker and rely on run-time enforcement for security. JGS-check is a type checker for the subset of Java that corresponds to the calculus presented in the paper and that implements the constraint generation and satisfiability checks of LJGS' type system. It's purpose is to illustrate and substantiate the behavior of our gradual security type system. It takes a directory of Java source code as input and reports methods that violate the typing rules. JGS-check is merely a type checker and does not implement code generation. The submission archive includes the compiled type checker, the code of the example section (Section 2) as well additional examples and testcases that did not fit into the paper. The user should also be able to check custom code as long as it corresponds the subset of Java that is covered by LJGS.
Cite as

Luminous Fennell and Peter Thiemann. LJGS: Gradual Security Types for Object-Oriented Languages (Artifact). In Special Issue of the 30th European Conference on Object-Oriented Programming (ECOOP 2016). Dagstuhl Artifacts Series (DARTS), Volume 2, Issue 1, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{fennell_et_al:DARTS.2.1.4,
  author =	{Fennell, Luminous and Thiemann, Peter},
  title =	{{LJGS: Gradual Security Types for Object-Oriented Languages (Artifact)}},
  pages =	{4:1--4:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2016},
  volume =	{2},
  number =	{1},
  editor =	{Fennell, Luminous and Thiemann, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.2.1.4},
  URN =		{urn:nbn:de:0030-drops-61253},
  doi =		{10.4230/DARTS.2.1.4},
  annote =	{Keywords: gradual typing, security typing, Java, hybrid information flow control}
}
Document
DOI: 10.4230/DARTS.1.1.1
TreatJS: Higher-Order Contracts for JavaScript (Artifact)

Authors: Matthias Keil and Peter Thiemann

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

Abstract
TreatJS is a language embedded, higher-order contract system for JavaScript which enforces contracts by run-time monitoring. Beyond providing the standard abstractions for building higher-order contracts (base, function, and object contracts), TreatJS's novel contributions are its guarantee of non-interfering contract execution, its systematic approach to blame assignment, its support for contracts in the style of union and intersection types, and its notion of a parameterized contract scope, which is the building block for composable run-time generated contracts that generalize dependent function contracts. TreatJS} is implemented as a library so that all aspects of a contract can be specified using the full JavaScript language. The library relies on JavaScript proxies to guarantee full interposition for contracts. It further exploits JavaScript's reflective features to run contracts in a sandbox environment, which guarantees that the execution of contract code does not modify the application state. No source code transformation or change in the JavaScript run-time system is required.
Cite as

Matthias Keil and Peter Thiemann. TreatJS: Higher-Order Contracts for JavaScript (Artifact). In Special Issue of the 29th European Conference on Object-Oriented Programming (ECOOP 2015). Dagstuhl Artifacts Series (DARTS), Volume 1, Issue 1, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{keil_et_al:DARTS.1.1.1,
  author =	{Keil, Matthias and Thiemann, Peter},
  title =	{{TreatJS: Higher-Order Contracts for JavaScript (Artifact)}},
  pages =	{1:1--1:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2015},
  volume =	{1},
  number =	{1},
  editor =	{Keil, Matthias and Thiemann, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.1.1.1},
  URN =		{urn:nbn:de:0030-drops-55105},
  doi =		{10.4230/DARTS.1.1.1},
  annote =	{Keywords: Higher-Order Contracts, JavaScript, Proxies}
}
Document
DOI: 10.4230/DARTS.1.1.2
Transparent Object Proxies for JavaScript (Artifact)

Authors: Matthias Keil, Sankha Narayan Guria, Andreas Schlegel, Manuel Geffken, and Peter Thiemann

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

Abstract
This artifact provides two prototype extensions of the SpiderMonkey JavaScript engine. Both extensions implement alternative designs for transparent proxies that are better suited for use cases such as certain contract wrappers and access restricting membranes. The first prototype extends the proxy handler by an isTransparent trap that regulates the proxy's transparency. The second prototype implements a new global object TransparentProxy that implements the constructor for transparent proxy objects.
Cite as

Matthias Keil, Sankha Narayan Guria, Andreas Schlegel, Manuel Geffken, and Peter Thiemann. Transparent Object Proxies for JavaScript (Artifact). In Special Issue of the 29th European Conference on Object-Oriented Programming (ECOOP 2015). Dagstuhl Artifacts Series (DARTS), Volume 1, Issue 1, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{keil_et_al:DARTS.1.1.2,
  author =	{Keil, Matthias and Guria, Sankha Narayan and Schlegel, Andreas and Geffken, Manuel and Thiemann, Peter},
  title =	{{Transparent Object Proxies for JavaScript (Artifact)}},
  pages =	{2:1--2:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2015},
  volume =	{1},
  number =	{1},
  editor =	{Keil, Matthias and Guria, Sankha Narayan and Schlegel, Andreas and Geffken, Manuel and Thiemann, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.1.1.2},
  URN =		{urn:nbn:de:0030-drops-55114},
  doi =		{10.4230/DARTS.1.1.2},
  annote =	{Keywords: JavaScript, Proxies, Equality, Contracts}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2015.28
TreatJS: Higher-Order Contracts for JavaScripts

Authors: Matthias Keil and Peter Thiemann

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

Abstract
TreatJS is a language embedded, higher-order contract system for JavaScript which enforces contracts by run-time monitoring. Beyond providing the standard abstractions for building higher-order contracts (base, function, and object contracts), TreatJS's novel contributions are its guarantee of non-interfering contract execution, its systematic approach to blame assignment, its support for contracts in the style of union and intersection types, and its notion of a parameterized contract scope, which is the building block for composable run-time generated contracts that generalize dependent function contracts. TreatJS is implemented as a library so that all aspects of a contract can be specified using the full JavaScript language. The library relies on JavaScript proxies to guarantee full interposition for contracts. It further exploits JavaScript's reflective features to run contracts in a sandbox environment, which guarantees that the execution of contract code does not modify the application state. No source code transformation or change in the JavaScript run-time system is required. The impact of contracts on execution speed is evaluated using the Google Octane benchmark.
Cite as

Matthias Keil and Peter Thiemann. TreatJS: Higher-Order Contracts for JavaScripts. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 28-51, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{keil_et_al:LIPIcs.ECOOP.2015.28,
  author =	{Keil, Matthias and Thiemann, Peter},
  title =	{{TreatJS: Higher-Order Contracts for JavaScripts}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{28--51},
  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.28},
  URN =		{urn:nbn:de:0030-drops-52164},
  doi =		{10.4230/LIPIcs.ECOOP.2015.28},
  annote =	{Keywords: Higher-Order Contracts, JavaScript, Proxies}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2015.149
Transparent Object Proxies in JavaScript

Authors: Matthias Keil, Sankha Narayan Guria, Andreas Schlegel, Manuel Geffken, and Peter Thiemann

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

Abstract
Proxies are the swiss army knives of object adaptation. They introduce a level of indirection to intercept select operations on a target object and divert them as method calls to a handler. Proxies have many uses like implementing access control, enforcing contracts, virtualizing resources. One important question in the design of a proxy API is whether a proxy object should inherit the identity of its target. Apparently proxies should have their own identity for security-related applications whereas other applications, in particular contract systems, require transparent proxies that compare equal to their target objects. We examine the issue with transparency in various use cases for proxies, discuss different approaches to obtain transparency, and propose two designs that require modest modifications in the JavaScript engine and cannot be bypassed by the programmer. We implement our designs in the SpiderMonkey JavaScript interpreter and bytecode compiler. Our evaluation shows that these modifications of have no statistically significant impact on the benchmark performance of the JavaScript engine. Furthermore, we demonstrate that contract systems based on wrappers require transparent proxies to avoid interference with program execution in realistic settings.
Cite as

Matthias Keil, Sankha Narayan Guria, Andreas Schlegel, Manuel Geffken, and Peter Thiemann. Transparent Object Proxies in JavaScript. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 149-173, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{keil_et_al:LIPIcs.ECOOP.2015.149,
  author =	{Keil, Matthias and Guria, Sankha Narayan and Schlegel, Andreas and Geffken, Manuel and Thiemann, Peter},
  title =	{{Transparent Object Proxies in JavaScript}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{149--173},
  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.149},
  URN =		{urn:nbn:de:0030-drops-52299},
  doi =		{10.4230/LIPIcs.ECOOP.2015.149},
  annote =	{Keywords: JavaScript, Proxies, Equality, Contracts}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.175
Symbolic Solving of Extended Regular Expression Inequalities

Authors: Matthias Keil and Peter Thiemann

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
This paper presents a new algorithm for the containment problem for extended regular expressions that contain intersection and complement operators and that range over infinite alphabets. The algorithm solves extended regular expressions inequalities symbolically by term rewriting and thus avoids the translation to an expression-equivalent automaton. Our algorithm is based on Brzozowski's regular expression derivatives and on Antimirov's term-rewriting approach to check containment. To deal with large or infinite alphabets effectively, we generalize Brzozowski's derivative operator to work with respect to (potentially infinite) representable character sets.
Cite as

Matthias Keil and Peter Thiemann. Symbolic Solving of Extended Regular Expression Inequalities. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 175-186, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{keil_et_al:LIPIcs.FSTTCS.2014.175,
  author =	{Keil, Matthias and Thiemann, Peter},
  title =	{{Symbolic Solving of Extended Regular Expression Inequalities}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{175--186},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.175},
  URN =		{urn:nbn:de:0030-drops-48411},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.175},
  annote =	{Keywords: Extended regular expression, containment, infinite alphabet, infinite character set, effective boolean algebra}
}
Document
DOI: 10.4230/DagRep.4.6.84
Scripting Languages and Frameworks: Analysis and Verification (Dagstuhl Seminar 14271)

Authors: Fritz Henglein, Ranjit Jhala, Shriram Krishnamurthi, and Peter Thiemann

Published in: Dagstuhl Reports, Volume 4, Issue 6 (2015)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 14271 "Scripting Languages and Frameworks: Analysis and Verification". The seminar brought together a broad spectrum of researchers working on the semantics, analysis and verification of scripting languages. In addition to talks describing the latest problems and research on the key issues, split roughly into four overarching themes: semantics, types, analysis, contracts, languages, and security, the seminar had breakout sessions devoted to crosscutting topics that were of broad interest across the community, including, how to create shared analysis infrastructure, how to think about the semantics of contracts and blame, and the role of soundness in analyzing real world languages, as well as several "tutorial" sessions explaining various new tools and techniques.
Cite as

Fritz Henglein, Ranjit Jhala, Shriram Krishnamurthi, and Peter Thiemann. Scripting Languages and Frameworks: Analysis and Verification (Dagstuhl Seminar 14271). In Dagstuhl Reports, Volume 4, Issue 6, pp. 84-107, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{henglein_et_al:DagRep.4.6.84,
  author =	{Henglein, Fritz and Jhala, Ranjit and Krishnamurthi, Shriram and Thiemann, Peter},
  title =	{{Scripting Languages and Frameworks: Analysis and Verification (Dagstuhl Seminar 14271)}},
  pages =	{84--107},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{4},
  number =	{6},
  editor =	{Henglein, Fritz and Jhala, Ranjit and Krishnamurthi, Shriram and Thiemann, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.4.6.84},
  URN =		{urn:nbn:de:0030-drops-47816},
  doi =		{10.4230/DagRep.4.6.84},
  annote =	{Keywords: Scripting Languages, Frameworks, Contracts, Types, Analysis, Semantics}
}
Document
DOI: 10.4230/DagSemProc.07051.1
07051 Abstracts Collection – Programming Paradigms for the Web: Web Programming and Web Services

Authors: Richard Hull, Peter Thiemann, and Philip Wadler

Published in: Dagstuhl Seminar Proceedings, Volume 7051, Programming Paradigms for the Web: Web Programming and Web Services (2007)

Abstract
From 28.01. to 02.02.2007, the Dagstuhl Seminar 07051 ``Programming Paradigms for the Web: Web Programming and Web Services'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

Richard Hull, Peter Thiemann, and Philip Wadler. 07051 Abstracts Collection – Programming Paradigms for the Web: Web Programming and Web Services. In Programming Paradigms for the Web: Web Programming and Web Services. Dagstuhl Seminar Proceedings, Volume 7051, pp. 1-7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{hull_et_al:DagSemProc.07051.1,
  author =	{Hull, Richard and Thiemann, Peter and Wadler, Philip},
  title =	{{07051 Abstracts Collection – Programming Paradigms for the Web: Web Programming and Web Services}},
  booktitle =	{Programming Paradigms for the Web: Web Programming and Web Services},
  pages =	{1--7},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7051},
  editor =	{Richard Hull and Peter Thiemann and Philip Wadler},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07051.1},
  URN =		{urn:nbn:de:0030-drops-11287},
  doi =		{10.4230/DagSemProc.07051.1},
  annote =	{Keywords: Web programming, programming concepts, program analysis, type systems, scripting languages, XML processing and querying}
}
Document
DOI: 10.4230/DagSemProc.07051.2
07051 Executive Summary – Programming Paradigms for the Web: Web Programming and Web Services

Authors: Richard Hull, Peter Thiemann, and Philip Wadler

Published in: Dagstuhl Seminar Proceedings, Volume 7051, Programming Paradigms for the Web: Web Programming and Web Services (2007)

Abstract
The world-wide web raises a variety of new programming challenges. To name a few: programming at the level of the web browser, data-centric approaches, and attempts to automatically discover and compose web services. This seminar brought together researchers from the web programming and web services communities and strove to engage them in communication with each other. The seminar was held in an unusual style, in a mixture of short presentations and in-depth discussion sessions in small groups. This style enabled the participants to identify and discuss burning questions in small birds-of-a-feather sessions as well as in large plenary sessions. It required active participation of all attendees.
Cite as

Richard Hull, Peter Thiemann, and Philip Wadler. 07051 Executive Summary – Programming Paradigms for the Web: Web Programming and Web Services. In Programming Paradigms for the Web: Web Programming and Web Services. Dagstuhl Seminar Proceedings, Volume 7051, pp. 1-4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{hull_et_al:DagSemProc.07051.2,
  author =	{Hull, Richard and Thiemann, Peter and Wadler, Philip},
  title =	{{07051 Executive Summary – Programming Paradigms for the Web: Web Programming and Web Services}},
  booktitle =	{Programming Paradigms for the Web: Web Programming and Web Services},
  pages =	{1--4},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7051},
  editor =	{Richard Hull and Peter Thiemann and Philip Wadler},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07051.2},
  URN =		{urn:nbn:de:0030-drops-11259},
  doi =		{10.4230/DagSemProc.07051.2},
  annote =	{Keywords: Web programming, web services, programming paradigms, analysis and verification, implementation techniques and optimizations}
}
Document
DOI: 10.4230/DagSemProc.07051.3
07051 Working Group Outcomes – Programming Paradigms for the Web: Web Programming and Web Services

Authors: Richard Hull, Peter Thiemann, and Philip Wadler

Published in: Dagstuhl Seminar Proceedings, Volume 7051, Programming Paradigms for the Web: Web Programming and Web Services (2007)

Abstract
Participants in the seminar broke into groups on ``Patterns and Paradigms'' for web programming, ``Web Services,'' ``Data on the Web,'' ``Software Engineering'' and ``Security.'' Here we give the raw notes recorded during these sessions.
Cite as

Richard Hull, Peter Thiemann, and Philip Wadler. 07051 Working Group Outcomes – Programming Paradigms for the Web: Web Programming and Web Services. In Programming Paradigms for the Web: Web Programming and Web Services. Dagstuhl Seminar Proceedings, Volume 7051, pp. 1-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)

Copy BibTex To Clipboard

@InProceedings{hull_et_al:DagSemProc.07051.3,
  author =	{Hull, Richard and Thiemann, Peter and Wadler, Philip},
  title =	{{07051 Working Group Outcomes – Programming Paradigms for the Web: Web Programming and Web Services}},
  booktitle =	{Programming Paradigms for the Web: Web Programming and Web Services},
  pages =	{1--17},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7051},
  editor =	{Richard Hull and Peter Thiemann and Philip Wadler},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07051.3},
  URN =		{urn:nbn:de:0030-drops-11273},
  doi =		{10.4230/DagSemProc.07051.3},
  annote =	{Keywords: Web programming, web services, programming paradigms, analysis and verification, implementation techniques and optimizations}
}
Document
DOI: 10.4230/DagSemRep.317
Dependent Type Theory meets Practical Programming (Dagstuhl Seminar 01341)

Authors: Gilles Barthe, Peter Dybjer, and Peter Thiemann

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Gilles Barthe, Peter Dybjer, and Peter Thiemann. Dependent Type Theory meets Practical Programming (Dagstuhl Seminar 01341). Dagstuhl Seminar Report 317, pp. 1-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2002)

Copy BibTex To Clipboard

@TechReport{barthe_et_al:DagSemRep.317,
  author =	{Barthe, Gilles and Dybjer, Peter and Thiemann, Peter},
  title =	{{Dependent Type Theory meets Practical Programming (Dagstuhl Seminar 01341)}},
  pages =	{1--13},
  ISSN =	{1619-0203},
  year =	{2002},
  type = 	{Dagstuhl Seminar Report},
  number =	{317},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.317},
  URN =		{urn:nbn:de:0030-drops-152017},
  doi =		{10.4230/DagSemRep.317},
}
Document
DOI: 10.4230/DagSemRep.134
Partial Evaluation (Dagstuhl Seminar 9607)

Authors: Olivier Danvy, Robert Glück, and Peter Thiemann

Published in: Dagstuhl Seminar Reports. Dagstuhl Seminar Reports, Volume 1 (2021)

Abstract
Cite as

Olivier Danvy, Robert Glück, and Peter Thiemann. Partial Evaluation (Dagstuhl Seminar 9607). Dagstuhl Seminar Report 134, pp. 1-35, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (1996)

Copy BibTex To Clipboard

@TechReport{danvy_et_al:DagSemRep.134,
  author =	{Danvy, Olivier and Gl\"{u}ck, Robert and Thiemann, Peter},
  title =	{{Partial Evaluation (Dagstuhl Seminar 9607)}},
  pages =	{1--35},
  ISSN =	{1619-0203},
  year =	{1996},
  type = 	{Dagstuhl Seminar Report},
  number =	{134},
  institution =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemRep.134},
  URN =		{urn:nbn:de:0030-drops-150218},
  doi =		{10.4230/DagSemRep.134},
}
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact