5 Search Results for "Vasconcelos, Vasco T."

Document
DOI: 10.4230/LIPIcs.CONCUR.2023.11
Subtyping Context-Free Session Types

Authors: Gil Silva, Andreia Mordido, and Vasco T. Vasconcelos

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

Abstract
Context-free session types describe structured patterns of communication on heterogeneously typed channels, allowing the specification of protocols unconstrained by tail recursion. The enhanced expressive power provided by non-regular recursion comes, however, at the cost of the decidability of subtyping, even if equivalence is still decidable. We present an approach to subtyping context-free session types based on a novel kind of observational preorder we call XYZW-simulation, which generalizes XY-simulation (also known as covariant-contravariant simulation) and therefore also bisimulation and plain simulation. We further propose a subtyping algorithm that we prove to be sound, and present an empirical evaluation in the context of a compiler for a programming language. Due to the general nature of the simulation relation upon which it is built, this algorithm may also find applications in other domains.
Cite as

Gil Silva, Andreia Mordido, and Vasco T. Vasconcelos. Subtyping Context-Free Session Types. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 11:1-11:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{silva_et_al:LIPIcs.CONCUR.2023.11,
  author =	{Silva, Gil and Mordido, Andreia and Vasconcelos, Vasco T.},
  title =	{{Subtyping Context-Free Session Types}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{11:1--11:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.11},
  URN =		{urn:nbn:de:0030-drops-190055},
  doi =		{10.4230/LIPIcs.CONCUR.2023.11},
  annote =	{Keywords: Session types, Subtyping, Simulation, Simple grammars, Non-regular recursion}
}
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}
}
Document
DOI: 10.4230/DagRep.7.1.158
Theory and Applications of Behavioural Types (Dagstuhl Seminar 17051)

Authors: Simon Gay, Vasco T. Vasconcelos, Philip Wadler, and Nobuko Yoshida

Published in: Dagstuhl Reports, Volume 7, Issue 1 (2017)

Abstract
This report documents the programme and the outcomes of Dagstuhl Seminar 17051 "Theory and Applications of Behavioural Types". Behavioural types describe the dynamic aspects of programs, in contrast to data types, which describe the fixed structure of data. Perhaps the most well-known form of behavioural types is session types, which are type-theoretic specifications of communication protocols. More generally, behavioural types include typestate systems, which specify state-dependent availability of operations; choreographies, which specify collective communication behaviour; and behavioural contracts. In recent years, research activity in behavioural types has increased dramatically, in both theoretical and practical directions. Theoretical work has explored new relationships between established behavioural type systems and areas such as linear logic, automata theory, process calculus testing theory, dependent type theory, and model-checking. On the practical side, there are several implementations of programming languages, programming language extensions, software development tools, and runtime monitoring systems, which are becoming mature enough to apply to real-world case studies. The seminar brought together researchers from the established, largely European, research community in behavioural types, and other participants from outside Europe and from related research topics such as effect systems and actor-based languages. The questions that we intended to explore included: - How can we understand the relationships between the foundations of session types in terms of linear logic, automata, denotational models, and other type theories? - How can the scope and applicability of behavioural types be increased by incorporating ideas and approaches from gradual typing and dependent type theory? - What is the relationship, in terms of expressivity and tractability, between behavioural types and other verification techniques such as model-checking? - What are the theoretical and practical obstacles to delivering behavioural types to software developers in a range of mainstream programming languages? - What are the advantages and disadvantages of incorporating behavioural types into standard programming languages or designing new languages directly based on the foundations of session types? - How can we evaluate the effectiveness of behavioural types in programming languages and software development?
Cite as

Simon Gay, Vasco T. Vasconcelos, Philip Wadler, and Nobuko Yoshida. Theory and Applications of Behavioural Types (Dagstuhl Seminar 17051). In Dagstuhl Reports, Volume 7, Issue 1, pp. 158-189, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{gay_et_al:DagRep.7.1.158,
  author =	{Gay, Simon and Vasconcelos, Vasco T. and Wadler, Philip and Yoshida, Nobuko},
  title =	{{Theory and Applications of Behavioural Types (Dagstuhl Seminar 17051)}},
  pages =	{158--189},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2017},
  volume =	{7},
  number =	{1},
  editor =	{Gay, Simon and Vasconcelos, Vasco T. and Wadler, Philip and Yoshida, Nobuko},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.7.1.158},
  URN =		{urn:nbn:de:0030-drops-72497},
  doi =		{10.4230/DagRep.7.1.158},
  annote =	{Keywords: Behavioural Types, Programming Languages, Runtime Verification, Type Systems}
}
Document
DOI: 10.4230/DagSemProc.05081.6
MiKO---Mikado Koncurrent Objects

Authors: Francisco Martins, Liliana Salvador, Vasco T. Vasconcelos, and Luís Lopes

Published in: Dagstuhl Seminar Proceedings, Volume 5081, Foundations of Global Computing (2006)

Abstract
The motivation for the Mikado migration model is to provide programming constructs for controlling code mobility that are as independent as possible from the particular programming language used to program the code. The main idea is to regard a domain (or site, or locality), where mobile code may enter or exit, as a membrane enclosing running processes, and offering services that have to be called for entering or exiting the domain. MiKO---Mikado Koncurrent Objects is a particular instance of this model, where the membrane is explicitly split in two parts: the methods defining the interface, and a process part describing the data for, and the behavior of, the interface. The talk presents the syntax, operational semantics, and type system of MiKO, together with an example. It concludes by briefly mentioning the implementation of a language based on the calculus.
Cite as

Francisco Martins, Liliana Salvador, Vasco T. Vasconcelos, and Luís Lopes. MiKO---Mikado Koncurrent Objects. In Foundations of Global Computing. Dagstuhl Seminar Proceedings, Volume 5081, pp. 1-43, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{martins_et_al:DagSemProc.05081.6,
  author =	{Martins, Francisco and Salvador, Liliana and Vasconcelos, Vasco T. and Lopes, Lu{\'\i}s},
  title =	{{MiKO---Mikado Koncurrent Objects}},
  booktitle =	{Foundations of Global Computing},
  pages =	{1--43},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{5081},
  editor =	{Jos\'{e} Luiz Fiadeiro and Ugo Montanari and Martin Wirsing},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.05081.6},
  URN =		{urn:nbn:de:0030-drops-3014},
  doi =		{10.4230/DagSemProc.05081.6},
  annote =	{Keywords: Global computing, code migration, administrative domains, process calculus}
}
  • Refine by Author
  • 5 Vasconcelos, Vasco T.
  • 2 Campos, Joana
  • 1 Gay, Simon
  • 1 Lopes, Luís
  • 1 Martins, Francisco
  • Show More...

  • Refine by Classification
  • 1 Software and its engineering → Concurrent programming structures
  • 1 Software and its engineering → Semantics
  • 1 Theory of computation → Concurrency
  • 1 Theory of computation → Type structures

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

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 2 2018
  • 1 2006
  • 1 2017
  • 1 2023

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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact