3 Search Results for "Campos, Joana"

Document
DOI: 10.4230/LIPIcs.CONCUR.2025.23
First-Order Store and Visibility in Name-Passing Calculi

Authors: Daniel Hirschkoff, Iwan Quémerais, and Davide Sangiorgi

Published in: LIPIcs, Volume 348, 36th International Conference on Concurrency Theory (CONCUR 2025)

Abstract
The π-calculus is the paradigmatical name-passing calculus. While being purely name-passing, it allows the representation of higher-order functions and store. We study how π-calculus processes can be controlled so that computations can only involve storage of first-order values. The discipline is enforced by a type system that is based on the notion of visibility, coming from game semantics. We discuss the impact of visibility on the behavioural theory. We propose characterisations of may-testing and barbed equivalence, based on (variants of) trace equivalence and labelled bisimilarity, in the case where computation is sequential, and in the case where computation is well-bracketed.
Cite as

Daniel Hirschkoff, Iwan Quémerais, and Davide Sangiorgi. First-Order Store and Visibility in Name-Passing Calculi. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 23:1-23:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{hirschkoff_et_al:LIPIcs.CONCUR.2025.23,
  author =	{Hirschkoff, Daniel and Qu\'{e}merais, Iwan and Sangiorgi, Davide},
  title =	{{First-Order Store and Visibility in Name-Passing Calculi}},
  booktitle =	{36th International Conference on Concurrency Theory (CONCUR 2025)},
  pages =	{23:1--23:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-389-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{348},
  editor =	{Bouyer, Patricia and van de Pol, Jaco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.23},
  URN =		{urn:nbn:de:0030-drops-239737},
  doi =		{10.4230/LIPIcs.CONCUR.2025.23},
  annote =	{Keywords: process calculi, behavioural equivalence, type system}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2018.13
Dependent Types for Class-based Mutable Objects

Authors: Joana Campos and Vasco T. Vasconcelos

Published in: LIPIcs, Volume 109, 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

Abstract
We present an imperative object-oriented language featuring a dependent type system designed to support class-based programming and inheritance. Programmers implement classes in the usual imperative style, and may take advantage of a richer dependent type system to express class invariants and restrictions on how objects are allowed to change and be used as arguments to methods. By way of example, we implement insertion and deletion for binary search trees in an imperative style, and come up with types that ensure the binary search tree invariant. This is the first dependently-typed language with mutable objects that we know of to bring classes and index refinements into play, enabling types (classes) to be refined by indices drawn from some constraint domain. We give a declarative type system that supports objects whose types may change, despite being sound. We also give an algorithmic type system that provides a precise account of quantifier instantiation in a bidirectional style, and from which it is straightforward to read off an implementation. Moreover, all the examples in the paper have been run, compiled and executed in a fully functional prototype that includes a plugin for the Eclipse IDE.
Cite as

Joana Campos and Vasco T. Vasconcelos. Dependent Types for Class-based Mutable Objects. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 13:1-13:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{campos_et_al:LIPIcs.ECOOP.2018.13,
  author =	{Campos, Joana and Vasconcelos, Vasco T.},
  title =	{{Dependent Types for Class-based Mutable Objects}},
  booktitle =	{32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
  pages =	{13:1--13:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-079-8},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{109},
  editor =	{Millstein, Todd},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2018.13},
  URN =		{urn:nbn:de:0030-drops-92182},
  doi =		{10.4230/LIPIcs.ECOOP.2018.13},
  annote =	{Keywords: dependent types, index refinements, mutable objects, type systems}
}
Document
DOI: 10.4230/DARTS.4.3.1
Dependent Types for Class-based Mutable Objects (Artifact)

Authors: Joana Campos and Vasco T. Vasconcelos

Published in: DARTS, Volume 4, Issue 3, Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018)

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}
}
  • Refine by Type
  • 3 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 2 2018

  • Refine by Author
  • 2 Campos, Joana
  • 2 Vasconcelos, Vasco T.
  • 1 Hirschkoff, Daniel
  • 1 Quémerais, Iwan
  • 1 Sangiorgi, Davide

  • Refine by Series/Journal
  • 2 LIPIcs
  • 1 DARTS

  • Refine by Classification
  • 1 Software and its engineering → Semantics
  • 1 Theory of computation → Process calculi

  • Refine by Keyword
  • 2 dependent types
  • 2 index refinements
  • 2 mutable objects
  • 2 type systems
  • 1 behavioural equivalence
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact