24 Search Results for "Oliveira, Bruno C. d. S."

Document
DOI: 10.4230/LIPIcs.ECOOP.2023.34
Dependent Merges and First-Class Environments

Authors: Jinhao Tan and Bruno C. d. S. Oliveira

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

Abstract
In most programming languages a (runtime) environment stores all the definitions that are available to programmers. Typically, environments are a meta-level notion, used only conceptually or internally in the implementation of programming languages. Only a few programming languages allow environments to be first-class values, which can be manipulated directly in programs. Although there is some research on calculi with first-class environments for statically typed programming languages, these calculi typically have significant restrictions. In this paper we propose a statically typed calculus, called 𝖤_i, with first-class environments. The main novelty of the 𝖤_i calculus is its support for first-class environments, together with an expressive set of operators that manipulate them. Such operators include: reification of the current environment, environment concatenation, environment restriction, and reflection mechanisms for running computations under a given environment. In 𝖤_i any type can act as a context (i.e. an environment type) and contexts are simply types. Furthermore, because 𝖤_i supports subtyping, there is a natural notion of context subtyping. There are two important ideas in 𝖤_i that generalize and are inspired by existing notions in the literature. The 𝖤_i calculus borrows disjoint intersection types and a merge operator, used in 𝖤_i to model contexts and environments, from the λ_i calculus. However, unlike the merges in λ_i, the merges in 𝖤_i can depend on previous components of a merge. From implicit calculi, the 𝖤_i calculus borrows the notion of a query, which allows type-based lookups on environments. In particular, queries are key to the ability of 𝖤_i to reify the current environment, or some parts of it. We prove the determinism and type soundness of 𝖤_i, and show that 𝖤_i can encode all well-typed λ_i programs.
Cite as

Jinhao Tan and Bruno C. d. S. Oliveira. Dependent Merges and First-Class Environments. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 34:1-34:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{tan_et_al:LIPIcs.ECOOP.2023.34,
  author =	{Tan, Jinhao and Oliveira, Bruno C. d. S.},
  title =	{{Dependent Merges and First-Class Environments}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{34:1--34:32},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.34},
  URN =		{urn:nbn:de:0030-drops-182277},
  doi =		{10.4230/LIPIcs.ECOOP.2023.34},
  annote =	{Keywords: First-class Environments, Disjointness, Intersection Types}
}
Document
Artifact
DOI: 10.4230/DARTS.9.2.2
Dependent Merges and First-Class Environments (Artifact)

Authors: Jinhao Tan and Bruno C. d. S. Oliveira

Published in: DARTS, Volume 9, Issue 2, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
This artifact contains the mechanical formalization of the calculi associated with the paper Dependent Merges and First-Class Environments. All of the metatheory has been formalized in Coq theorem prover. The paper studies a statically typed calculus, called 𝖤_i, with first-class environments. The main novelty of the 𝖤_i calculus is its support for first-class environments, together with an expressive set of operators that manipulate them.
Cite as

Jinhao Tan and Bruno C. d. S. Oliveira. Dependent Merges and First-Class Environments (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{tan_et_al:DARTS.9.2.2,
  author =	{Tan, Jinhao and Oliveira, Bruno C. d. S.},
  title =	{{Dependent Merges and First-Class Environments (Artifact)}},
  pages =	{2:1--2:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{2},
  editor =	{Tan, Jinhao and Oliveira, Bruno C. d. S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.9.2.2},
  URN =		{urn:nbn:de:0030-drops-182427},
  doi =		{10.4230/DARTS.9.2.2},
  annote =	{Keywords: First-class Environments, Disjointness, Intersection Types}
}
Document
DOI: 10.4230/LIPIcs.CCC.2023.29
Constant-Depth Circuits vs. Monotone Circuits

Authors: Bruno P. Cavalar and Igor C. Oliveira

Published in: LIPIcs, Volume 264, 38th Computational Complexity Conference (CCC 2023)

Abstract
We establish new separations between the power of monotone and general (non-monotone) Boolean circuits: - For every k ≥ 1, there is a monotone function in AC⁰ (constant-depth poly-size circuits) that requires monotone circuits of depth Ω(log^k n). This significantly extends a classical result of Okol'nishnikova [Okol'nishnikova, 1982] and Ajtai and Gurevich [Ajtai and Gurevich, 1987]. In addition, our separation holds for a monotone graph property, which was unknown even in the context of AC⁰ versus mAC⁰. - For every k ≥ 1, there is a monotone function in AC⁰[⊕] (constant-depth poly-size circuits extended with parity gates) that requires monotone circuits of size exp(Ω(log^k n)). This makes progress towards a question posed by Grigni and Sipser [Grigni and Sipser, 1992]. These results show that constant-depth circuits can be more efficient than monotone formulas and monotone circuits when computing monotone functions. In the opposite direction, we observe that non-trivial simulations are possible in the absence of parity gates: every monotone function computed by an AC⁰ circuit of size s and depth d can be computed by a monotone circuit of size 2^{n - n/O(log s)^{d-1}}. We show that the existence of significantly faster monotone simulations would lead to breakthrough circuit lower bounds. In particular, if every monotone function in AC⁰ admits a polynomial size monotone circuit, then NC² is not contained in NC¹. Finally, we revisit our separation result against monotone circuit size and investigate the limits of our approach, which is based on a monotone lower bound for constraint satisfaction problems (CSPs) established by Göös, Kamath, Robere and Sokolov [Göös et al., 2019] via lifting techniques. Adapting results of Schaefer [Thomas J. Schaefer, 1978] and Allender, Bauland, Immerman, Schnoor and Vollmer [Eric Allender et al., 2009], we obtain an unconditional classification of the monotone circuit complexity of Boolean-valued CSPs via their polymorphisms. This result and the consequences we derive from it might be of independent interest.
Cite as

Bruno P. Cavalar and Igor C. Oliveira. Constant-Depth Circuits vs. Monotone Circuits. In 38th Computational Complexity Conference (CCC 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 264, pp. 29:1-29:37, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{cavalar_et_al:LIPIcs.CCC.2023.29,
  author =	{Cavalar, Bruno P. and Oliveira, Igor C.},
  title =	{{Constant-Depth Circuits vs. Monotone Circuits}},
  booktitle =	{38th Computational Complexity Conference (CCC 2023)},
  pages =	{29:1--29:37},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-282-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{264},
  editor =	{Ta-Shma, Amnon},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2023.29},
  URN =		{urn:nbn:de:0030-drops-182998},
  doi =		{10.4230/LIPIcs.CCC.2023.29},
  annote =	{Keywords: circuit complexity, monotone circuit complexity, bounded-depth circuis, constraint-satisfaction problems}
}
Document
Artifact
DOI: 10.4230/DARTS.8.2.4
Direct Foundations for Compositional Programming (Artifact)

Authors: Andong Fan, Xuejing Huang, Han Xu, Yaozhu Sun, and Bruno C. d. S. Oliveira

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

Abstract
Our companion paper proposes a new formulation of the 𝖥_{i}^{+} calculus with disjoint polymorphism and a merge operator based on Type-Directed Operational Semantics. The artifact contains Coq formalization of the 𝖥_{i}^{+} calculus and our new implementation of the CP language, which demonstrates the new 𝖥_{i}^{+} can serve as the direct foundation for Compositional Programming.
Cite as

Andong Fan, Xuejing Huang, Han Xu, Yaozhu Sun, and Bruno C. d. S. Oliveira. Direct Foundations for Compositional Programming (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 4:1-4:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{fan_et_al:DARTS.8.2.4,
  author =	{Fan, Andong and Huang, Xuejing and Xu, Han and Sun, Yaozhu and Oliveira, Bruno C. d. S.},
  title =	{{Direct Foundations for Compositional Programming (Artifact)}},
  pages =	{4:1--4:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Fan, Andong and Huang, Xuejing and Xu, Han and Sun, Yaozhu and Oliveira, Bruno C. d. S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.4},
  URN =		{urn:nbn:de:0030-drops-162020},
  doi =		{10.4230/DARTS.8.2.4},
  annote =	{Keywords: Intersection types, disjoint polymorphism, operational semantics}
}
Document
Artifact
DOI: 10.4230/DARTS.8.2.5
Elementary Type Inference (Artifact)

Authors: Jinxu Zhao and Bruno C. d. S. Oliveira

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

Abstract
This artifact contains the Appendix of the paper, proofs of theorems declared in the paper, and a sample implementation of the type inference algorithm. The proof contains 3 main results: soundness, completness and decidability of the type-inference algorithm. Moreover, there are several proofs about the declarative system and also a soundness/completeness proof between stable subtyping and a syntax-directed specification.
Cite as

Jinxu Zhao and Bruno C. d. S. Oliveira. Elementary Type Inference (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 5:1-5:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{zhao_et_al:DARTS.8.2.5,
  author =	{Zhao, Jinxu and Oliveira, Bruno C. d. S.},
  title =	{{Elementary Type Inference (Artifact)}},
  pages =	{5:1--5:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Zhao, Jinxu and Oliveira, Bruno C. d. S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.5},
  URN =		{urn:nbn:de:0030-drops-162036},
  doi =		{10.4230/DARTS.8.2.5},
  annote =	{Keywords: Type Inference}
}
Document
Artifact
DOI: 10.4230/DARTS.8.2.17
Union Types with Disjoint Switches (Artifact)

Authors: Baber Rehman, Xuejing Huang, Ningning Xie, and Bruno C. d. S. Oliveira

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

Abstract
This artifact contains the mechanical formalization of the calculi associated with the paper Union Types with Disjoint Switches. All of the metatheory has been formalized in Coq theorem prover. We provide a docker image as well the code archive. The paper studies a union calculus ({λ_{u}}). Primary idea of {λ_{u}} calculus is a type based disjoint switch construct for the elimination of union types. We also study several extensions of the {λ_{u}} calculus including intersection types, distributive subtyping, nominal types, parametric polymorphism and an extension for the empty types.
Cite as

Baber Rehman, Xuejing Huang, Ningning Xie, and Bruno C. d. S. Oliveira. Union Types with Disjoint Switches (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 17:1-17:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{rehman_et_al:DARTS.8.2.17,
  author =	{Rehman, Baber and Huang, Xuejing and Xie, Ningning and Oliveira, Bruno C. d. S.},
  title =	{{Union Types with Disjoint Switches (Artifact)}},
  pages =	{17:1--17:6},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Rehman, Baber and Huang, Xuejing and Xie, Ningning and Oliveira, Bruno C. d. S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.8.2.17},
  URN =		{urn:nbn:de:0030-drops-162150},
  doi =		{10.4230/DARTS.8.2.17},
  annote =	{Keywords: Union types, switch expression, disjointness, intersection types}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.2
Elementary Type Inference

Authors: Jinxu Zhao and Bruno C. d. S. Oliveira

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

Abstract
Languages with polymorphic type systems are made convenient to use by employing type inference to avoid redundant type information. Unfortunately, features such as impredicative types and subtyping make complete type inference very challenging or impossible to realize. This paper presents a form of partial type inference called elementary type inference. Elementary type inference adopts the idea of inferring only monotypes from past work on predicative higher-ranked polymorphism. This idea is extended with the addition of explicit type applications that work for any polytypes. Thus easy (predicative) instantiations can be inferred, while all other (impredicative) instantiations are always possible with explicit type applications without any compromise in expressiveness. Our target is a System F extension with top and bottom types, similar to the language employed by Pierce and Turner in their seminal work on local type inference. We show a sound, complete and decidable type system for a calculus called F_{< :}^e, that targets that extension of System F. A key design choice in F_{< :}^e is to consider top and bottom types as polytypes only. An important technical challenge is that the combination of predicative implicit instantiation and impredicative explicit type applications, in the presence of standard subtyping rules, is non-trivial. Without some restrictions, key properties, such as subsumption and stability of type substitution lemmas, break. To address this problem we introduce a variant of polymorphic subtyping called stable subtyping with some mild restrictions on implicit instantiation. All the results are mechanically formalized in the Abella theorem prover.
Cite as

Jinxu Zhao and Bruno C. d. S. Oliveira. Elementary Type Inference. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 2:1-2:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{zhao_et_al:LIPIcs.ECOOP.2022.2,
  author =	{Zhao, Jinxu and Oliveira, Bruno C. d. S.},
  title =	{{Elementary Type Inference}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{2:1--2:28},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.2},
  URN =		{urn:nbn:de:0030-drops-162303},
  doi =		{10.4230/LIPIcs.ECOOP.2022.2},
  annote =	{Keywords: Type Inference}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.18
Direct Foundations for Compositional Programming

Authors: Andong Fan, Xuejing Huang, Han Xu, Yaozhu Sun, and Bruno C. d. S. Oliveira

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

Abstract
The recently proposed CP language adopts Compositional Programming: a new modular programming style that solves challenging problems such as the Expression Problem. CP is implemented on top of a polymorphic core language with disjoint intersection types called 𝖥_{i}^{+}. The semantics of 𝖥_{i}^{+} employs an elaboration to a target language and relies on a sophisticated proof technique to prove the coherence of the elaboration. Unfortunately, the proof technique is technically challenging and hard to scale to many common features, including recursion or impredicative polymorphism. Thus, the original formulation of 𝖥_{i}^{+} does not support the two later features, which creates a gap between theory and practice, since CP fundamentally relies on them. This paper presents a new formulation of 𝖥_{i}^{+} based on a type-directed operational semantics (TDOS). The TDOS approach was recently proposed to model the semantics of languages with disjoint intersection types (but without polymorphism). Our work shows that the TDOS approach can be extended to languages with disjoint polymorphism and model the full 𝖥_{i}^{+} calculus. Unlike the elaboration semantics, which gives the semantics to 𝖥_{i}^{+} indirectly via a target language, the TDOS approach gives a semantics to 𝖥_{i}^{+} directly. With a TDOS, there is no need for a coherence proof. Instead, we can simply prove that the semantics is deterministic. The proof of determinism only uses simple reasoning techniques, such as straightforward induction, and is able to handle problematic features such as recursion and impredicative polymorphism. This removes the gap between theory and practice and validates the original proofs of correctness for CP. We formalized the TDOS variant of the 𝖥_{i}^{+} calculus and all its proofs in the Coq proof assistant.
Cite as

Andong Fan, Xuejing Huang, Han Xu, Yaozhu Sun, and Bruno C. d. S. Oliveira. Direct Foundations for Compositional Programming. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 18:1-18:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{fan_et_al:LIPIcs.ECOOP.2022.18,
  author =	{Fan, Andong and Huang, Xuejing and Xu, Han and Sun, Yaozhu and Oliveira, Bruno C. d. S.},
  title =	{{Direct Foundations for Compositional Programming}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{18:1--18:28},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.18},
  URN =		{urn:nbn:de:0030-drops-162463},
  doi =		{10.4230/LIPIcs.ECOOP.2022.18},
  annote =	{Keywords: Intersection types, disjoint polymorphism, operational semantics}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.25
Union Types with Disjoint Switches

Authors: Baber Rehman, Xuejing Huang, Ningning Xie, and Bruno C. d. S. Oliveira

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

Abstract
Union types are nowadays a common feature in many modern programming languages. This paper investigates a formulation of union types with an elimination construct that enables case analysis (or switches) on types. The interesting aspect of this construct is that each clause must operate on disjoint types. By using disjoint switches, it is possible to ensure exhaustiveness (i.e. all possible cases are handled), and that none of the cases overlap. In turn, this means that the order of the cases does not matter and that reordering the cases has no impact on the semantics, helping with program understanding and refactoring. While implemented in the Ceylon language, disjoint switches have not been formally studied in the research literature, although a related notion of disjointness has been studied in the context of disjoint intersection types. We study union types with disjoint switches formally and in a language independent way. We first present a simplified calculus, called the union calculus (λ_u), which includes disjoint switches and prove several results, including type soundness and determinism. The notion of disjointness in λ_u is in essence the dual notion of disjointness for intersection types. We then present a more feature-rich formulation of λ_u, which includes intersection types, distributive subtyping and a simple form of nominal types. This extension reveals new challenges. Those challenges require us to depart from the dual notion of disjointness for intersection types, and use a more general formulation of disjointness instead. Among other applications, we show that disjoint switches provide an alternative to certain forms of overloading, and that they enable a simple approach to nullable (or optional) types. All the results about λ_u and its extensions have been formalized in the Coq theorem prover.
Cite as

Baber Rehman, Xuejing Huang, Ningning Xie, and Bruno C. d. S. Oliveira. Union Types with Disjoint Switches. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 25:1-25:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{rehman_et_al:LIPIcs.ECOOP.2022.25,
  author =	{Rehman, Baber and Huang, Xuejing and Xie, Ningning and Oliveira, Bruno C. d. S.},
  title =	{{Union Types with Disjoint Switches}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{25:1--25:31},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.25},
  URN =		{urn:nbn:de:0030-drops-162531},
  doi =		{10.4230/LIPIcs.ECOOP.2022.25},
  annote =	{Keywords: Union types, switch expression, disjointness, intersection types}
}
Document
Artifact
DOI: 10.4230/DARTS.7.2.9
Type-Directed Operational Semantics for Gradual Typing (Artifact)

Authors: Wenjia Ye, Bruno C. d. S. Oliveira, and Xuejing Huang

Published in: DARTS, Volume 7, Issue 2, Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021)

Abstract
This artifact includes the Coq formalization associated with the paper Type-Directed Operational Semantics for Gradual Typing submitted in ECOOP 2021. The paper illustrates how to employ TDOS on gradually typed languages using two calculi. The first calculus, called λB, is inspired by the semantics of the blame calculus(λB^g) and is sound with λB^g. The second calculus, called λB^r, explores a different design space in the semantics of gradually typed languages. This document explains how to run the Coq formalization. Artifact can either be compiled in the pre-built docker image with all the dependencies installed or it could be built from the scratch. Sections 1-7 explain the basic information about the artifact. Section 7 explains how to get the docker image for the artifact. Section 8 explains the prerequisites and the steps to run coq files from scratch. Section 9 explains coq files briefly. Section 10 shows the correspondence of important lemmas, definitions and pictures discussed in the paper with their respective Coq formalization.
Cite as

Wenjia Ye, Bruno C. d. S. Oliveira, and Xuejing Huang. Type-Directed Operational Semantics for Gradual Typing (Artifact). In Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021). Dagstuhl Artifacts Series (DARTS), Volume 7, Issue 2, pp. 9:1-9:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Article{ye_et_al:DARTS.7.2.9,
  author =	{Ye, Wenjia and Oliveira, Bruno C. d. S. and Huang, Xuejing},
  title =	{{Type-Directed Operational Semantics for Gradual Typing (Artifact)}},
  pages =	{9:1--9:6},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2021},
  volume =	{7},
  number =	{2},
  editor =	{Ye, Wenjia and Oliveira, Bruno C. d. S. and Huang, Xuejing},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.7.2.9},
  URN =		{urn:nbn:de:0030-drops-140337},
  doi =		{10.4230/DARTS.7.2.9},
  annote =	{Keywords: Gradual Typing, Operational Semantics, Type Systems}
}
Document
Artifact
DOI: 10.4230/DARTS.7.2.11
Compositional Programming (Artifact)

Authors: Weixin Zhang, Yaozhu Sun, and Bruno C. d. S. Oliveira

Published in: DARTS, Volume 7, Issue 2, Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021)

Abstract
Our main paper presents CP, a Compositional Programming language in a statically typed modular programming style. This artifact includes its Haskell implementation, together with several examples and three case studies written in CP. All code snippets in our main paper can be type-checked and run using our CP interpreter.
Cite as

Weixin Zhang, Yaozhu Sun, and Bruno C. d. S. Oliveira. Compositional Programming (Artifact). In Special Issue of the 35th European Conference on Object-Oriented Programming (ECOOP 2021). Dagstuhl Artifacts Series (DARTS), Volume 7, Issue 2, pp. 11:1-11:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@Article{zhang_et_al:DARTS.7.2.11,
  author =	{Zhang, Weixin and Sun, Yaozhu and Oliveira, Bruno C. d. S.},
  title =	{{Compositional Programming (Artifact)}},
  pages =	{11:1--11:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2021},
  volume =	{7},
  number =	{2},
  editor =	{Zhang, Weixin and Sun, Yaozhu and Oliveira, Bruno C. d. S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.7.2.11},
  URN =		{urn:nbn:de:0030-drops-140356},
  doi =		{10.4230/DARTS.7.2.11},
  annote =	{Keywords: Expression Problem, Compositionality, Traits}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2021.12
Type-Directed Operational Semantics for Gradual Typing

Authors: Wenjia Ye, Bruno C. d. S. Oliveira, and Xuejing Huang

Published in: LIPIcs, Volume 194, 35th European Conference on Object-Oriented Programming (ECOOP 2021)

Abstract
The semantics of gradually typed languages is typically given indirectly via an elaboration into a cast calculus. This contrasts with more conventional formulations of programming language semantics, where the semantics of a language is given directly using, for instance, an operational semantics. This paper presents a new approach to give the semantics of gradually typed languages directly. We use a recently proposed variant of small-step operational semantics called type-directed operational semantics (TDOS). In TDOS type annotations become operationally relevant and can affect the result of a program. In the context of a gradually typed language, such type annotations are used to trigger type-based conversions on values. We illustrate how to employ TDOS on gradually typed languages using two calculi. The first calculus, called λ B^g, is inspired by the semantics of the blame calculus, but it has implicit type conversions, enabling it to be used as a gradually typed language. The second calculus, called λ B^r, explores a different design space in the semantics of gradually typed languages. It uses a so-called blame recovery semantics, which enables eliminating some false positives where blame is raised but normal computation could succeed. For both calculi, type safety is proved. Furthermore we show that the semantics of λ B^g is sound with respect to the semantics of the blame calculus, and that λ B^r comes with a gradual guarantee. All the results have been mechanically formalized in the Coq theorem prover.
Cite as

Wenjia Ye, Bruno C. d. S. Oliveira, and Xuejing Huang. Type-Directed Operational Semantics for Gradual Typing. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 12:1-12:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{ye_et_al:LIPIcs.ECOOP.2021.12,
  author =	{Ye, Wenjia and Oliveira, Bruno C. d. S. and Huang, Xuejing},
  title =	{{Type-Directed Operational Semantics for Gradual Typing}},
  booktitle =	{35th European Conference on Object-Oriented Programming (ECOOP 2021)},
  pages =	{12:1--12:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-190-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{194},
  editor =	{M{\o}ller, Anders and Sridharan, Manu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2021.12},
  URN =		{urn:nbn:de:0030-drops-140551},
  doi =		{10.4230/LIPIcs.ECOOP.2021.12},
  annote =	{Keywords: Gradual Typing, Type Systems, Operational Semantics}
}
Document
Artifact
DOI: 10.4230/DARTS.6.2.8
The Duality of Subtyping (Artifact)

Authors: Bruno C. d. S. Oliveira, Cui Shaobo, and Baber Rehman

Published in: DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
This artifact contains the Coq formalization associated with the paper The Duality of Subtyping submitted in ECOOP 2020. This document explains how to run the Coq formalization. Artifact can either be compiled in the pre-built docker image with all the dependencies installed or it could be built from the scratch. Sections 1-7 explain the basic information about the artifact. Section A explains how to get the docker image for the artifact. Section B explains the prerequisites and the steps to run coq files from scratch. Section C explains coq files briefly. Section D shows the correspondence between important lemmas discussed in paper and their respective Coq formalization. The term MonoTyping used in artifact corresponds to the standard subtyping systems.
Cite as

Bruno C. d. S. Oliveira, Cui Shaobo, and Baber Rehman. The Duality of Subtyping (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 8:1-8:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{oliveira_et_al:DARTS.6.2.8,
  author =	{Oliveira, Bruno C. d. S. and Shaobo, Cui and Rehman, Baber},
  title =	{{The Duality of Subtyping (Artifact)}},
  pages =	{8:1--8:6},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  editor =	{Oliveira, Bruno C. d. S. and Shaobo, Cui and Rehman, Baber},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.6.2.8},
  URN =		{urn:nbn:de:0030-drops-132051},
  doi =		{10.4230/DARTS.6.2.8},
  annote =	{Keywords: DuoTyping, OOP, Duality, Subtyping, Supertyping}
}
Document
Artifact
DOI: 10.4230/DARTS.6.2.9
A Type-Directed Operational Semantics For a Calculus with a Merge Operator (Artifact)

Authors: Xuejing Huang and Bruno C. d. S. Oliveira

Published in: DARTS, Volume 6, Issue 2, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
Our companion paper proposes a type-directed operational semantics (TDOS) for λ_i^{:}: a calculus with intersection types and a merge operator. The artifact contains the specification of λ_i^{:} and its TDOS, and related Coq code. λ_i^{:} is formalized using the locally nameless representation with cofinite quantification. The Coq definition and some infrastructure code are generated by Ott and LNgen. λ_i^{:} is inspired by two closely related calculi by Dunfield (2014) and Oliveira et al. (2016), and a simple variant of it is designed to demonstrate the possibility to match with them without any modification. To relate the two calculi with λ_i^{:}, a sound theorem on semantics and a completeness theorem on typing are proved for each variant. In addition, we extended the bidirectional typing of Oliveira et al.’s λ_i calculus, and designed an elaboration from it to λ_i^{:}, to show that many of λ_i^{:}’s explicit annotations can be inferred automatically.
Cite as

Xuejing Huang and Bruno C. d. S. Oliveira. A Type-Directed Operational Semantics For a Calculus with a Merge Operator (Artifact). In Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020). Dagstuhl Artifacts Series (DARTS), Volume 6, Issue 2, pp. 9:1-9:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@Article{huang_et_al:DARTS.6.2.9,
  author =	{Huang, Xuejing and Oliveira, Bruno C. d. S.},
  title =	{{A Type-Directed Operational Semantics For a Calculus with a Merge Operator (Artifact)}},
  pages =	{9:1--9:4},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2020},
  volume =	{6},
  number =	{2},
  editor =	{Huang, Xuejing and Oliveira, Bruno C. d. S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DARTS.6.2.9},
  URN =		{urn:nbn:de:0030-drops-132060},
  doi =		{10.4230/DARTS.6.2.9},
  annote =	{Keywords: operational semantics, type systems, intersection types}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2020.26
A Type-Directed Operational Semantics For a Calculus with a Merge Operator

Authors: Xuejing Huang and Bruno C. d. S. Oliveira

Published in: LIPIcs, Volume 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020)

Abstract
Calculi with disjoint intersection types and a merge operator provide general mechanisms that can subsume various other features. Such calculi can also encode highly dynamic forms of object composition, which capture common programming patterns in dynamically typed languages (such as JavaScript) in a fully statically typed manner. Unfortunately, unlike many other foundational calculi (such as System F, System F_{< :} or Featherweight Java), recent calculi with the merge operator lack a (direct) operational semantics with standard and expected properties such as determinism and subject-reduction. Furthermore the metatheory for such calculi can only account for terminating programs, which is a significant restriction in practice. This paper proposes a type-directed operational semantics (TDOS) for λ_i^{:}: a calculus with intersection types and a merge operator. The calculus is inspired by two closely related calculi by Dunfield (2014) and Oliveira et al. (2016). Although Dunfield proposes a direct small-step semantics for her calculus, her semantics lacks both determinism and subject-reduction. Using our TDOS we obtain a direct semantics for λ_i^{:} that has both properties. To fully obtain determinism, the λ_i^{:} calculus employs a disjointness restriction proposed in Oliveira et al.’s λ_i calculus. As an added benefit the TDOS approach deals with recursion in a straightforward way, unlike λ_i and subsequent calculi where recursion is problematic. To further relate λ_i^{:} to the calculi by Dunfield and Oliveira et al. we show two results. Firstly, the semantics of λ_i^{:} is sound with respect to Dunfield’s small-step semantics. Secondly, we show that the type system of λ_i^{:} is complete with respect to the λ_i type system. All results have been fully formalized in the Coq theorem prover.
Cite as

Xuejing Huang and Bruno C. d. S. Oliveira. A Type-Directed Operational Semantics For a Calculus with a Merge Operator. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 26:1-26:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{huang_et_al:LIPIcs.ECOOP.2020.26,
  author =	{Huang, Xuejing and Oliveira, Bruno C. d. S.},
  title =	{{A Type-Directed Operational Semantics For a Calculus with a Merge Operator}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{26:1--26:32},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-154-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{166},
  editor =	{Hirschfeld, Robert and Pape, Tobias},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.26},
  URN =		{urn:nbn:de:0030-drops-131832},
  doi =		{10.4230/LIPIcs.ECOOP.2020.26},
  annote =	{Keywords: operational semantics, type systems, intersection types}
}
  • Refine by Author
  • 23 Oliveira, Bruno C. d. S.
  • 8 Huang, Xuejing
  • 5 Bi, Xuan
  • 4 Rehman, Baber
  • 3 Schrijvers, Tom
  • Show More...

  • Refine by Classification
  • 11 Software and its engineering → Object oriented languages
  • 11 Theory of computation → Type theory
  • 5 Software and its engineering → Polymorphism
  • 2 Software and its engineering → General programming languages
  • 1 Theory of computation → Circuit complexity

  • Refine by Keyword
  • 6 intersection types
  • 4 operational semantics
  • 3 Intersection types
  • 3 OOP
  • 2 Disjointness
  • Show More...

  • Refine by Type
  • 24 document

  • Refine by Publication Year
  • 6 2022
  • 5 2018
  • 5 2020
  • 3 2021
  • 3 2023
  • Show More...

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