Search Results

Documents authored by Jones, Timothy M.

Found 2 Possible Name Variants:

Jones, Timothy M.

Document
DOI: 10.4230/LIPIcs.TIME.2019.20
On Verifying Timed Hyperproperties

Authors: Hsi-Ming Ho, Ruoyu Zhou, and Timothy M. Jones

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

Abstract
We study the satisfiability and model-checking problems for timed hyperproperties specified with HyperMTL, a timed extension of HyperLTL. Depending on whether interleaving of events in different traces is allowed, two possible semantics can be defined for timed hyperproperties: synchronous and asynchronous. While the satisfiability problem can be decided similarly as for HyperLTL regardless of the choice of semantics, we show that the model-checking problem for HyperMTL, unless the specification is alternation-free, is undecidable even when very restricted timing constraints are allowed. On the positive side, we show that model checking HyperMTL with quantifier alternations is possible under certain conditions in the synchronous semantics, or when there is a fixed bound on the length of the time domain.
Cite as

Hsi-Ming Ho, Ruoyu Zhou, and Timothy M. Jones. On Verifying Timed Hyperproperties. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 20:1-20:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{ho_et_al:LIPIcs.TIME.2019.20,
  author =	{Ho, Hsi-Ming and Zhou, Ruoyu and Jones, Timothy M.},
  title =	{{On Verifying Timed Hyperproperties}},
  booktitle =	{26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
  pages =	{20:1--20:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-127-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{147},
  editor =	{Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.20},
  URN =		{urn:nbn:de:0030-drops-113782},
  doi =		{10.4230/LIPIcs.TIME.2019.20},
  annote =	{Keywords: Timed Automata, Temporal Logics, Cybersecurity}
}

Jones, Timothy

Document
DOI: 10.4230/LIPIcs.ECOOP.2016.13
Object Inheritance Without Classes

Authors: Timothy Jones, Michael Homer, James Noble, and Kim Bruce

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

Abstract
Which comes first: the object or the class? Language designers enjoy the conceptual simplicity of object-based languages (such as Emerald or Self) while many programmers prefer the pragmatic utility of classical inheritance (as in Simula and Java). Programmers in object-based languages have a tendency to build libraries to support traditional inheritance, and language implementations are often contorted to the same end. In this paper, we revisit the relationship between classes and objects. We model various kinds of inheritance in the context of an object-oriented language whose objects are not defined by classes, and explain why class inheritance and initialisation cannot be easily modelled purely by delegation.
Cite as

Timothy Jones, Michael Homer, James Noble, and Kim Bruce. Object Inheritance Without Classes. In 30th European Conference on Object-Oriented Programming (ECOOP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 56, pp. 13:1-13:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{jones_et_al:LIPIcs.ECOOP.2016.13,
  author =	{Jones, Timothy and Homer, Michael and Noble, James and Bruce, Kim},
  title =	{{Object Inheritance Without Classes}},
  booktitle =	{30th European Conference on Object-Oriented Programming (ECOOP 2016)},
  pages =	{13:1--13: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.13},
  URN =		{urn:nbn:de:0030-drops-61077},
  doi =		{10.4230/LIPIcs.ECOOP.2016.13},
  annote =	{Keywords: Inheritance, Objects, Classes, Operational semantics}
}
Document
DOI: 10.4230/DARTS.2.1.6
Object Inheritance Without Classes (Artifact)

Authors: Timothy Jones and Michael Homer

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

Abstract
This artifact is a PLT Redex implementation of the operational semantics presented in Object Inheritance Without Classes. It defines the core syntax and runtime semantics of the Graceless language, and then extends it in multiple different ways to produce the various implementations of object inheritance, including single and multiple inheritance. The implementation makes the semantics runnable, and precisely defines some behaviour which is defined informally in the paper.
Cite as

Timothy Jones and Michael Homer. Object Inheritance Without Classes (Artifact). In Special Issue of the 30th European Conference on Object-Oriented Programming (ECOOP 2016). Dagstuhl Artifacts Series (DARTS), Volume 2, Issue 1, pp. 6:1-6:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@Article{jones_et_al:DARTS.2.1.6,
  author =	{Jones, Timothy and Homer, Michael},
  title =	{{Object Inheritance Without Classes (Artifact)}},
  pages =	{6:1--6:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2016},
  volume =	{2},
  number =	{1},
  editor =	{Jones, Timothy and Homer, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.2.1.6},
  URN =		{urn:nbn:de:0030-drops-61278},
  doi =		{10.4230/DARTS.2.1.6},
  annote =	{Keywords: Inheritance, Objects, Classes, Operational semantics, PLT Redex}
}
Document
DOI: 10.4230/DARTS.1.1.4
Brand Objects for Nominal Typing (Artifact)

Authors: Timothy Jones, Michael Homer, and James Noble

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

Abstract
In Brand Objects for Nominal Typing, we describe an implementation of a branding system for both runtime and static types. This artifact provides the extended form of Hopper, an interpreter for the Grace programming language, and extra modules which define both the dynamic objects and the modular static type checker. The extra modules extend the existing structural type checker in the provided version of Hopper, and are capable of statically checking code which interacts with statically determinable declarations of brand objects, including singleton brand constructors, brand sums, and dynamic variables which are known to contain some brand value at runtime. The dynamic brand objects extend this behaviour to the runtime, enforcing non-static contracts and allowing runtime type testing.
Cite as

Timothy Jones, Michael Homer, and James Noble. Brand Objects for Nominal Typing (Artifact). In Special Issue of the 29th European Conference on Object-Oriented Programming (ECOOP 2015). Dagstuhl Artifacts Series (DARTS), Volume 1, Issue 1, pp. 4:1-4:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@Article{jones_et_al:DARTS.1.1.4,
  author =	{Jones, Timothy and Homer, Michael and Noble, James},
  title =	{{Brand Objects for Nominal Typing (Artifact)}},
  pages =	{4:1--4:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2015},
  volume =	{1},
  number =	{1},
  editor =	{Jones, Timothy and Homer, Michael and Noble, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.1.1.4},
  URN =		{urn:nbn:de:0030-drops-55134},
  doi =		{10.4230/DARTS.1.1.4},
  annote =	{Keywords: brands, types, structural, nominal, Grace}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2015.198
Brand Objects for Nominal Typing

Authors: Timothy Jones, Michael Homer, and James Noble

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

Abstract
Combinations of structural and nominal object typing in systems such as Scala, Whiteoak, and Unity have focused on extending existing nominal, class-based systems with structural subtyping. The typical rules of nominal typing do not lend themselves to such an extension, resulting in major modifications. Adding object branding to an existing structural system integrates nominal and structural typing without excessively complicating the type system. We have implemented brand objects to explicitly type objects, using existing features of the structurally typed language Grace, along with a static type checker which treats the brands as nominal types. We demonstrate that the brands are useful in an existing implementation of Grace, and provide a formal model of the extension to the language.
Cite as

Timothy Jones, Michael Homer, and James Noble. Brand Objects for Nominal Typing. In 29th European Conference on Object-Oriented Programming (ECOOP 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 37, pp. 198-221, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{jones_et_al:LIPIcs.ECOOP.2015.198,
  author =	{Jones, Timothy and Homer, Michael and Noble, James},
  title =	{{Brand Objects for Nominal Typing}},
  booktitle =	{29th European Conference on Object-Oriented Programming (ECOOP 2015)},
  pages =	{198--221},
  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.198},
  URN =		{urn:nbn:de:0030-drops-52314},
  doi =		{10.4230/LIPIcs.ECOOP.2015.198},
  annote =	{Keywords: brands, types, structural, nominal, Grace}
}
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