Search Results

Documents authored by Oliveira e Silva, Miguel

Found 12 Possible Name Variants:

Oliveira, Miguel

Document
DOI: 10.4230/OASIcs.SLATE.2020.4
BhTSL, Behavior Trees Specification and Processing

Authors: Miguel Oliveira, Pedro Mimoso Silva, Pedro Moura, José João Almeida, and Pedro Rangel Henriques

Published in: OASIcs, Volume 83, 9th Symposium on Languages, Applications and Technologies (SLATE 2020)

Abstract
In the context of game development, there is always the need for describing behaviors for various entities, whether NPCs or even the world itself. That need requires a formalism to describe properly such behaviors. As the gaming industry has been growing, many approaches were proposed. First, finite state machines were used and evolved to hierarchical state machines. As that formalism was not enough, a more powerful concept appeared. Instead of using states for describing behaviors, people started to use tasks. This concept was incorporated in behavior trees. This paper focuses in the specification and processing of Behavior Trees. A DSL designed for that purpose will be introduced. It will also be discussed a generator that produces LaTeX diagrams to document the trees, and a Python module to implement the behavior described. Additionally, a simulator will be presented. These achievements will be illustrated using a concrete game as a case study.
Cite as

Miguel Oliveira, Pedro Mimoso Silva, Pedro Moura, José João Almeida, and Pedro Rangel Henriques. BhTSL, Behavior Trees Specification and Processing. In 9th Symposium on Languages, Applications and Technologies (SLATE 2020). Open Access Series in Informatics (OASIcs), Volume 83, pp. 4:1-4:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{oliveira_et_al:OASIcs.SLATE.2020.4,
  author =	{Oliveira, Miguel and Silva, Pedro Mimoso and Moura, Pedro and Almeida, Jos\'{e} Jo\~{a}o and Henriques, Pedro Rangel},
  title =	{{BhTSL, Behavior Trees Specification and Processing}},
  booktitle =	{9th Symposium on Languages, Applications and Technologies (SLATE 2020)},
  pages =	{4:1--4:13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-165-8},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{83},
  editor =	{Sim\~{o}es, Alberto and Henriques, Pedro Rangel and Queir\'{o}s, Ricardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SLATE.2020.4},
  URN =		{urn:nbn:de:0030-drops-130174},
  doi =		{10.4230/OASIcs.SLATE.2020.4},
  annote =	{Keywords: Game development, Behavior trees (BT), NPC, DSL, Code generation}
}

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.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.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
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.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.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.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.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.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.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.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.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.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.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.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.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}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2020.27
Row and Bounded Polymorphism via Disjoint Polymorphism

Authors: Ningning Xie, Bruno C. d. S. Oliveira, Xuan Bi, and Tom Schrijvers

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

Abstract
Polymorphism and subtyping are important features in mainstream OO languages. The most common way to integrate the two is via 𝖥_{< :} style bounded quantification. A closely related mechanism is row polymorphism, which provides an alternative to subtyping, while still enabling many of the same applications. Yet another approach is to have type systems with intersection types and polymorphism. A recent addition to this design space are calculi with disjoint intersection types and disjoint polymorphism. With all these alternatives it is natural to wonder how they are related. This paper provides an answer to this question. We show that disjoint polymorphism can recover forms of both row polymorphism and bounded polymorphism, while retaining key desirable properties, such as type-safety and decidability. Furthermore, we identify the extra power of disjoint polymorphism which enables additional features that cannot be easily encoded in calculi with row polymorphism or bounded quantification alone. Ultimately we expect that our work is useful to inform language designers about the expressive power of those common features, and to simplify implementations and metatheory of feature-rich languages with polymorphism and subtyping.
Cite as

Ningning Xie, Bruno C. d. S. Oliveira, Xuan Bi, and Tom Schrijvers. Row and Bounded Polymorphism via Disjoint Polymorphism. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 27:1-27:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{xie_et_al:LIPIcs.ECOOP.2020.27,
  author =	{Xie, Ningning and Oliveira, Bruno C. d. S. and Bi, Xuan and Schrijvers, Tom},
  title =	{{Row and Bounded Polymorphism via Disjoint Polymorphism}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{27:1--27:30},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.27},
  URN =		{urn:nbn:de:0030-drops-131846},
  doi =		{10.4230/LIPIcs.ECOOP.2020.27},
  annote =	{Keywords: Intersection types, bounded polymorphism, row polymorphism}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2020.29
The Duality of Subtyping

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

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

Abstract
Subtyping is a concept frequently encountered in many programming languages and calculi. Various forms of subtyping exist for different type system features, including intersection types, union types or bounded quantification. Normally these features are designed independently of each other, without exploiting obvious similarities (or dualities) between features. This paper proposes a novel methodology for designing subtyping relations that exploits duality between features. At the core of our methodology is a generalization of subtyping relations, which we call Duotyping. Duotyping is parameterized by the mode of the relation. One of these modes is the usual subtyping, while another mode is supertyping (the dual of subtyping). Using the mode it is possible to generalize the usual rules of subtyping to account not only for the intended behaviour of one particular language construct, but also of its dual. Duotyping brings multiple benefits, including: shorter specifications and implementations, dual features that come essentially for free, as well as new proof techniques for various properties of subtyping. To evaluate a design based on Duotyping against traditional designs, we formalized various calculi with common OOP features (including union types, intersection types and bounded quantification) in Coq in both styles. Our results show that the metatheory when using Duotyping does not come at a significant cost: the metatheory with Duotyping has similar complexity and size compared to the metatheory for traditional designs. However, we discover new features as duals to well-known features. Furthermore, we also show that Duotyping can significantly simplify transitivity proofs for many of the calculi studied by us.
Cite as

Bruno C. d. S. Oliveira, Cui Shaobo, and Baber Rehman. The Duality of Subtyping. In 34th European Conference on Object-Oriented Programming (ECOOP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 166, pp. 29:1-29:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{oliveira_et_al:LIPIcs.ECOOP.2020.29,
  author =	{Oliveira, Bruno C. d. S. and Shaobo, Cui and Rehman, Baber},
  title =	{{The Duality of Subtyping}},
  booktitle =	{34th European Conference on Object-Oriented Programming (ECOOP 2020)},
  pages =	{29:1--29:29},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2020.29},
  URN =		{urn:nbn:de:0030-drops-131864},
  doi =		{10.4230/LIPIcs.ECOOP.2020.29},
  annote =	{Keywords: DuoTyping, OOP, Duality, Subtyping, Supertyping}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2018.9
Typed First-Class Traits

Authors: Xuan Bi and Bruno C. d. S. Oliveira

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

Abstract
Many dynamically-typed languages (including JavaScript, Ruby, Python or Racket) support first-class classes, or related concepts such as first-class traits and/or mixins. In those languages classes are first-class values and, like any other values, they can be passed as an argument, or returned from a function. Furthermore first-class classes support dynamic inheritance: i.e. they can inherit from other classes at runtime, enabling programmers to abstract over the inheritance hierarchy. In contrast, type system limitations prevent most statically-typed languages from having first-class classes and dynamic inheritance. This paper shows the design of SEDEL: a polymorphic statically-typed language with first-class traits, supporting dynamic inheritance as well as conventional OO features such as dynamic dispatching and abstract methods. To address the challenges of type-checking first-class traits, SEDEL employs a type system based on the recent work on disjoint intersection types and disjoint polymorphism. The novelty of SEDEL over core disjoint intersection calculi are source level features for practical OO programming, including first-class traits with dynamic inheritance, dynamic dispatching and abstract methods. Inspired by Cook and Palsberg's work on the denotational semantics for inheritance, we show how to design a source language that can be elaborated into Alpuim et al.'s F_{i} (a core polymorphic calculus with records supporting disjoint polymorphism). We illustrate the applicability of SEDEL with several example uses for first-class traits, and a case study that modularizes programming language interpreters using a highly modular form of visitors.
Cite as

Xuan Bi and Bruno C. d. S. Oliveira. Typed First-Class Traits. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 9:1-9:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bi_et_al:LIPIcs.ECOOP.2018.9,
  author =	{Bi, Xuan and Oliveira, Bruno C. d. S.},
  title =	{{Typed First-Class Traits}},
  booktitle =	{32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
  pages =	{9:1--9: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.9},
  URN =		{urn:nbn:de:0030-drops-92145},
  doi =		{10.4230/LIPIcs.ECOOP.2018.9},
  annote =	{Keywords: traits, extensible designs}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2018.20
FHJ: A Formal Model for Hierarchical Dispatching and Overriding

Authors: Yanlin Wang, Haoyuan Zhang, Bruno C. d. S. Oliveira, and Marco Servetto

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

Abstract
Multiple inheritance is a valuable feature for Object-Oriented Programming. However, it is also tricky to get right, as illustrated by the extensive literature on the topic. A key issue is the ambiguity arising from inheriting multiple parents, which can have conflicting methods. Numerous existing work provides solutions for conflicts which arise from diamond inheritance: i.e. conflicts that arise from implementations sharing a common ancestor. However, most mechanisms are inadequate to deal with unintentional method conflicts: conflicts which arise from two unrelated methods that happen to share the same name and signature. This paper presents a new model called Featherweight Hierarchical Java (FHJ) that deals with unintentional method conflicts. In our new model, which is partly inspired by C++, conflicting methods arising from unrelated methods can coexist in the same class, and hierarchical dispatching supports unambiguous lookups in the presence of such conflicting methods. To avoid ambiguity, hierarchical information is employed in method dispatching, which uses a combination of static and dynamic type information to choose the implementation of a method at run-time. Furthermore, unlike all existing inheritance models, our model supports hierarchical method overriding: that is, methods can be independently overridden along the multiple inheritance hierarchy. We give illustrative examples of our language and features and formalize FHJ as a minimal Featherweight-Java style calculus.
Cite as

Yanlin Wang, Haoyuan Zhang, Bruno C. d. S. Oliveira, and Marco Servetto. FHJ: A Formal Model for Hierarchical Dispatching and Overriding. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 20:1-20:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{wang_et_al:LIPIcs.ECOOP.2018.20,
  author =	{Wang, Yanlin and Zhang, Haoyuan and Oliveira, Bruno C. d. S. and Servetto, Marco},
  title =	{{FHJ: A Formal Model for Hierarchical Dispatching and Overriding}},
  booktitle =	{32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
  pages =	{20:1--20:30},
  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.20},
  URN =		{urn:nbn:de:0030-drops-92259},
  doi =		{10.4230/LIPIcs.ECOOP.2018.20},
  annote =	{Keywords: multiple inheritance, hierarchical dispatching, OOP, language design}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2018.22
The Essence of Nested Composition

Authors: Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers

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

Abstract
Calculi with disjoint intersection types support an introduction form for intersections called the merge operator, while retaining a coherent semantics. Disjoint intersections types have great potential to serve as a foundation for powerful, flexible and yet type-safe and easy to reason OO languages. This paper shows how to significantly increase the expressive power of disjoint intersection types by adding support for nested subtyping and composition, which enables simple forms of family polymorphism to be expressed in the calculus. The extension with nested subtyping and composition is challenging, for two different reasons. Firstly, the subtyping relation that supports these features is non-trivial, especially when it comes to obtaining an algorithmic version. Secondly, the syntactic method used to prove coherence for previous calculi with disjoint intersection types is too inflexible, making it hard to extend those calculi with new features (such as nested subtyping). We show how to address the first problem by adapting and extending the Barendregt, Coppo and Dezani (BCD) subtyping rules for intersections with records and coercions. A sound and complete algorithmic system is obtained by using an approach inspired by Pierce's work. To address the second problem we replace the syntactic method to prove coherence, by a semantic proof method based on logical relations. Our work has been fully formalized in Coq, and we have an implementation of our calculus.
Cite as

Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. The Essence of Nested Composition. In 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 109, pp. 22:1-22:33, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{bi_et_al:LIPIcs.ECOOP.2018.22,
  author =	{Bi, Xuan and Oliveira, Bruno C. d. S. and Schrijvers, Tom},
  title =	{{The Essence of Nested Composition}},
  booktitle =	{32nd European Conference on Object-Oriented Programming (ECOOP 2018)},
  pages =	{22:1--22:33},
  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.22},
  URN =		{urn:nbn:de:0030-drops-92275},
  doi =		{10.4230/LIPIcs.ECOOP.2018.22},
  annote =	{Keywords: nested composition, family polymorphism, intersection types, coherence}
}
Document
DOI: 10.4230/DARTS.4.3.5
The Essence of Nested Composition (Artifact)

Authors: Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers

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

Abstract
The artifact contains the Coq formalization of \name, a simple calculus with disjoint intersection types supporting nested subtyping and composition, as described in the companion paper.
Cite as

Xuan Bi, Bruno C. d. S. Oliveira, and Tom Schrijvers. The Essence of Nested Composition (Artifact). In Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 5:1-5:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{bi_et_al:DARTS.4.3.5,
  author =	{Bi, Xuan and Oliveira, Bruno C. d. S. and Schrijvers, Tom},
  title =	{{The Essence of Nested Composition (Artifact)}},
  pages =	{5:1--5:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2018},
  volume =	{4},
  number =	{3},
  editor =	{Bi, Xuan and Oliveira, Bruno C. d. S. and Schrijvers, Tom},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.4.3.5},
  URN =		{urn:nbn:de:0030-drops-92363},
  doi =		{10.4230/DARTS.4.3.5},
  annote =	{Keywords: nested composition, family polymorphism, intersection types, coherence}
}
Document
DOI: 10.4230/DARTS.4.3.9
Typed First-Class Traits (Artifact)

Authors: Xuan Bi and Bruno C. d. S. Oliveira

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

Abstract
This artifact contains the prototype Haskell implementation of SEDEL, with support for first-class traits, as described in the companion paper. This artifact also contains the source code of the case study on "Anatomy of Programming Languages", illustrating how effective SEDEL is in terms of modularizing programming language features. For comparison, it also includes a vanilla Haskell implementation of the case study without any code reuse.
Cite as

Xuan Bi and Bruno C. d. S. Oliveira. Typed First-Class Traits (Artifact). In Special Issue of the 32nd European Conference on Object-Oriented Programming (ECOOP 2018). Dagstuhl Artifacts Series (DARTS), Volume 4, Issue 3, pp. 9:1-9:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{bi_et_al:DARTS.4.3.9,
  author =	{Bi, Xuan and Oliveira, Bruno C. d. S.},
  title =	{{Typed First-Class Traits (Artifact)}},
  pages =	{9:1--9:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2018},
  volume =	{4},
  number =	{3},
  editor =	{Bi, Xuan and Oliveira, Bruno C. d. S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.4.3.9},
  URN =		{urn:nbn:de:0030-drops-92407},
  doi =		{10.4230/DARTS.4.3.9},
  annote =	{Keywords: traits, extensible designs}
}
Document
DOI: 10.4230/DARTS.3.2.10
EVF: An Extensible and Expressive Visitor Framework for Programming Language Reuse (Artifact)

Authors: Weixin Zhang and Bruno C. d. S. Oliveira

Published in: DARTS, Volume 3, Issue 2, Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract
This artifact is based on EVF, an extensible and expressive Java visitor framework. EVF aims at reducing the effort involved in creation and reuse of programming languages. EVF an annotation processor that automatically generate boilerplate ASTs and AST for a given an Object Algebra interface. This artifact contains source code of the case study on "Types and Programming Languages", illustrating how effective EVF is in modularizing programming languages. There is also a microbenchmark in the artifact that shows that EVF has reasonable performance with respect to traditional visitors.
Cite as

Weixin Zhang and Bruno C. d. S. Oliveira. EVF: An Extensible and Expressive Visitor Framework for Programming Language Reuse (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 10:1-10:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{zhang_et_al:DARTS.3.2.10,
  author =	{Zhang, Weixin and Oliveira, Bruno C. d. S.},
  title =	{{EVF: An Extensible and Expressive Visitor Framework for Programming Language Reuse (Artifact)}},
  pages =	{10:1--10:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2017},
  volume =	{3},
  number =	{2},
  editor =	{Zhang, Weixin and Oliveira, Bruno C. d. S.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.10},
  URN =		{urn:nbn:de:0030-drops-72918},
  doi =		{10.4230/DARTS.3.2.10},
  annote =	{Keywords: visitor pattern, object algebras, modularity, domain-specific languages}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2017.29
EVF: An Extensible and Expressive Visitor Framework for Programming Language Reuse

Authors: Weixin Zhang and Bruno C. d. S. Oliveira

Published in: LIPIcs, Volume 74, 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract
Object Algebras are a design pattern that enables extensibility, modularity, and reuse in mainstream object-oriented languages such as Java. The theoretical foundations of Object Algebras are rooted on Church encodings of datatypes, which are in turn closely related to folds in functional programming. Unfortunately, it is well-known that certain programs are difficult to write, and may incur performance penalties when using Church-encodings/folds. This paper presents EVF: an extensible and expressive Java Visitor framework. The visitors supported by EVF generalize Object Algebras and enable writing programs using a generally recursive style rather than folds. The use of such generally recursive style enables users to more naturally write programs, which would otherwise require contrived workarounds using a fold-like structure. EVF visitors retain the type-safe extensibility of Object Algebras. The key advance in EVF is a novel technique to support extensible external visitors. Extensible external visitors are able to control traversals with direct access to the data structure being traversed, allowing dependent operations to be defined modularly without the need of advanced type system features. To make EVF practical, the framework employs annotations to automatically generate large amounts of boilerplate code related to visitors and traversals. To illustrate the applicability of EVF we conduct a case study, which refactors a large number of non-modular interpreters from the “Types and Programming Languages” (TAPL) book. Using EVF we are able to create a modular software product line (SPL) of the TAPL interpreters, enabling sharing of large portions of code and features. The TAPL software product line contains several modular operations, which would be non-trivial to define with standard Object Algebras.
Cite as

Weixin Zhang and Bruno C. d. S. Oliveira. EVF: An Extensible and Expressive Visitor Framework for Programming Language Reuse. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 29:1-29:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{zhang_et_al:LIPIcs.ECOOP.2017.29,
  author =	{Zhang, Weixin and Oliveira, Bruno C. d. S.},
  title =	{{EVF: An Extensible and Expressive Visitor Framework for Programming Language Reuse}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{29:1--29:32},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{M\"{u}ller, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.29},
  URN =		{urn:nbn:de:0030-drops-72749},
  doi =		{10.4230/LIPIcs.ECOOP.2017.29},
  annote =	{Keywords: Visitor Pattern, Object Algebras, Modularity, Domain-Specific Languages}
}

Oliveira, Fabiano S.

Document
DOI: 10.4230/LIPIcs.MFCS.2021.38
Maximum Cut on Interval Graphs of Interval Count Four Is NP-Complete

Authors: Celina M. H. de Figueiredo, Alexsander A. de Melo, Fabiano S. Oliveira, and Ana Silva

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
The computational complexity of the MaxCut problem restricted to interval graphs has been open since the 80’s, being one of the problems proposed by Johnson on his Ongoing Guide to NP-completeness, and has been settled as NP-complete only recently by Adhikary, Bose, Mukherjee and Roy. On the other hand, many flawed proofs of polynomiality for MaxCut on the more restrictive class of unit/proper interval graphs (or graphs with interval count 1) have been presented along the years, and the classification of the problem is still not known. In this paper, we present the first NP-completeness proof for MaxCut when restricted to interval graphs with bounded interval count, namely graphs with interval count 4.
Cite as

Celina M. H. de Figueiredo, Alexsander A. de Melo, Fabiano S. Oliveira, and Ana Silva. Maximum Cut on Interval Graphs of Interval Count Four Is NP-Complete. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 38:1-38:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{defigueiredo_et_al:LIPIcs.MFCS.2021.38,
  author =	{de Figueiredo, Celina M. H. and de Melo, Alexsander A. and Oliveira, Fabiano S. and Silva, Ana},
  title =	{{Maximum Cut on Interval Graphs of Interval Count Four Is NP-Complete}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{38:1--38:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.38},
  URN =		{urn:nbn:de:0030-drops-144781},
  doi =		{10.4230/LIPIcs.MFCS.2021.38},
  annote =	{Keywords: maximum cut, interval graphs, interval lengths, interval count, NP-complete}
}

Oliveira, Daniela

Document
DOI: 10.4230/DagRep.9.7.117
Cybersafety Threats - from Deception to Aggression (Dagstuhl Seminar 19302)

Authors: Zinaida Benenson, Marianne Junger, Daniela Oliveira, and Gianluca Stringhini

Published in: Dagstuhl Reports, Volume 9, Issue 7 (2020)

Abstract
A number of malicious activities, such as cyberbullying, disinformation, and phishing, are becoming increasingly serious, affecting the wellbeing of Internet users both financially and psychologically. These malicious activities are inherently socio-technical, and therefore effective countermeasures against them must draw not only from engineering and computer science, but also from other disciplines. To discuss these topics and find appropriate countermeasures, we assembled a group of researchers from a number of disciplines such as computer science, criminology, crime science, psychology, and education. Through five days of brainstorming and discussion, the participants developed a roadmap for future research on these topics, along four directions: modelling the attackers, measuring human behavior, detection and prevention approaches for online threats to adolescents, and understanding unintended consequences of mitigation techniques.
Cite as

Zinaida Benenson, Marianne Junger, Daniela Oliveira, and Gianluca Stringhini. Cybersafety Threats - from Deception to Aggression (Dagstuhl Seminar 19302). In Dagstuhl Reports, Volume 9, Issue 7, pp. 117-154, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@Article{benenson_et_al:DagRep.9.7.117,
  author =	{Benenson, Zinaida and Junger, Marianne and Oliveira, Daniela and Stringhini, Gianluca},
  title =	{{Cybersafety Threats - from Deception to Aggression (Dagstuhl Seminar 19302)}},
  pages =	{117--154},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2019},
  volume =	{9},
  number =	{7},
  editor =	{Benenson, Zinaida and Junger, Marianne and Oliveira, Daniela and Stringhini, Gianluca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.9.7.117},
  URN =		{urn:nbn:de:0030-drops-116387},
  doi =		{10.4230/DagRep.9.7.117},
  annote =	{Keywords: Cybersafety, Legal and Ethical Issues on the Web, Online Social Networks, Security and Privacy}
}

Oliveira, Nuno

Document
DOI: 10.4230/OASIcs.SLATE.2021.14
Using Machine Learning for Vulnerability Detection and Classification

Authors: Tiago Baptista, Nuno Oliveira, and Pedro Rangel Henriques

Published in: OASIcs, Volume 94, 10th Symposium on Languages, Applications and Technologies (SLATE 2021)

Abstract
The work described in this paper aims at developing a machine learning based tool for automatic identification of vulnerabilities on programs (source, high level code), that uses an abstract syntax tree representation. It is based on FastScan, using code2seq approach. Fastscan is a recently developed system aimed capable of detecting vulnerabilities in source code using machine learning techniques. Nevertheless, FastScan is not able of identifying the vulnerability type. In the presented work the main goal is to go further and develop a method to identify specific types of vulnerabilities. As will be shown, the goal will be achieved by optimizing the model’s hyperparameters, changing the method of preprocessing the input data and developing an architecture that brings together multiple models to predict different specific vulnerabilities. The preliminary results obtained from the training stage, are very promising. The best f1 metric obtained is 93% resulting in a precision of 90% and accuracy of 85%, according to the performed tests and regarding a trained model to predict vulnerabilities of the injection type.
Cite as

Tiago Baptista, Nuno Oliveira, and Pedro Rangel Henriques. Using Machine Learning for Vulnerability Detection and Classification. In 10th Symposium on Languages, Applications and Technologies (SLATE 2021). Open Access Series in Informatics (OASIcs), Volume 94, pp. 14:1-14:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{baptista_et_al:OASIcs.SLATE.2021.14,
  author =	{Baptista, Tiago and Oliveira, Nuno and Henriques, Pedro Rangel},
  title =	{{Using Machine Learning for Vulnerability Detection and Classification}},
  booktitle =	{10th Symposium on Languages, Applications and Technologies (SLATE 2021)},
  pages =	{14:1--14:14},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-202-0},
  ISSN =	{2190-6807},
  year =	{2021},
  volume =	{94},
  editor =	{Queir\'{o}s, Ricardo and Pinto, M\'{a}rio and Sim\~{o}es, Alberto and Portela, Filipe and Pereira, Maria Jo\~{a}o},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SLATE.2021.14},
  URN =		{urn:nbn:de:0030-drops-144315},
  doi =		{10.4230/OASIcs.SLATE.2021.14},
  annote =	{Keywords: Vulnerability Detection, Source Code Analysis, Machine Learning}
}
Document
DOI: 10.4230/OASIcs.SLATE.2014.61
ReCooPLa: a DSL for Coordination-based Reconfiguration of Software Architectures

Authors: Flávio Rodrigues, Nuno Oliveira, and Luís S. Barbosa

Published in: OASIcs, Volume 38, 3rd Symposium on Languages, Applications and Technologies (2014)

Abstract
In production environments where change is the rule rather than the exception, adaptation of software plays an important role. Such adaptations presuppose dynamic reconfiguration of the system architecture, however, it is in the static setting (design-phase) that such reconfigurations must be designed and analysed, to preclude erroneous evolutions. Modern software systems, which are built from the coordinated composition of loosely-coupled software components, are naturally adaptable; and coordination specification is, usually, the main reference point to inserting changes in these systems. In this paper, a domain-specific language—-referred to as ReCooPLa--is proposed to design reconfigurations that change the coordination structures, so that they are analysed before being applied in run time. Moreover, a reconfiguration engine is introduced, that takes conveniently translated ReCooPLa specifications and applies them to coordination structures.
Cite as

Flávio Rodrigues, Nuno Oliveira, and Luís S. Barbosa. ReCooPLa: a DSL for Coordination-based Reconfiguration of Software Architectures. In 3rd Symposium on Languages, Applications and Technologies. Open Access Series in Informatics (OASIcs), Volume 38, pp. 61-76, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{rodrigues_et_al:OASIcs.SLATE.2014.61,
  author =	{Rodrigues, Fl\'{a}vio and Oliveira, Nuno and Barbosa, Lu{\'\i}s S.},
  title =	{{ReCooPLa: a DSL for Coordination-based Reconfiguration of Software Architectures}},
  booktitle =	{3rd Symposium on Languages, Applications and Technologies},
  pages =	{61--76},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-68-2},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{38},
  editor =	{Pereira, Maria Jo\~{a}o Varanda and Leal, Jos\'{e} Paulo and Sim\~{o}es, Alberto},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SLATE.2014.61},
  URN =		{urn:nbn:de:0030-drops-45593},
  doi =		{10.4230/OASIcs.SLATE.2014.61},
  annote =	{Keywords: domain-specific languages, architectural reconfiguration, coordination}
}
Document
DOI: 10.4230/OASIcs.SLATE.2014.101
Unfuzzying Fuzzy Parsing

Authors: Pedro Carvalho, Nuno Oliveira, and Pedro Rangel Henriques

Published in: OASIcs, Volume 38, 3rd Symposium on Languages, Applications and Technologies (2014)

Abstract
Traditional parsing has always been a focus of discussion among the computer science community. Numerous techniques and algorithms have been proposed along these years, but they require that input texts are correct according to a specific grammar. However, in some cases it's necessary to cope with incorrect or unpredicted inputs that raise ambiguities, making traditional parsing unsuitable. These situations led to the emergence of robust parsing theories, where fuzzy parsing gains relevance. Robust parsing comes with a price by losing precision and decaying performance, as multiple parses of the input may be necessary while looking for an optimal one. In this short paper we briefly describe the main robust parsing techniques and end up proposing a different solution to deal with fuzziness of input texts. It is based on automata where states represent contexts and edges represent potential matches (of constructs of interest) inside those contexts. It is expected that such an approach reduces recognition time and ambiguity as contexts reduce the search space by defining a smaller domain for constructs of interest. Such benefits may be a great addition to the robust parsing area with application on program comprehension, among other research fields.
Cite as

Pedro Carvalho, Nuno Oliveira, and Pedro Rangel Henriques. Unfuzzying Fuzzy Parsing. In 3rd Symposium on Languages, Applications and Technologies. Open Access Series in Informatics (OASIcs), Volume 38, pp. 101-108, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{carvalho_et_al:OASIcs.SLATE.2014.101,
  author =	{Carvalho, Pedro and Oliveira, Nuno and Henriques, Pedro Rangel},
  title =	{{Unfuzzying Fuzzy Parsing}},
  booktitle =	{3rd Symposium on Languages, Applications and Technologies},
  pages =	{101--108},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-68-2},
  ISSN =	{2190-6807},
  year =	{2014},
  volume =	{38},
  editor =	{Pereira, Maria Jo\~{a}o Varanda and Leal, Jos\'{e} Paulo and Sim\~{o}es, Alberto},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SLATE.2014.101},
  URN =		{urn:nbn:de:0030-drops-45637},
  doi =		{10.4230/OASIcs.SLATE.2014.101},
  annote =	{Keywords: robust parsing, fuzzy parsing, automata}
}
Document
DOI: 10.4230/OASIcs.SLATE.2013.155
Choosing Grammars to Support Language Processing Courses

Authors: Maria João Varanda Pereira, Nuno Oliveira, Daniela da Cruz, and Pedro Rangel Henriques

Published in: OASIcs, Volume 29, 2nd Symposium on Languages, Applications and Technologies (2013)

Abstract
Teaching Language Processing courses is a hard task. The level of abstraction inherent to some of the basic concepts in the area and the technical skills required to implement efficient processors are responsible for the number of students that do not learn the subject and do not succeed to finish the course. In this paper we intend to list the main concepts involved in Language Processing subject, and identify the skills required to learn them. In this context, it is feasible to identify the difficulties that lead students to fail. This enables us to suggest some pragmatic ways to overcome those troubles. We will focus on the grammars suitable to motivate students and help them to learn easily the basic concepts. After identifying the characteristics of such grammars, some examples are presented to make concrete and clear our proposal. The contribution of this paper is the systematic way we approach the process of teaching Language Processing courses towards a successful learning activity.
Cite as

Maria João Varanda Pereira, Nuno Oliveira, Daniela da Cruz, and Pedro Rangel Henriques. Choosing Grammars to Support Language Processing Courses. In 2nd Symposium on Languages, Applications and Technologies. Open Access Series in Informatics (OASIcs), Volume 29, pp. 155-168, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{pereira_et_al:OASIcs.SLATE.2013.155,
  author =	{Pereira, Maria Jo\~{a}o Varanda and Oliveira, Nuno and Cruz, Daniela da and Henriques, Pedro Rangel},
  title =	{{Choosing Grammars to Support Language Processing Courses}},
  booktitle =	{2nd Symposium on Languages, Applications and Technologies},
  pages =	{155--168},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-52-1},
  ISSN =	{2190-6807},
  year =	{2013},
  volume =	{29},
  editor =	{Leal, Jos\'{e} Paulo and Rocha, Ricardo and Sim\~{o}es, Alberto},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SLATE.2013.155},
  URN =		{urn:nbn:de:0030-drops-40369},
  doi =		{10.4230/OASIcs.SLATE.2013.155},
  annote =	{Keywords: Teaching Language Processing, Domain Specific Languages, Grammars}
}
Document
DOI: 10.4230/OASIcs.SLATE.2012.91
Problem Domain Oriented Approach for Program Comprehension

Authors: Maria João Varanda Pereira, Mario Marcelo Beron, Daniela da Cruz, Nuno Oliveira, and Pedro Rangel Henriques

Published in: OASIcs, Volume 21, 1st Symposium on Languages, Applications and Technologies (2012)

Abstract
This paper is concerned with an ontology driven approach for Program Comprehension that starts picking up concepts from the problem domain ontology, analyzing source code and, after locating problem concepts in the code, goes up and links them to the programming language ontology. Different location techniques are used to search for concepts embedded in comments, in the code (identifier names and execution traces), and in string-literals associated with I/O statements. The expected result is a mapping between problem domain concepts and code slices. This mapping can be visualized using graph-based approaches like, for instance, navigation facilities through a System Dependency Graph. The paper also describes a PCTool suite, Quixote, that implements the approach proposed.
Cite as

Maria João Varanda Pereira, Mario Marcelo Beron, Daniela da Cruz, Nuno Oliveira, and Pedro Rangel Henriques. Problem Domain Oriented Approach for Program Comprehension. In 1st Symposium on Languages, Applications and Technologies. Open Access Series in Informatics (OASIcs), Volume 21, pp. 91-105, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{varandapereira_et_al:OASIcs.SLATE.2012.91,
  author =	{Varanda Pereira, Maria Jo\~{a}o and Beron, Mario Marcelo and da Cruz, Daniela and Oliveira, Nuno and Henriques, Pedro Rangel},
  title =	{{Problem Domain Oriented Approach for Program Comprehension}},
  booktitle =	{1st Symposium on Languages, Applications and Technologies},
  pages =	{91--105},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-40-8},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{21},
  editor =	{Sim\~{o}es, Alberto and Queir\'{o}s, Ricardo and da Cruz, Daniela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SLATE.2012.91},
  URN =		{urn:nbn:de:0030-drops-35161},
  doi =		{10.4230/OASIcs.SLATE.2012.91},
  annote =	{Keywords: Program Comprehension, Ontology-based SW development, Problem and Program domain mapping, Code Analysis. Software Visualization}
}
Document
DOI: 10.4230/OASIcs.SLATE.2012.175
Learning Spaces for Knowledge Generation

Authors: Nuno Oliveira, Maria João Varanda Pereira, Alda Lopes Gancarski, and Pedro Rangel Henriques

Published in: OASIcs, Volume 21, 1st Symposium on Languages, Applications and Technologies (2012)

Abstract
As the Internet is becoming the main point for information access, Libraries, Museums and similar Institutions are preserving their collections as digital object repositories. In that way, the important information associated with digital objects may be delivered as Internet content over portals equipped with modern interfaces and navigation features. This enables the virtualization of real information exhibition spaces rising new learning paradigms. Geny is a project aiming at defining domain-specific languages and developing tools to generate web-based learning spaces from existent digital object repositories and associated semantic. The motto for Geny is "Generating learning spaces to generate knowledge". Our objective within this project is to use (i) ontologies - one to give semantics to the digital object repository and another to describe the information to exhibit - and (ii) special languages to define the exhibition space, to enable the automatic construction of the learning space supported by a web browser. This paper presents the proposal of the Geny project along with a review of the state of the art concerning learning spaces and their virtualization. Geny is, currently, under appreciation by Fundação para a Ciêencia e a Tecnologia (FCT), the main Portuguese scientific funding institution.
Cite as

Nuno Oliveira, Maria João Varanda Pereira, Alda Lopes Gancarski, and Pedro Rangel Henriques. Learning Spaces for Knowledge Generation. In 1st Symposium on Languages, Applications and Technologies. Open Access Series in Informatics (OASIcs), Volume 21, pp. 175-184, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{oliveira_et_al:OASIcs.SLATE.2012.175,
  author =	{Oliveira, Nuno and Varanda Pereira, Maria Jo\~{a}o and Gancarski, Alda Lopes and Henriques, Pedro Rangel},
  title =	{{Learning Spaces for Knowledge Generation}},
  booktitle =	{1st Symposium on Languages, Applications and Technologies},
  pages =	{175--184},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-40-8},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{21},
  editor =	{Sim\~{o}es, Alberto and Queir\'{o}s, Ricardo and da Cruz, Daniela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SLATE.2012.175},
  URN =		{urn:nbn:de:0030-drops-35228},
  doi =		{10.4230/OASIcs.SLATE.2012.175},
  annote =	{Keywords: Learning Spaces, Knowledge Acquisition, Digital Object Repositories, Ontology-based semantic Web-pages Generation}
}

Oliveira, Tiago

Document
DOI: 10.4230/LIPIcs.OPODIS.2016.30
Exploring Key-Value Stores in Multi-Writer Byzantine-Resilient Register Emulations

Authors: Tiago Oliveira, Ricardo Mendes, and Alysson Bessani

Published in: LIPIcs, Volume 70, 20th International Conference on Principles of Distributed Systems (OPODIS 2016)

Abstract
Resilient register emulation is a fundamental technique to implement dependable storage and distributed systems. In data-centric models, where servers are modeled as fail-prone base objects, classical solutions achieve resilience by using fault-tolerant quorums of read-write registers or read-modify-write objects. Recently, this model has attracted renewed interest due to the popularity of cloud storage providers (e.g., Amazon S3), that can be modeled as key-value stores (KVSs) and combined for providing secure and dependable multi-cloud storage services. In this paper we present three novel wait-free multi-writer multi-reader regular register emulations on top of Byzantine-prone KVSs. We implemented and evaluated these constructions using five existing cloud storage services and show that their performance matches or surpasses existing data-centric register emulations.
Cite as

Tiago Oliveira, Ricardo Mendes, and Alysson Bessani. Exploring Key-Value Stores in Multi-Writer Byzantine-Resilient Register Emulations. In 20th International Conference on Principles of Distributed Systems (OPODIS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 70, pp. 30:1-30:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{oliveira_et_al:LIPIcs.OPODIS.2016.30,
  author =	{Oliveira, Tiago and Mendes, Ricardo and Bessani, Alysson},
  title =	{{Exploring Key-Value Stores in Multi-Writer Byzantine-Resilient Register Emulations}},
  booktitle =	{20th International Conference on Principles of Distributed Systems (OPODIS 2016)},
  pages =	{30:1--30:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-031-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{70},
  editor =	{Fatourou, Panagiota and Jim\'{e}nez, Ernesto and Pedone, Fernando},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2016.30},
  URN =		{urn:nbn:de:0030-drops-70999},
  doi =		{10.4230/LIPIcs.OPODIS.2016.30},
  annote =	{Keywords: Byzantine fault tolerance, register emulation, multi-writer, key-value store, data-centric algorithms}
}
Document
DOI: 10.4230/OASIcs.ICCSW.2015.62
Representing Temporal Patterns in Computer-Interpretable Clinical Guidelines

Authors: António Silva, Tiago Oliveira, Paulo Novais, and José Neves

Published in: OASIcs, Volume 49, 2015 Imperial College Computing Student Workshop (ICCSW 2015)

Abstract
Computer-Interpretable Guidelines (CIGs) as machine-readable versions of clinical protocols have to provide appropriate constructs for the representation of different aspects of medical knowledge, namely administrative information, workflows of procedures, clinical constraints and temporal constraints. This work focuses on the latter, by aiming to develop a comprehensive representation of temporal constraints for machine readable formats of clinical protocols and provide a proper execution engine that deals with different time patterns and constraints placed on them. A model for the representation of time is presented for the CompGuide ontology in Ontology Web language (OWL) along with a comparison with the available formalisms in this field.
Cite as

António Silva, Tiago Oliveira, Paulo Novais, and José Neves. Representing Temporal Patterns in Computer-Interpretable Clinical Guidelines. In 2015 Imperial College Computing Student Workshop (ICCSW 2015). Open Access Series in Informatics (OASIcs), Volume 49, pp. 62-69, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{silva_et_al:OASIcs.ICCSW.2015.62,
  author =	{Silva, Ant\'{o}nio and Oliveira, Tiago and Novais, Paulo and Neves, Jos\'{e}},
  title =	{{Representing Temporal Patterns in Computer-Interpretable Clinical Guidelines}},
  booktitle =	{2015 Imperial College Computing Student Workshop (ICCSW 2015)},
  pages =	{62--69},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-000-2},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{49},
  editor =	{Schulz, Claudia and Liew, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICCSW.2015.62},
  URN =		{urn:nbn:de:0030-drops-54827},
  doi =		{10.4230/OASIcs.ICCSW.2015.62},
  annote =	{Keywords: Computer-Interpretable Guidelines, Temporal Constraints, Clinical Decision Support, Ontologies}
}

Oliveira, Francisco José Moreira

Document
Short Paper
DOI: 10.4230/OASIcs.SLATE.2020.15
Open Web Ontobud: An Open Source RDF4J Frontend (Short Paper)

Authors: Francisco José Moreira Oliveira and José Carlos Ramalho

Published in: OASIcs, Volume 83, 9th Symposium on Languages, Applications and Technologies (SLATE 2020)

Abstract
Nowadays, we deal with increasing volumes of data. A few years ago, data was isolated, which did not allow communication or sharing between datasets. We live in a world where everything is connected, and our data mimics this. Data model focus changed from a square structure like the relational model to a model centered on the relations. Knowledge graphs are the new paradigm to represent and manage this new kind of information structure. Along with this new paradigm, a new kind of database emerged to support the new needs, graph databases! Although there is an increasing interest in this field, only a few native solutions are available. Most of these are commercial, and the ones that are open source have poor interfaces, and for that, they are a little distant from end-users. In this article, we introduce Ontobud, and discuss its design and development. A Web application that intends to improve the interface for one of the most interesting frameworks in this area: RDF4J. RDF4J is a Java framework to deal with RDF triples storage and management. Open Web Ontobud is an open source RDF4J web frontend, created to reduce the gap between end users and the RDF4J backend. We have created a web interface that enables users with a basic knowledge of OWL and SPARQL to explore ontologies and extract information from them.
Cite as

Francisco José Moreira Oliveira and José Carlos Ramalho. Open Web Ontobud: An Open Source RDF4J Frontend (Short Paper). In 9th Symposium on Languages, Applications and Technologies (SLATE 2020). Open Access Series in Informatics (OASIcs), Volume 83, pp. 15:1-15:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{oliveira_et_al:OASIcs.SLATE.2020.15,
  author =	{Oliveira, Francisco Jos\'{e} Moreira and Ramalho, Jos\'{e} Carlos},
  title =	{{Open Web Ontobud: An Open Source RDF4J Frontend}},
  booktitle =	{9th Symposium on Languages, Applications and Technologies (SLATE 2020)},
  pages =	{15:1--15:8},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-165-8},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{83},
  editor =	{Sim\~{o}es, Alberto and Henriques, Pedro Rangel and Queir\'{o}s, Ricardo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SLATE.2020.15},
  URN =		{urn:nbn:de:0030-drops-130283},
  doi =		{10.4230/OASIcs.SLATE.2020.15},
  annote =	{Keywords: RDF4J, Frontend, Open Source, Ontology, REST API, RDF, SPARQL, Graph Databases}
}

Oliveira, Cristóvão

Document
DOI: 10.4230/DagSemProc.05081.2
Architectural Views for CommUnity

Authors: Cristóvão Oliveira and Michel Wermelinger

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

Abstract
CommUnity and its categorical foundations provide a formal approach to Software Architecture (SA). Several concepts such as (re) configuration and (higher-order) connector have been given precise definitions in this setting. One of the cornerstones of the approach is the separation between computation, coordination and distribution. In this paper, we take this separation one step further and define explicit architectural views, one for each concern. They will be used to help to detect errors made while building the architecture. Moreover they will be a support to improve the design of the system by focusing on one concern at a time and/or by combining them with each other.
Cite as

Cristóvão Oliveira and Michel Wermelinger. Architectural Views for CommUnity. In Foundations of Global Computing. Dagstuhl Seminar Proceedings, Volume 5081, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{oliveira_et_al:DagSemProc.05081.2,
  author =	{Oliveira, Crist\'{o}v\~{a}o and Wermelinger, Michel},
  title =	{{Architectural Views for CommUnity}},
  booktitle =	{Foundations of Global Computing},
  pages =	{1--3},
  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.2},
  URN =		{urn:nbn:de:0030-drops-2967},
  doi =		{10.4230/DagSemProc.05081.2},
  annote =	{Keywords: Software Architecture, views, computation, coordination, distribution}
}

Oliveira, Igor Carboni

Document
DOI: 10.4230/LIPIcs.CCC.2019.23
Parity Helps to Compute Majority

Authors: Igor Carboni Oliveira, Rahul Santhanam, and Srikanth Srinivasan

Published in: LIPIcs, Volume 137, 34th Computational Complexity Conference (CCC 2019)

Abstract
We study the complexity of computing symmetric and threshold functions by constant-depth circuits with Parity gates, also known as AC^0[oplus] circuits. Razborov [Alexander A. Razborov, 1987] and Smolensky [Roman Smolensky, 1987; Roman Smolensky, 1993] showed that Majority requires depth-d AC^0[oplus] circuits of size 2^{Omega(n^{1/2(d-1)})}. By using a divide-and-conquer approach, it is easy to show that Majority can be computed with depth-d AC^0[oplus] circuits of size 2^{O~(n^{1/(d-1)})}. This gap between upper and lower bounds has stood for nearly three decades. Somewhat surprisingly, we show that neither the upper bound nor the lower bound above is tight for large d. We show for d >= 5 that any symmetric function can be computed with depth-d AC^0[oplus] circuits of size exp(O~(n^{2/3 * 1/(d-4)})). Our upper bound extends to threshold functions (with a constant additive loss in the denominator of the double exponent). We improve the Razborov-Smolensky lower bound to show that for d >= 3 Majority requires depth-d AC^0[oplus] circuits of size 2^{Omega(n^{1/(2d-4)})}. For depths d <= 4, we are able to refine our techniques to get almost-optimal bounds: the depth-3 AC^0[oplus] circuit size of Majority is 2^{Theta~(n^{1/2})}, while its depth-4 AC^0[oplus] circuit size is 2^{Theta~(n^{1/4})}.
Cite as

Igor Carboni Oliveira, Rahul Santhanam, and Srikanth Srinivasan. Parity Helps to Compute Majority. In 34th Computational Complexity Conference (CCC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 137, pp. 23:1-23:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{oliveira_et_al:LIPIcs.CCC.2019.23,
  author =	{Oliveira, Igor Carboni and Santhanam, Rahul and Srinivasan, Srikanth},
  title =	{{Parity Helps to Compute Majority}},
  booktitle =	{34th Computational Complexity Conference (CCC 2019)},
  pages =	{23:1--23:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-116-0},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{137},
  editor =	{Shpilka, Amir},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2019.23},
  URN =		{urn:nbn:de:0030-drops-108453},
  doi =		{10.4230/LIPIcs.CCC.2019.23},
  annote =	{Keywords: Computational Complexity, Boolean Circuits, Lower Bounds, Parity, Majority}
}
Document
DOI: 10.4230/LIPIcs.CCC.2019.27
Hardness Magnification near State-Of-The-Art Lower Bounds

Authors: Igor Carboni Oliveira, Ján Pich, and Rahul Santhanam

Published in: LIPIcs, Volume 137, 34th Computational Complexity Conference (CCC 2019)

Abstract
This work continues the development of hardness magnification. The latter proposes a new strategy for showing strong complexity lower bounds by reducing them to a refined analysis of weaker models, where combinatorial techniques might be successful. We consider gap versions of the meta-computational problems MKtP and MCSP, where one needs to distinguish instances (strings or truth-tables) of complexity <= s_1(N) from instances of complexity >= s_2(N), and N = 2^n denotes the input length. In MCSP, complexity is measured by circuit size, while in MKtP one considers Levin’s notion of time-bounded Kolmogorov complexity. (In our results, the parameters s_1(N) and s_2(N) are asymptotically quite close, and the problems almost coincide with their standard formulations without a gap.) We establish that for Gap-MKtP[s_1,s_2] and Gap-MCSP[s_1,s_2], a marginal improvement over the state-of-the-art in unconditional lower bounds in a variety of computational models would imply explicit super-polynomial lower bounds. Theorem. There exists a universal constant c >= 1 for which the following hold. If there exists epsilon > 0 such that for every small enough beta > 0 (1) Gap-MCSP[2^{beta n}/c n, 2^{beta n}] !in Circuit[N^{1 + epsilon}], then NP !subseteq Circuit[poly]. (2) Gap-MKtP[2^{beta n}, 2^{beta n} + cn] !in TC^0[N^{1 + epsilon}], then EXP !subseteq TC^0[poly]. (3) Gap-MKtP[2^{beta n}, 2^{beta n} + cn] !in B_2-Formula[N^{2 + epsilon}], then EXP !subseteq Formula[poly]. (4) Gap-MKtP[2^{beta n}, 2^{beta n} + cn] !in U_2-Formula[N^{3 + epsilon}], then EXP !subseteq Formula[poly]. (5) Gap-MKtP[2^{beta n}, 2^{beta n} + cn] !in BP[N^{2 + epsilon}], then EXP !subseteq BP[poly]. (6) Gap-MKtP[2^{beta n}, 2^{beta n} + cn] !in (AC^0[6])[N^{1 + epsilon}], then EXP !subseteq AC^0[6]. These results are complemented by lower bounds for Gap-MCSP and Gap-MKtP against different models. For instance, the lower bound assumed in (1) holds for U_2-formulas of near-quadratic size, and lower bounds similar to (3)-(5) hold for various regimes of parameters. We also identify a natural computational model under which the hardness magnification threshold for Gap-MKtP lies below existing lower bounds: U_2-formulas that can compute parity functions at the leaves (instead of just literals). As a consequence, if one managed to adapt the existing lower bound techniques against such formulas to work with Gap-MKtP, then EXP !subseteq NC^1 would follow via hardness magnification.
Cite as

Igor Carboni Oliveira, Ján Pich, and Rahul Santhanam. Hardness Magnification near State-Of-The-Art Lower Bounds. In 34th Computational Complexity Conference (CCC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 137, pp. 27:1-27:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{oliveira_et_al:LIPIcs.CCC.2019.27,
  author =	{Oliveira, Igor Carboni and Pich, J\'{a}n and Santhanam, Rahul},
  title =	{{Hardness Magnification near State-Of-The-Art Lower Bounds}},
  booktitle =	{34th Computational Complexity Conference (CCC 2019)},
  pages =	{27:1--27:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-116-0},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{137},
  editor =	{Shpilka, Amir},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2019.27},
  URN =		{urn:nbn:de:0030-drops-108494},
  doi =		{10.4230/LIPIcs.CCC.2019.27},
  annote =	{Keywords: Circuit Complexity, Minimum Circuit Size Problem, Kolmogorov Complexity}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2019.32
Randomness and Intractability in Kolmogorov Complexity

Authors: Igor Carboni Oliveira

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract
We introduce randomized time-bounded Kolmogorov complexity (rKt), a natural extension of Levin’s notion [Leonid A. Levin, 1984] of Kolmogorov complexity. A string w of low rKt complexity can be decompressed from a short representation via a time-bounded algorithm that outputs w with high probability. This complexity measure gives rise to a decision problem over strings: MrKtP (The Minimum rKt Problem). We explore ideas from pseudorandomness to prove that MrKtP and its variants cannot be solved in randomized quasi-polynomial time. This exhibits a natural string compression problem that is provably intractable, even for randomized computations. Our techniques also imply that there is no n^{1 - epsilon}-approximate algorithm for MrKtP running in randomized quasi-polynomial time. Complementing this lower bound, we observe connections between rKt, the power of randomness in computing, and circuit complexity. In particular, we present the first hardness magnification theorem for a natural problem that is unconditionally hard against a strong model of computation.
Cite as

Igor Carboni Oliveira. Randomness and Intractability in Kolmogorov Complexity. In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 32:1-32:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{oliveira:LIPIcs.ICALP.2019.32,
  author =	{Oliveira, Igor Carboni},
  title =	{{Randomness and Intractability in Kolmogorov Complexity}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{32:1--32:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.32},
  URN =		{urn:nbn:de:0030-drops-106087},
  doi =		{10.4230/LIPIcs.ICALP.2019.32},
  annote =	{Keywords: computational complexity, randomness, circuit lower bounds, Kolmogorov complexity}
}
Document
DOI: 10.4230/LIPIcs.CCC.2015.124
Majority is Incompressible by AC^0[p] Circuits

Authors: Igor Carboni Oliveira and Rahul Santhanam

Published in: LIPIcs, Volume 33, 30th Conference on Computational Complexity (CCC 2015)

Abstract
We consider C-compression games, a hybrid model between computational and communication complexity. A C-compression game for a function f:{0,1}^n -> {0,1} is a two-party communication game, where the first party Alice knows the entire input x but is restricted to use strategies computed by C-circuits, while the second party Bob initially has no information about the input, but is computationally unbounded. The parties implement an interactive communication protocol to decide the value of f(x), and the communication cost of the protocol is the maximum number of bits sent by Alice as a function of n = |x|. We show that any AC_d[p]-compression protocol to compute Majority_n requires communication n / (log(n))^(2d + O(1)), where p is prime, and AC_d[p] denotes polynomial size unbounded fan-in depth-d Boolean circuits extended with modulo p gates. This bound is essentially optimal, and settles a question of Chattopadhyay and Santhanam (2012). This result has a number of consequences, and yields a tight lower bound on the total fan-in of oracle gates in constant-depth oracle circuits computing Majority_n. We define multiparty compression games, where Alice interacts in parallel with a polynomial number of players that are not allowed to communicate with each other, and communication cost is defined as the sum of the lengths of the longest messages sent by Alice during each round. In this setting, we prove that the randomized r-round AC^0[p]-compression cost of Majority_n is n^(Theta(1/r)). This result implies almost tight lower bounds on the maximum individual fan-in of oracle gates in certain restricted bounded-depth oracle circuits computing Majority_n. Stronger lower bounds for functions in NP would separate NP from NC^1. Finally, we consider the round separation question for two-party AC-compression games, and significantly improve known separations between r-round and (r+1)-round protocols, for any constant r.
Cite as

Igor Carboni Oliveira and Rahul Santhanam. Majority is Incompressible by AC^0[p] Circuits. In 30th Conference on Computational Complexity (CCC 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 33, pp. 124-157, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{oliveira_et_al:LIPIcs.CCC.2015.124,
  author =	{Oliveira, Igor Carboni and Santhanam, Rahul},
  title =	{{Majority is Incompressible by AC^0\lbrackp\rbrack Circuits}},
  booktitle =	{30th Conference on Computational Complexity (CCC 2015)},
  pages =	{124--157},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-81-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{33},
  editor =	{Zuckerman, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2015.124},
  URN =		{urn:nbn:de:0030-drops-50658},
  doi =		{10.4230/LIPIcs.CCC.2015.124},
  annote =	{Keywords: interactive communication, compression, circuit lower bound}
}

Oliveira, Rafael

Document
DOI: 10.4230/LIPIcs.CCC.2023.20
Radical Sylvester-Gallai Theorem for Tuples of Quadratics

Authors: Abhibhav Garg, Rafael Oliveira, Shir Peleg, and Akash Kumar Sengupta

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

Abstract
We prove a higher codimensional radical Sylvester-Gallai type theorem for quadratic polynomials, simultaneously generalizing [Hansen, 1965; Shpilka, 2020]. Hansen’s theorem is a high-dimensional version of the classical Sylvester-Gallai theorem in which the incidence condition is given by high-dimensional flats instead of lines. We generalize Hansen’s theorem to the setting of quadratic forms in a polynomial ring, where the incidence condition is given by radical membership in a high-codimensional ideal. Our main theorem is also a generalization of the quadratic Sylvester-Gallai Theorem of [Shpilka, 2020]. Our work is the first to prove a radical Sylvester-Gallai type theorem for arbitrary codimension k ≥ 2, whereas previous works [Shpilka, 2020; Shir Peleg and Amir Shpilka, 2020; Shir Peleg and Amir Shpilka, 2021; Garg et al., 2022] considered the case of codimension 2 ideals. Our techniques combine algebraic geometric and combinatorial arguments. A key ingredient is a structural result for ideals generated by a constant number of quadratics, showing that such ideals must be radical whenever the quadratic forms are far apart. Using the wide algebras defined in [Garg et al., 2022], combined with results about integral ring extensions and dimension theory, we develop new techniques for studying such ideals generated by quadratic forms. One advantage of our approach is that it does not need the finer classification theorems for codimension 2 complete intersection of quadratics proved in [Shpilka, 2020; Garg et al., 2022].
Cite as

Abhibhav Garg, Rafael Oliveira, Shir Peleg, and Akash Kumar Sengupta. Radical Sylvester-Gallai Theorem for Tuples of Quadratics. In 38th Computational Complexity Conference (CCC 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 264, pp. 20:1-20:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{garg_et_al:LIPIcs.CCC.2023.20,
  author =	{Garg, Abhibhav and Oliveira, Rafael and Peleg, Shir and Sengupta, Akash Kumar},
  title =	{{Radical Sylvester-Gallai Theorem for Tuples of Quadratics}},
  booktitle =	{38th Computational Complexity Conference (CCC 2023)},
  pages =	{20:1--20:30},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2023.20},
  URN =		{urn:nbn:de:0030-drops-182903},
  doi =		{10.4230/LIPIcs.CCC.2023.20},
  annote =	{Keywords: Sylvester-Gallai theorem, arrangements of hypersurfaces, algebraic complexity, polynomial identity testing, algebraic geometry, commutative algebra}
}
Document
DOI: 10.4230/LIPIcs.SoCG.2022.42
Robust Radical Sylvester-Gallai Theorem for Quadratics

Authors: Abhibhav Garg, Rafael Oliveira, and Akash Kumar Sengupta

Published in: LIPIcs, Volume 224, 38th International Symposium on Computational Geometry (SoCG 2022)

Abstract
We prove a robust generalization of a Sylvester-Gallai type theorem for quadratic polynomials. More precisely, given a parameter 0 < δ ≤ 1 and a finite collection ℱ of irreducible and pairwise independent polynomials of degree at most 2, we say that ℱ is a (δ, 2)-radical Sylvester-Gallai configuration if for any polynomial F_i ∈ ℱ, there exist δ(|ℱ|-1) polynomials F_j such that |rad (F_i, F_j) ∩ ℱ| ≥ 3, that is, the radical of F_i, F_j contains a third polynomial in the set. We prove that any (δ, 2)-radical Sylvester-Gallai configuration ℱ must be of low dimension: that is dim span_ℂ{ℱ} = poly(1/δ).
Cite as

Abhibhav Garg, Rafael Oliveira, and Akash Kumar Sengupta. Robust Radical Sylvester-Gallai Theorem for Quadratics. In 38th International Symposium on Computational Geometry (SoCG 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 224, pp. 42:1-42:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{garg_et_al:LIPIcs.SoCG.2022.42,
  author =	{Garg, Abhibhav and Oliveira, Rafael and Sengupta, Akash Kumar},
  title =	{{Robust Radical Sylvester-Gallai Theorem for Quadratics}},
  booktitle =	{38th International Symposium on Computational Geometry (SoCG 2022)},
  pages =	{42:1--42:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-227-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{224},
  editor =	{Goaoc, Xavier and Kerber, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SoCG.2022.42},
  URN =		{urn:nbn:de:0030-drops-160505},
  doi =		{10.4230/LIPIcs.SoCG.2022.42},
  annote =	{Keywords: Sylvester-Gallai theorem, arrangements of hypersurfaces, locally correctable codes, algebraic complexity, polynomial identity testing, algebraic geometry, commutative algebra}
}
Document
DOI: 10.4230/LIPIcs.CCC.2020.12
Search Problems in Algebraic Complexity, GCT, and Hardness of Generators for Invariant Rings

Authors: Ankit Garg, Christian Ikenmeyer, Visu Makam, Rafael Oliveira, Michael Walter, and Avi Wigderson

Published in: LIPIcs, Volume 169, 35th Computational Complexity Conference (CCC 2020)

Abstract
We consider the problem of computing succinct encodings of lists of generators for invariant rings for group actions. Mulmuley conjectured that there are always polynomial sized such encodings for invariant rings of SL_n(ℂ)-representations. We provide simple examples that disprove this conjecture (under standard complexity assumptions). We develop a general framework, denoted algebraic circuit search problems, that captures many important problems in algebraic complexity and computational invariant theory. This framework encompasses various proof systems in proof complexity and some of the central problems in invariant theory as exposed by the Geometric Complexity Theory (GCT) program, including the aforementioned problem of computing succinct encodings for generators for invariant rings.
Cite as

Ankit Garg, Christian Ikenmeyer, Visu Makam, Rafael Oliveira, Michael Walter, and Avi Wigderson. Search Problems in Algebraic Complexity, GCT, and Hardness of Generators for Invariant Rings. In 35th Computational Complexity Conference (CCC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 169, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{garg_et_al:LIPIcs.CCC.2020.12,
  author =	{Garg, Ankit and Ikenmeyer, Christian and Makam, Visu and Oliveira, Rafael and Walter, Michael and Wigderson, Avi},
  title =	{{Search Problems in Algebraic Complexity, GCT, and Hardness of Generators for Invariant Rings}},
  booktitle =	{35th Computational Complexity Conference (CCC 2020)},
  pages =	{12:1--12:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-156-6},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{169},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2020.12},
  URN =		{urn:nbn:de:0030-drops-125645},
  doi =		{10.4230/LIPIcs.CCC.2020.12},
  annote =	{Keywords: generators for invariant rings, succinct encodings}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2019.78
Towards Optimal Depth Reductions for Syntactically Multilinear Circuits

Authors: Mrinal Kumar, Rafael Oliveira, and Ramprasad Saptharishi

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract
We show that any n-variate polynomial computable by a syntactically multilinear circuit of size poly(n) can be computed by a depth-4 syntactically multilinear (Sigma Pi Sigma Pi) circuit of size at most exp ({O (sqrt{n log n})}). For degree d = omega(n/log n), this improves upon the upper bound of exp ({O(sqrt{d}log n)}) obtained by Tavenas [Sébastien Tavenas, 2015] for general circuits, and is known to be asymptotically optimal in the exponent when d < n^{epsilon} for a small enough constant epsilon. Our upper bound matches the lower bound of exp ({Omega (sqrt{n log n})}) proved by Raz and Yehudayoff [Ran Raz and Amir Yehudayoff, 2009], and thus cannot be improved further in the exponent. Our results hold over all fields and also generalize to circuits of small individual degree. More generally, we show that an n-variate polynomial computable by a syntactically multilinear circuit of size poly(n) can be computed by a syntactically multilinear circuit of product-depth Delta of size at most exp inparen{O inparen{Delta * (n/log n)^{1/Delta} * log n}}. It follows from the lower bounds of Raz and Yehudayoff [Ran Raz and Amir Yehudayoff, 2009] that in general, for constant Delta, the exponent in this upper bound is tight and cannot be improved to o inparen{inparen{n/log n}^{1/Delta}* log n}.
Cite as

Mrinal Kumar, Rafael Oliveira, and Ramprasad Saptharishi. Towards Optimal Depth Reductions for Syntactically Multilinear Circuits. In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 78:1-78:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kumar_et_al:LIPIcs.ICALP.2019.78,
  author =	{Kumar, Mrinal and Oliveira, Rafael and Saptharishi, Ramprasad},
  title =	{{Towards Optimal Depth Reductions for Syntactically Multilinear Circuits}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{78:1--78:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.78},
  URN =		{urn:nbn:de:0030-drops-106548},
  doi =		{10.4230/LIPIcs.ICALP.2019.78},
  annote =	{Keywords: arithmetic circuits, multilinear circuits, depth reduction, lower bounds}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2018.1
Barriers for Rank Methods in Arithmetic Complexity

Authors: Klim Efremenko, Ankit Garg, Rafael Oliveira, and Avi Wigderson

Published in: LIPIcs, Volume 94, 9th Innovations in Theoretical Computer Science Conference (ITCS 2018)

Abstract
Arithmetic complexity, the study of the cost of computing polynomials via additions and multiplications, is considered (for many good reasons) simpler to understand than Boolean complexity, namely computing Boolean functions via logical gates. And indeed, we seem to have significantly more lower bound techniques and results in arithmetic complexity than in Boolean complexity. Despite many successes and rapid progress, however, foundational challenges, like proving super-polynomial lower bounds on circuit or formula size for explicit polynomials, or super-linear lower bounds on explicit 3-dimensional tensors, remain elusive. At the same time (and possibly for similar reasons), we have plenty more excuses, in the form of "barrier results" for failing to prove basic lower bounds in Boolean complexity than in arithmetic complexity. Efforts to find barriers to arithmetic lower bound techniques seem harder, and despite some attempts we have no excuses of similar quality for these failures in arithmetic complexity. This paper aims to add to this study. In this paper we address rank methods, which were long recognized as encompassing and abstracting almost all known arithmetic lower bounds to-date, including the most recent impressive successes. Rank methods (under the name of flattenings) are also in wide use in algebraic geometry for proving tensor rank and symmetric tensor rank lower bounds. Our main results are barriers to these methods. In particular, 1. Rank methods cannot prove better than (2^d)*n^(d/2) lower bound on the tensor rank of any d-dimensional tensor of side n. (In particular, they cannot prove super-linear, indeed even >8n tensor rank lower bounds for any 3-dimensional tensors.) 2. Rank methods cannot prove (d+1)n^(d/2) on the Waring rank of any n-variate polynomial of degree d. (In particular, they cannot prove such lower bounds on stronger models, including depth-3 circuits.) The proofs of these bounds use simple linear-algebraic arguments, leveraging connections between the symbolic rank of matrix polynomials and the usual rank of their evaluations. These techniques can perhaps be extended to barriers for other arithmetic models on which progress has halted. To see how these barrier results directly inform the state-of-art in arithmetic complexity we note the following. First, the bounds above nearly match the best explicit bounds we know for these models, hence offer an explanations why the rank methods got stuck there. Second, the bounds above are a far cry (quadratically away) from the true complexity (e.g. of random polynomials) in these models, which if achieved (by any methods), are known to imply super-polynomial formula lower bounds. We also explain the relation of our barrier results to other attempts, and in particular how they significantly differ from the recent attempts to find analogues of "natural proofs" for arithmetic complexity. Finally, we discuss the few arithmetic lower bound approaches which fall outside rank methods, and some natural directions our barriers suggest.
Cite as

Klim Efremenko, Ankit Garg, Rafael Oliveira, and Avi Wigderson. Barriers for Rank Methods in Arithmetic Complexity. In 9th Innovations in Theoretical Computer Science Conference (ITCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 94, pp. 1:1-1:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{efremenko_et_al:LIPIcs.ITCS.2018.1,
  author =	{Efremenko, Klim and Garg, Ankit and Oliveira, Rafael and Wigderson, Avi},
  title =	{{Barriers for Rank Methods in Arithmetic Complexity}},
  booktitle =	{9th Innovations in Theoretical Computer Science Conference (ITCS 2018)},
  pages =	{1:1--1:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-060-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{94},
  editor =	{Karlin, Anna R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2018.1},
  URN =		{urn:nbn:de:0030-drops-83506},
  doi =		{10.4230/LIPIcs.ITCS.2018.1},
  annote =	{Keywords: Lower Bounds, Barriers, Partial Derivatives, Flattenings, Algebraic Complexity}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2018.24
Alternating Minimization, Scaling Algorithms, and the Null-Cone Problem from Invariant Theory

Authors: Peter Bürgisser, Ankit Garg, Rafael Oliveira, Michael Walter, and Avi Wigderson

Published in: LIPIcs, Volume 94, 9th Innovations in Theoretical Computer Science Conference (ITCS 2018)

Abstract
Alternating minimization heuristics seek to solve a (difficult) global optimization task through iteratively solving a sequence of (much easier) local optimization tasks on different parts (or blocks) of the input parameters. While popular and widely applicable, very few examples of this heuristic are rigorously shown to converge to optimality, and even fewer to do so efficiently. In this paper we present a general framework which is amenable to rigorous analysis, and expose its applicability. Its main feature is that the local optimization domains are each a group of invertible matrices, together naturally acting on tensors, and the optimization problem is minimizing the norm of an input tensor under this joint action. The solution of this optimization problem captures a basic problem in Invariant Theory, called the null-cone problem. This algebraic framework turns out to encompass natural computational problems in combinatorial optimization, algebra, analysis, quantum information theory, and geometric complexity theory. It includes and extends to high dimensions the recent advances on (2-dimensional) operator scaling. Our main result is a fully polynomial time approximation scheme for this general problem, which may be viewed as a multi-dimensional scaling algorithm. This directly leads to progress on some of the problems in the areas above, and a unified view of others. We explain how faster convergence of an algorithm for the same problem will allow resolving central open problems. Our main techniques come from Invariant Theory, and include its rich non-commutative duality theory, and new bounds on the bitsizes of coefficients of invariant polynomials. They enrich the algorithmic toolbox of this very computational field of mathematics, and are directly related to some challenges in geometric complexity theory (GCT).
Cite as

Peter Bürgisser, Ankit Garg, Rafael Oliveira, Michael Walter, and Avi Wigderson. Alternating Minimization, Scaling Algorithms, and the Null-Cone Problem from Invariant Theory. In 9th Innovations in Theoretical Computer Science Conference (ITCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 94, pp. 24:1-24:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{burgisser_et_al:LIPIcs.ITCS.2018.24,
  author =	{B\"{u}rgisser, Peter and Garg, Ankit and Oliveira, Rafael and Walter, Michael and Wigderson, Avi},
  title =	{{Alternating Minimization, Scaling Algorithms, and the Null-Cone Problem from Invariant Theory}},
  booktitle =	{9th Innovations in Theoretical Computer Science Conference (ITCS 2018)},
  pages =	{24:1--24:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-060-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{94},
  editor =	{Karlin, Anna R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2018.24},
  URN =		{urn:nbn:de:0030-drops-83510},
  doi =		{10.4230/LIPIcs.ITCS.2018.24},
  annote =	{Keywords: alternating minimization, tensors, scaling, quantum marginal problem, null cone, invariant theory, geometric complexity theory}
}
Document
DOI: 10.4230/LIPIcs.CCC.2015.198
Factors of Low Individual Degree Polynomials

Authors: Rafael Oliveira

Published in: LIPIcs, Volume 33, 30th Conference on Computational Complexity (CCC 2015)

Abstract
In [Kaltofen, 1989], Kaltofen proved the remarkable fact that multivariate polynomial factorization can be done efficiently, in randomized polynomial time. Still, more than twenty years after Kaltofen's work, many questions remain unanswered regarding the complexity aspects of polynomial factorization, such as the question of whether factors of polynomials efficiently computed by arithmetic formulas also have small arithmetic formulas, asked in [Kopparty/Saraf/Shpilka,CCC'14], and the question of bounding the depth of the circuits computing the factors of a polynomial. We are able to answer these questions in the affirmative for the interesting class of polynomials of bounded individual degrees, which contains polynomials such as the determinant and the permanent. We show that if P(x_1, ..., x_n) is a polynomial with individual degrees bounded by r that can be computed by a formula of size s and depth d, then any factor f(x_1, ..., x_n) of P(x_1, ..., x_n) can be computed by a formula of size poly((rn)^r, s) and depth d+5. This partially answers the question above posed in [Kopparty/Saraf/Shpilka,CCC'14], that asked if this result holds without the exponential dependence on r. Our work generalizes the main factorization theorem from Dvir et al. [Dvir/Shpilka/Yehudayoff,SIAM J. Comp., 2009], who proved it for the special case when the factors are of the form f(x_1, ..., x_n) = x_n - g(x_1, ..., x_n-1). Along the way, we introduce several new technical ideas that could be of independent interest when studying arithmetic circuits (or formulas).
Cite as

Rafael Oliveira. Factors of Low Individual Degree Polynomials. In 30th Conference on Computational Complexity (CCC 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 33, pp. 198-216, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{oliveira:LIPIcs.CCC.2015.198,
  author =	{Oliveira, Rafael},
  title =	{{Factors of Low Individual Degree Polynomials}},
  booktitle =	{30th Conference on Computational Complexity (CCC 2015)},
  pages =	{198--216},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-81-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{33},
  editor =	{Zuckerman, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2015.198},
  URN =		{urn:nbn:de:0030-drops-50594},
  doi =		{10.4230/LIPIcs.CCC.2015.198},
  annote =	{Keywords: Arithmetic Circuits, Factoring, Algebraic Complexity}
}
Document
DOI: 10.4230/LIPIcs.CCC.2015.304
Subexponential Size Hitting Sets for Bounded Depth Multilinear Formulas

Authors: Rafael Oliveira, Amir Shpilka, and Ben Lee Volk

Published in: LIPIcs, Volume 33, 30th Conference on Computational Complexity (CCC 2015)

Abstract
In this paper we give subexponential size hitting sets for bounded depth multilinear arithmetic formulas. Using the known relation between black-box PIT and lower bounds we obtain lower bounds for these models. For depth-3 multilinear formulas, of size exp(n^delta), we give a hitting set of size exp(~O(n^(2/3 + 2*delta/3))). This implies a lower bound of exp(~Omega(n^(1/2))) for depth-3 multilinear formulas, for some explicit polynomial. For depth-4 multilinear formulas, of size exp(n^delta), we give a hitting set of size exp(~O(n^(2/3 + 4*delta/3)). This implies a lower bound of exp(~Omega(n^(1/4))) for depth-4 multilinear formulas, for some explicit polynomial. A regular formula consists of alternating layers of +,* gates, where all gates at layer i have the same fan-in. We give a hitting set of size (roughly) exp(n^(1-delta)), for regular depth-d multilinear formulas of size exp(n^delta), where delta = O(1/sqrt(5)^d)). This result implies a lower bound of roughly exp(~Omega(n^(1/sqrt(5)^d))) for such formulas. We note that better lower bounds are known for these models, but also that none of these bounds was achieved via construction of a hitting set. Moreover, no lower bound that implies such PIT results, even in the white-box model, is currently known. Our results are combinatorial in nature and rely on reducing the underlying formula, first to a depth-4 formula, and then to a read-once algebraic branching program (from depth-3 formulas we go straight to read-once algebraic branching programs).
Cite as

Rafael Oliveira, Amir Shpilka, and Ben Lee Volk. Subexponential Size Hitting Sets for Bounded Depth Multilinear Formulas. In 30th Conference on Computational Complexity (CCC 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 33, pp. 304-322, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{oliveira_et_al:LIPIcs.CCC.2015.304,
  author =	{Oliveira, Rafael and Shpilka, Amir and Volk, Ben Lee},
  title =	{{Subexponential Size Hitting Sets for Bounded Depth Multilinear Formulas}},
  booktitle =	{30th Conference on Computational Complexity (CCC 2015)},
  pages =	{304--322},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-81-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{33},
  editor =	{Zuckerman, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2015.304},
  URN =		{urn:nbn:de:0030-drops-50548},
  doi =		{10.4230/LIPIcs.CCC.2015.304},
  annote =	{Keywords: Arithmetic Circuits, Derandomization, Polynomial Identity Testing}
}

Oliveira, Igor C.

Document
DOI: 10.4230/LIPIcs.CCC.2024.29
Exact Search-To-Decision Reductions for Time-Bounded Kolmogorov Complexity

Authors: Shuichi Hirahara, Valentine Kabanets, Zhenjian Lu, and Igor C. Oliveira

Published in: LIPIcs, Volume 300, 39th Computational Complexity Conference (CCC 2024)

Abstract
A search-to-decision reduction is a procedure that allows one to find a solution to a problem from the mere ability to decide when a solution exists. The existence of a search-to-decision reduction for time-bounded Kolmogorov complexity, i.e., the problem of checking if a string x can be generated by a t-time bounded program of description length s, is a long-standing open problem that dates back to the 1960s. In this work, we obtain new average-case and worst-case search-to-decision reductions for the complexity measure 𝖪^t and its randomized analogue rK^t: 1) (Conditional Errorless and Error-Prone Reductions for 𝖪^t) Under the assumption that 𝖤 requires exponential size circuits, we design polynomial-time average-case search-to-decision reductions for 𝖪^t in both errorless and error-prone settings. In fact, under the easiness of deciding 𝖪^t under the uniform distribution, we obtain a search algorithm for any given polynomial-time samplable distribution. In the error-prone reduction, the search algorithm works in the more general setting of conditional 𝖪^t complexity, i.e., it finds a minimum length t-time bound program for generating x given a string y. 2) (Unconditional Errorless Reduction for rK^t) We obtain an unconditional polynomial-time average-case search-to-decision reduction for rK^t in the errorless setting. Similarly to the results described above, we obtain a search algorithm for each polynomial-time samplable distribution, assuming the existence of a decision algorithm under the uniform distribution. To our knowledge, this is the first unconditional sub-exponential time search-to-decision reduction among the measures 𝖪^t and rK^t that works with respect to any given polynomial-time samplable distribution. 3) (Worst-Case to Average-Case Reductions) Under the errorless average-case easiness of deciding rK^t, we design a worst-case search algorithm running in time 2^O(n/log n) that produces a minimum length randomized t-time program for every input string x ∈ {0,1}ⁿ, with the caveat that it only succeeds on some explicitly computed sub-exponential time bound t ≤ 2^{n^ε} that depends on x. A similar result holds for 𝖪^t, under the assumption that 𝖤 requires exponential size circuits. In these results, the corresponding search problem is solved exactly, i.e., a successful run of the search algorithm outputs a t-time bounded program for x of minimum length, as opposed to an approximately optimal program of slightly larger description length or running time.
Cite as

Shuichi Hirahara, Valentine Kabanets, Zhenjian Lu, and Igor C. Oliveira. Exact Search-To-Decision Reductions for Time-Bounded Kolmogorov Complexity. In 39th Computational Complexity Conference (CCC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 300, pp. 29:1-29:56, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{hirahara_et_al:LIPIcs.CCC.2024.29,
  author =	{Hirahara, Shuichi and Kabanets, Valentine and Lu, Zhenjian and Oliveira, Igor C.},
  title =	{{Exact Search-To-Decision Reductions for Time-Bounded Kolmogorov Complexity}},
  booktitle =	{39th Computational Complexity Conference (CCC 2024)},
  pages =	{29:1--29:56},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-331-7},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{300},
  editor =	{Santhanam, Rahul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2024.29},
  URN =		{urn:nbn:de:0030-drops-204256},
  doi =		{10.4230/LIPIcs.CCC.2024.29},
  annote =	{Keywords: average-case complexity, Kolmogorov complexity, search-to-decision reductions}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.STACS.2024.1
Polynomial-Time Pseudodeterministic Constructions (Invited Talk)

Authors: Igor C. Oliveira

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
A randomised algorithm for a search problem is pseudodeterministic if it produces a fixed canonical solution to the search problem with high probability. In their seminal work on the topic, Gat and Goldwasser (2011) posed as their main open problem whether prime numbers can be pseudodeterministically constructed in polynomial time. We provide a positive solution to this question in the infinitely-often regime. In more detail, we give an unconditional polynomial-time randomised algorithm B such that, for infinitely many values of n, B(1ⁿ) outputs a canonical n-bit prime p_n with high probability. More generally, we prove that for every dense property Q of strings that can be decided in polynomial time, there is an infinitely-often pseudodeterministic polynomial-time construction of strings satisfying Q. This improves upon a subexponential-time pseudodeterministic construction of Oliveira and Santhanam (2017). This talk will cover the main ideas behind these constructions and discuss their implications, such as the existence of infinitely many primes with succinct and efficient representations.
Cite as

Igor C. Oliveira. Polynomial-Time Pseudodeterministic Constructions (Invited Talk). In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{oliveira:LIPIcs.STACS.2024.1,
  author =	{Oliveira, Igor C.},
  title =	{{Polynomial-Time Pseudodeterministic Constructions}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{1:1--1:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.1},
  URN =		{urn:nbn:de:0030-drops-197112},
  doi =		{10.4230/LIPIcs.STACS.2024.1},
  annote =	{Keywords: Pseudorandomness, Explicit Constructions, Pseudodeterministic Algorithms}
}
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.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
DOI: 10.4230/LIPIcs.CCC.2022.16
Probabilistic Kolmogorov Complexity with Applications to Average-Case Complexity

Authors: Halley Goldberg, Valentine Kabanets, Zhenjian Lu, and Igor C. Oliveira

Published in: LIPIcs, Volume 234, 37th Computational Complexity Conference (CCC 2022)

Abstract
Understanding the relationship between the worst-case and average-case complexities of NP and of other subclasses of PH is a long-standing problem in complexity theory. Over the last few years, much progress has been achieved in this front through the investigation of meta-complexity: the complexity of problems that refer to the complexity of the input string x (e.g., given a string x, estimate its time-bounded Kolmogorov complexity). In particular, [Shuichi Hirahara, 2021] employed techniques from meta-complexity to show that if DistNP ⊆ AvgP then UP ⊆ DTIME[2^{O(n/log n)}]. While this and related results [Shuichi Hirahara and Mikito Nanashima, 2021; Lijie Chen et al., 2022] offer exciting progress after a long gap, they do not survive in the setting of randomized computations: roughly speaking, "randomness" is the opposite of "structure", and upper bounding the amount of structure (time-bounded Kolmogorov complexity) of different objects is crucial in recent applications of meta-complexity. This limitation is significant, since randomized computations are ubiquitous in algorithm design and give rise to a more robust theory of average-case complexity [Russell Impagliazzo and Leonid A. Levin, 1990]. In this work, we develop a probabilistic theory of meta-complexity, by incorporating randomness into the notion of complexity of a string x. This is achieved through a new probabilistic variant of time-bounded Kolmogorov complexity that we call pK^t complexity. Informally, pK^t(x) measures the complexity of x when shared randomness is available to all parties involved in a computation. By porting key results from meta-complexity to the probabilistic domain of pK^t complexity and its variants, we are able to establish new connections between worst-case and average-case complexity in the important setting of probabilistic computations: - If DistNP ⊆ AvgBPP, then UP ⊆ RTIME[2^O(n/log n)]. - If DistΣ^P_2 ⊆ AvgBPP, then AM ⊆ BPTIME[2^O(n/log n)]. - In the fine-grained setting [Lijie Chen et al., 2022], we get UTIME[2^O(√{nlog n})] ⊆ RTIME[2^O(√{nlog n})] and AMTIME[2^O(√{nlog n})] ⊆ BPTIME[2^O(√{nlog n})] from stronger average-case assumptions. - If DistPH ⊆ AvgBPP, then PH ⊆ BPTIME[2^O(n/log n)]. Specifically, for any 𝓁 ≥ 0, if DistΣ_{𝓁+2}^P ⊆ AvgBPP then Σ_𝓁^{P} ⊆ BPTIME[2^O(n/log n)]. - Strengthening a result from [Shuichi Hirahara and Mikito Nanashima, 2021], we show that if DistNP ⊆ AvgBPP then polynomial size Boolean circuits can be agnostically PAC learned under any unknown 𝖯/poly-samplable distribution in polynomial time. In some cases, our framework allows us to significantly simplify existing proofs, or to extend results to the more challenging probabilistic setting with little to no extra effort.
Cite as

Halley Goldberg, Valentine Kabanets, Zhenjian Lu, and Igor C. Oliveira. Probabilistic Kolmogorov Complexity with Applications to Average-Case Complexity. In 37th Computational Complexity Conference (CCC 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 234, pp. 16:1-16:60, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{goldberg_et_al:LIPIcs.CCC.2022.16,
  author =	{Goldberg, Halley and Kabanets, Valentine and Lu, Zhenjian and Oliveira, Igor C.},
  title =	{{Probabilistic Kolmogorov Complexity with Applications to Average-Case Complexity}},
  booktitle =	{37th Computational Complexity Conference (CCC 2022)},
  pages =	{16:1--16:60},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-241-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{234},
  editor =	{Lovett, Shachar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2022.16},
  URN =		{urn:nbn:de:0030-drops-165785},
  doi =		{10.4230/LIPIcs.CCC.2022.16},
  annote =	{Keywords: average-case complexity, Kolmogorov complexity, meta-complexity, worst-case to average-case reductions, learning}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2022.92
Optimal Coding Theorems in Time-Bounded Kolmogorov Complexity

Authors: Zhenjian Lu, Igor C. Oliveira, and Marius Zimand

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)

Abstract
The classical coding theorem in Kolmogorov complexity states that if an n-bit string x is sampled with probability δ by an algorithm with prefix-free domain then 𝖪(x) ≤ log(1/δ) + O(1). In a recent work, Lu and Oliveira [Zhenjian Lu and Igor C. Oliveira, 2021] established an unconditional time-bounded version of this result, by showing that if x can be efficiently sampled with probability δ then rKt(x) = O(log(1/δ)) + O(log n), where rKt denotes the randomized analogue of Levin’s Kt complexity. Unfortunately, this result is often insufficient when transferring applications of the classical coding theorem to the time-bounded setting, as it achieves a O(log(1/δ)) bound instead of the information-theoretic optimal log(1/δ). Motivated by this discrepancy, we investigate optimal coding theorems in the time-bounded setting. Our main contributions can be summarised as follows. • Efficient coding theorem for rKt with a factor of 2. Addressing a question from [Zhenjian Lu and Igor C. Oliveira, 2021], we show that if x can be efficiently sampled with probability at least δ then rKt(x) ≤ (2 + o(1)) ⋅ log(1/δ) + O(log n). As in previous work, our coding theorem is efficient in the sense that it provides a polynomial-time probabilistic algorithm that, when given x, the code of the sampler, and δ, it outputs, with probability ≥ 0.99, a probabilistic representation of x that certifies this rKt complexity bound. • Optimality under a cryptographic assumption. Under a hypothesis about the security of cryptographic pseudorandom generators, we show that no efficient coding theorem can achieve a bound of the form rKt(x) ≤ (2 - o(1)) ⋅ log(1/δ) + poly(log n). Under a weaker assumption, we exhibit a gap between efficient coding theorems and existential coding theorems with near-optimal parameters. • Optimal coding theorem for pK^t and unconditional Antunes-Fortnow. We consider pK^t complexity [Halley Goldberg et al., 2022], a variant of rKt where the randomness is public and the time bound is fixed. We observe the existence of an optimal coding theorem for pK^t, and employ this result to establish an unconditional version of a theorem of Antunes and Fortnow [Luis Filipe Coelho Antunes and Lance Fortnow, 2009] which characterizes the worst-case running times of languages that are in average polynomial-time over all 𝖯-samplable distributions.
Cite as

Zhenjian Lu, Igor C. Oliveira, and Marius Zimand. Optimal Coding Theorems in Time-Bounded Kolmogorov Complexity. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 92:1-92:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{lu_et_al:LIPIcs.ICALP.2022.92,
  author =	{Lu, Zhenjian and Oliveira, Igor C. and Zimand, Marius},
  title =	{{Optimal Coding Theorems in Time-Bounded Kolmogorov Complexity}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{92:1--92:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.92},
  URN =		{urn:nbn:de:0030-drops-164331},
  doi =		{10.4230/LIPIcs.ICALP.2022.92},
  annote =	{Keywords: computational complexity, randomized algorithms, Kolmogorov complexity}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2021.51
Majority vs. Approximate Linear Sum and Average-Case Complexity Below NC¹

Authors: Lijie Chen, Zhenjian Lu, Xin Lyu, and Igor C. Oliveira

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
We develop a general framework that characterizes strong average-case lower bounds against circuit classes 𝒞 contained in NC¹, such as AC⁰[⊕] and ACC⁰. We apply this framework to show: - Generic seed reduction: Pseudorandom generators (PRGs) against 𝒞 of seed length ≤ n -1 and error ε(n) = n^{-ω(1)} can be converted into PRGs of sub-polynomial seed length. - Hardness under natural distributions: If 𝖤 (deterministic exponential time) is average-case hard against 𝒞 under some distribution, then 𝖤 is average-case hard against 𝒞 under the uniform distribution. - Equivalence between worst-case and average-case hardness: Worst-case lower bounds against MAJ∘𝒞 for problems in 𝖤 are equivalent to strong average-case lower bounds against 𝒞. This can be seen as a certain converse to the Discriminator Lemma [Hajnal et al., JCSS'93]. These results were not known to hold for circuit classes that do not compute majority. Additionally, we prove that classical and recent approaches to worst-case lower bounds against ACC⁰ via communication lower bounds for NOF multi-party protocols [Håstad and Goldmann, CC'91; Razborov and Wigderson, IPL'93] and Torus polynomials degree lower bounds [Bhrushundi et al., ITCS'19] also imply strong average-case hardness against ACC⁰ under the uniform distribution. Crucial to these results is the use of non-black-box hardness amplification techniques and the interplay between Majority (MAJ) and Approximate Linear Sum (SUM̃) gates. Roughly speaking, while a MAJ gate outputs 1 when the sum of the m input bits is at least m/2, a SUM̃ gate computes a real-valued bounded weighted sum of the input bits and outputs 1 (resp. 0) if the sum is close to 1 (resp. close to 0), with the promise that one of the two cases always holds. As part of our framework, we explore ideas introduced in [Chen and Ren, STOC'20] to show that, for the purpose of proving lower bounds, a top layer MAJ gate is equivalent to a (weaker) SUM̃ gate. Motivated by this result, we extend the algorithmic method and establish stronger lower bounds against bounded-depth circuits with layers of MAJ and SUM̃ gates. Among them, we prove that: - Lower bound: NQP does not admit fixed quasi-polynomial size MAJ∘SUM̃∘ACC⁰∘THR circuits. This is the first explicit lower bound against circuits with distinct layers of MAJ, SUM̃, and THR gates. Consequently, if the aforementioned equivalence between MAJ and SUM̃ as a top gate can be extended to intermediate layers, long sought-after lower bounds against the class THR∘THR of depth-2 polynomial-size threshold circuits would follow.
Cite as

Lijie Chen, Zhenjian Lu, Xin Lyu, and Igor C. Oliveira. Majority vs. Approximate Linear Sum and Average-Case Complexity Below NC¹. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 51:1-51:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.ICALP.2021.51,
  author =	{Chen, Lijie and Lu, Zhenjian and Lyu, Xin and Oliveira, Igor C.},
  title =	{{Majority vs. Approximate Linear Sum and Average-Case Complexity Below NC¹}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{51:1--51:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.51},
  URN =		{urn:nbn:de:0030-drops-141202},
  doi =		{10.4230/LIPIcs.ICALP.2021.51},
  annote =	{Keywords: circuit complexity, average-case hardness, complexity lower bounds}
}
Document
Track A: Algorithms, Complexity and Games
DOI: 10.4230/LIPIcs.ICALP.2021.94
An Efficient Coding Theorem via Probabilistic Representations and Its Applications

Authors: Zhenjian Lu and Igor C. Oliveira

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
A probabilistic representation of a string x ∈ {0,1}ⁿ is given by the code of a randomized algorithm that outputs x with high probability [Igor C. Oliveira, 2019]. We employ probabilistic representations to establish the first unconditional Coding Theorem in time-bounded Kolmogorov complexity. More precisely, we show that if a distribution ensemble 𝒟_m can be uniformly sampled in time T(m) and generates a string x ∈ {0,1}^* with probability at least δ, then x admits a time-bounded probabilistic representation of complexity O(log(1/δ) + log (T) + log(m)). Under mild assumptions, a representation of this form can be computed from x and the code of the sampler in time polynomial in n = |x|. We derive consequences of this result relevant to the study of data compression, pseudodeterministic algorithms, time hierarchies for sampling distributions, and complexity lower bounds. In particular, we describe an instance-based search-to-decision reduction for Levin’s Kt complexity [Leonid A. Levin, 1984] and its probabilistic analogue rKt [Igor C. Oliveira, 2019]. As a consequence, if a string x admits a succinct time-bounded representation, then a near-optimal representation can be generated from x with high probability in polynomial time. This partially addresses in a time-bounded setting a question from [Leonid A. Levin, 1984] on the efficiency of computing an optimal encoding of a string.
Cite as

Zhenjian Lu and Igor C. Oliveira. An Efficient Coding Theorem via Probabilistic Representations and Its Applications. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 94:1-94:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{lu_et_al:LIPIcs.ICALP.2021.94,
  author =	{Lu, Zhenjian and Oliveira, Igor C.},
  title =	{{An Efficient Coding Theorem via Probabilistic Representations and Its Applications}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{94:1--94:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.94},
  URN =		{urn:nbn:de:0030-drops-141630},
  doi =		{10.4230/LIPIcs.ICALP.2021.94},
  annote =	{Keywords: computational complexity, randomized algorithms, Kolmogorov complexity}
}
Document
DOI: 10.4230/LIPIcs.CCC.2020.15
Algorithms and Lower Bounds for De Morgan Formulas of Low-Communication Leaf Gates

Authors: Valentine Kabanets, Sajin Koroth, Zhenjian Lu, Dimitrios Myrisiotis, and Igor C. Oliveira

Published in: LIPIcs, Volume 169, 35th Computational Complexity Conference (CCC 2020)

Abstract
The class 𝖥𝖮𝖱𝖬𝖴𝖫𝖠[s]∘𝒢 consists of Boolean functions computable by size-s de Morgan formulas whose leaves are any Boolean functions from a class 𝒢. We give lower bounds and (SAT, Learning, and PRG) algorithms for FORMULA[n^{1.99}]∘𝒢, for classes 𝒢 of functions with low communication complexity. Let R^(k)(𝒢) be the maximum k-party number-on-forehead randomized communication complexity of a function in 𝒢. Among other results, we show that: - The Generalized Inner Product function 𝖦𝖨𝖯^k_n cannot be computed in 𝖥𝖮𝖱𝖬𝖴𝖫𝖠[s]∘𝒢 on more than 1/2+ε fraction of inputs for s = o(n²/{(k⋅4^k⋅R^(k)(𝒢)⋅log (n/ε)⋅log(1/ε))²}). This significantly extends the lower bounds against bipartite formulas obtained by [Avishay Tal, 2017]. As a corollary, we get an average-case lower bound for 𝖦𝖨𝖯^k_n against 𝖥𝖮𝖱𝖬𝖴𝖫𝖠[n^{1.99}]∘𝖯𝖳𝖥^{k-1}, i.e., sub-quadratic-size de Morgan formulas with degree-(k-1) PTF (polynomial threshold function) gates at the bottom. - There is a PRG of seed length n/2 + O(√s⋅R^(2)(𝒢)⋅log(s/ε)⋅log(1/ε)) that ε-fools FORMULA[s]∘𝒢. For the special case of FORMULA[s]∘𝖫𝖳𝖥, i.e., size-s formulas with LTF (linear threshold function) gates at the bottom, we get the better seed length O(n^{1/2}⋅s^{1/4}⋅log(n)⋅log(n/ε)). In particular, this provides the first non-trivial PRG (with seed length o(n)) for intersections of n half-spaces in the regime where ε ≤ 1/n, complementing a recent result of [Ryan O'Donnell et al., 2019]. - There exists a randomized 2^{n-t}-time #SAT algorithm for 𝖥𝖮𝖱𝖬𝖴𝖫𝖠[s]∘𝒢, where t = Ω(n/{√s⋅log²(s)⋅R^(2)(𝒢)})^{1/2}. In particular, this implies a nontrivial #SAT algorithm for 𝖥𝖮𝖱𝖬𝖴𝖫𝖠[n^1.99]∘𝖫𝖳𝖥. - The Minimum Circuit Size Problem is not in 𝖥𝖮𝖱𝖬𝖴𝖫𝖠[n^1.99]∘𝖷𝖮𝖱; thereby making progress on hardness magnification, in connection with results from [Igor Carboni Oliveira et al., 2019; Lijie Chen et al., 2019]. On the algorithmic side, we show that the concept class 𝖥𝖮𝖱𝖬𝖴𝖫𝖠[n^1.99]∘𝖷𝖮𝖱 can be PAC-learned in time 2^O(n/log n).
Cite as

Valentine Kabanets, Sajin Koroth, Zhenjian Lu, Dimitrios Myrisiotis, and Igor C. Oliveira. Algorithms and Lower Bounds for De Morgan Formulas of Low-Communication Leaf Gates. In 35th Computational Complexity Conference (CCC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 169, pp. 15:1-15:41, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{kabanets_et_al:LIPIcs.CCC.2020.15,
  author =	{Kabanets, Valentine and Koroth, Sajin and Lu, Zhenjian and Myrisiotis, Dimitrios and Oliveira, Igor C.},
  title =	{{Algorithms and Lower Bounds for De Morgan Formulas of Low-Communication Leaf Gates}},
  booktitle =	{35th Computational Complexity Conference (CCC 2020)},
  pages =	{15:1--15:41},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-156-6},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{169},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2020.15},
  URN =		{urn:nbn:de:0030-drops-125673},
  doi =		{10.4230/LIPIcs.CCC.2020.15},
  annote =	{Keywords: de Morgan formulas, circuit lower bounds, satisfiability (SAT), pseudorandom generators (PRGs), learning, communication complexity, polynomial threshold functions (PTFs), parities}
}
Document
DOI: 10.4230/LIPIcs.CCC.2020.22
NP-Hardness of Circuit Minimization for Multi-Output Functions

Authors: Rahul Ilango, Bruno Loff, and Igor C. Oliveira

Published in: LIPIcs, Volume 169, 35th Computational Complexity Conference (CCC 2020)

Abstract
Can we design efficient algorithms for finding fast algorithms? This question is captured by various circuit minimization problems, and algorithms for the corresponding tasks have significant practical applications. Following the work of Cook and Levin in the early 1970s, a central question is whether minimizing the circuit size of an explicitly given function is NP-complete. While this is known to hold in restricted models such as DNFs, making progress with respect to more expressive classes of circuits has been elusive. In this work, we establish the first NP-hardness result for circuit minimization of total functions in the setting of general (unrestricted) Boolean circuits. More precisely, we show that computing the minimum circuit size of a given multi-output Boolean function f : {0,1}^n → {0,1}^m is NP-hard under many-one polynomial-time randomized reductions. Our argument builds on a simpler NP-hardness proof for the circuit minimization problem for (single-output) Boolean functions under an extended set of generators. Complementing these results, we investigate the computational hardness of minimizing communication. We establish that several variants of this problem are NP-hard under deterministic reductions. In particular, unless 𝖯 = 𝖭𝖯, no polynomial-time computable function can approximate the deterministic two-party communication complexity of a partial Boolean function up to a polynomial. This has consequences for the class of structural results that one might hope to show about the communication complexity of partial functions.
Cite as

Rahul Ilango, Bruno Loff, and Igor C. Oliveira. NP-Hardness of Circuit Minimization for Multi-Output Functions. In 35th Computational Complexity Conference (CCC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 169, pp. 22:1-22:36, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{ilango_et_al:LIPIcs.CCC.2020.22,
  author =	{Ilango, Rahul and Loff, Bruno and Oliveira, Igor C.},
  title =	{{NP-Hardness of Circuit Minimization for Multi-Output Functions}},
  booktitle =	{35th Computational Complexity Conference (CCC 2020)},
  pages =	{22:1--22:36},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-156-6},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{169},
  editor =	{Saraf, Shubhangi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2020.22},
  URN =		{urn:nbn:de:0030-drops-125744},
  doi =		{10.4230/LIPIcs.CCC.2020.22},
  annote =	{Keywords: MCSP, circuit minimization, communication complexity, Boolean circuit}
}
Document
DOI: 10.4230/LIPIcs.ITCS.2020.70
Beyond Natural Proofs: Hardness Magnification and Locality

Authors: Lijie Chen, Shuichi Hirahara, Igor C. Oliveira, Ján Pich, Ninad Rajgopal, and Rahul Santhanam

Published in: LIPIcs, Volume 151, 11th Innovations in Theoretical Computer Science Conference (ITCS 2020)

Abstract
Hardness magnification reduces major complexity separations (such as EXP ⊈ NC^1) to proving lower bounds for some natural problem Q against weak circuit models. Several recent works [Igor Carboni Oliveira and Rahul Santhanam, 2018; Dylan M. McKay et al., 2019; Lijie Chen and Roei Tell, 2019; Igor Carboni Oliveira et al., 2019; Lijie Chen et al., 2019; Igor Carboni Oliveira, 2019; Lijie Chen et al., 2019] have established results of this form. In the most intriguing cases, the required lower bound is known for problems that appear to be significantly easier than Q, while Q itself is susceptible to lower bounds but these are not yet sufficient for magnification. In this work, we provide more examples of this phenomenon, and investigate the prospects of proving new lower bounds using this approach. In particular, we consider the following essential questions associated with the hardness magnification program: - Does hardness magnification avoid the natural proofs barrier of Razborov and Rudich [Alexander A. Razborov and Steven Rudich, 1997]? - Can we adapt known lower bound techniques to establish the desired lower bound for Q? We establish that some instantiations of hardness magnification overcome the natural proofs barrier in the following sense: slightly superlinear-size circuit lower bounds for certain versions of the minimum circuit size problem MCSP imply the non-existence of natural proofs. As a corollary of our result, we show that certain magnification theorems not only imply strong worst-case circuit lower bounds but also rule out the existence of efficient learning algorithms. Hardness magnification might sidestep natural proofs, but we identify a source of difficulty when trying to adapt existing lower bound techniques to prove strong lower bounds via magnification. This is captured by a locality barrier: existing magnification theorems unconditionally show that the problems Q considered above admit highly efficient circuits extended with small fan-in oracle gates, while lower bound techniques against weak circuit models quite often easily extend to circuits containing such oracles. This explains why direct adaptations of certain lower bounds are unlikely to yield strong complexity separations via hardness magnification.
Cite as

Lijie Chen, Shuichi Hirahara, Igor C. Oliveira, Ján Pich, Ninad Rajgopal, and Rahul Santhanam. Beyond Natural Proofs: Hardness Magnification and Locality. In 11th Innovations in Theoretical Computer Science Conference (ITCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 151, pp. 70:1-70:48, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.ITCS.2020.70,
  author =	{Chen, Lijie and Hirahara, Shuichi and Oliveira, Igor C. and Pich, J\'{a}n and Rajgopal, Ninad and Santhanam, Rahul},
  title =	{{Beyond Natural Proofs: Hardness Magnification and Locality}},
  booktitle =	{11th Innovations in Theoretical Computer Science Conference (ITCS 2020)},
  pages =	{70:1--70:48},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-134-4},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{151},
  editor =	{Vidick, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2020.70},
  URN =		{urn:nbn:de:0030-drops-117550},
  doi =		{10.4230/LIPIcs.ITCS.2020.70},
  annote =	{Keywords: Hardness Magnification, Natural Proofs, Minimum Circuit Size Problem, Circuit Lower Bounds}
}
Document
DOI: 10.4230/LIPIcs.CCC.2018.5
NP-hardness of Minimum Circuit Size Problem for OR-AND-MOD Circuits

Authors: Shuichi Hirahara, Igor C. Oliveira, and Rahul Santhanam

Published in: LIPIcs, Volume 102, 33rd Computational Complexity Conference (CCC 2018)

Abstract
The Minimum Circuit Size Problem (MCSP) asks for the size of the smallest boolean circuit that computes a given truth table. It is a prominent problem in NP that is believed to be hard, but for which no proof of NP-hardness has been found. A significant number of works have demonstrated the central role of this problem and its variations in diverse areas such as cryptography, derandomization, proof complexity, learning theory, and circuit lower bounds. The NP-hardness of computing the minimum numbers of terms in a DNF formula consistent with a given truth table was proved by W. Masek [William J. Masek, 1979] in 1979. In this work, we make the first progress in showing NP-hardness for more expressive classes of circuits, and establish an analogous result for the MCSP problem for depth-3 circuits of the form OR-AND-MOD_2. Our techniques extend to an NP-hardness result for MOD_m gates at the bottom layer under inputs from (Z / m Z)^n.
Cite as

Shuichi Hirahara, Igor C. Oliveira, and Rahul Santhanam. NP-hardness of Minimum Circuit Size Problem for OR-AND-MOD Circuits. In 33rd Computational Complexity Conference (CCC 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 102, pp. 5:1-5:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{hirahara_et_al:LIPIcs.CCC.2018.5,
  author =	{Hirahara, Shuichi and Oliveira, Igor C. and Santhanam, Rahul},
  title =	{{NP-hardness of Minimum Circuit Size Problem for OR-AND-MOD Circuits}},
  booktitle =	{33rd Computational Complexity Conference (CCC 2018)},
  pages =	{5:1--5:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-069-9},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{102},
  editor =	{Servedio, Rocco A.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2018.5},
  URN =		{urn:nbn:de:0030-drops-88831},
  doi =		{10.4230/LIPIcs.CCC.2018.5},
  annote =	{Keywords: NP-hardness, Minimum Circuit Size Problem, depth-3 circuits}
}
Document
DOI: 10.4230/LIPIcs.APPROX-RANDOM.2015.512
Learning Circuits with few Negations

Authors: Eric Blais, Clément L. Canonne, Igor C. Oliveira, Rocco A. Servedio, and Li-Yang Tan

Published in: LIPIcs, Volume 40, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2015)

Abstract
Monotone Boolean functions, and the monotone Boolean circuits that compute them, have been intensively studied in complexity theory. In this paper we study the structure of Boolean functions in terms of the minimum number of negations in any circuit computing them, a complexity measure that interpolates between monotone functions and the class of all functions. We study this generalization of monotonicity from the vantage point of learning theory, establishing nearly matching upper and lower bounds on the uniform-distribution learnability of circuits in terms of the number of negations they contain. Our upper bounds are based on a new structural characterization of negation-limited circuits that extends a classical result of A.A. Markov. Our lower bounds, which employ Fourier-analytic tools from hardness amplification, give new results even for circuits with no negations (i.e. monotone functions).
Cite as

Eric Blais, Clément L. Canonne, Igor C. Oliveira, Rocco A. Servedio, and Li-Yang Tan. Learning Circuits with few Negations. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 40, pp. 512-527, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{blais_et_al:LIPIcs.APPROX-RANDOM.2015.512,
  author =	{Blais, Eric and Canonne, Cl\'{e}ment L. and Oliveira, Igor C. and Servedio, Rocco A. and Tan, Li-Yang},
  title =	{{Learning Circuits with few Negations}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2015)},
  pages =	{512--527},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-89-7},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{40},
  editor =	{Garg, Naveen and Jansen, Klaus and Rao, Anup and Rolim, Jos\'{e} D. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX-RANDOM.2015.512},
  URN =		{urn:nbn:de:0030-drops-53214},
  doi =		{10.4230/LIPIcs.APPROX-RANDOM.2015.512},
  annote =	{Keywords: Boolean functions, monotonicity, negations, PAC learning}
}

Oliveira, Igor C. Carboni

Document
DOI: 10.4230/LIPIcs.CCC.2017.18
Conspiracies Between Learning Algorithms, Circuit Lower Bounds, and Pseudorandomness

Authors: Igor C. Carboni Oliveira and Rahul Santhanam

Published in: LIPIcs, Volume 79, 32nd Computational Complexity Conference (CCC 2017)

Abstract
We prove several results giving new and stronger connections between learning theory, circuit complexity and pseudorandomness. Let C be any typical class of Boolean circuits, and C[s(n)] denote n-variable C-circuits of size <= s(n). We show: Learning Speedups: If C[s(n)] admits a randomized weak learning algorithm under the uniform distribution with membership queries that runs in time 2^n/n^{\omega(1)}, then for every k >= 1 and epsilon > 0 the class C[n^k] can be learned to high accuracy in time O(2^{n^epsilon}). There is epsilon > 0 such that C[2^{n^{epsilon}}] can be learned in time 2^n/n^{omega(1)} if and only if C[poly(n)] can be learned in time 2^{(log(n))^{O(1)}}. Equivalences between Learning Models: We use learning speedups to obtain equivalences between various randomized learning and compression models, including sub-exponential time learning with membership queries, sub-exponential time learning with membership and equivalence queries, probabilistic function compression and probabilistic average-case function compression. A Dichotomy between Learnability and Pseudorandomness: In the non-uniform setting, there is non-trivial learning for C[poly(n)] if and only if there are no exponentially secure pseudorandom functions computable in C[poly(n)]. Lower Bounds from Nontrivial Learning: If for each k >= 1, (depth-d)-C[n^k] admits a randomized weak learning algorithm with membership queries under the uniform distribution that runs in time 2^n/n^{\omega(1)}, then for each k >= 1, BPE is not contained in (depth-d)-C[n^k]. If for some epsilon > 0 there are P-natural proofs useful against C[2^{n^{epsilon}}], then ZPEXP is not contained in C[poly(n)]. Karp-Lipton Theorems for Probabilistic Classes: If there is a k > 0 such that BPE is contained in i.o.Circuit[n^k], then BPEXP is contained in i.o.EXP/O(log(n)). If ZPEXP is contained in i.o.Circuit[2^{n/3}], then ZPEXP is contained in i.o.ESUBEXP. Hardness Results for MCSP: All functions in non-uniform NC^1 reduce to the Minimum Circuit Size Problem via truth-table reductions computable by TC^0 circuits. In particular, if MCSP is in TC^0 then NC^1 = TC^0.
Cite as

Igor C. Carboni Oliveira and Rahul Santhanam. Conspiracies Between Learning Algorithms, Circuit Lower Bounds, and Pseudorandomness. In 32nd Computational Complexity Conference (CCC 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 79, pp. 18:1-18:49, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{oliveira_et_al:LIPIcs.CCC.2017.18,
  author =	{Oliveira, Igor C. Carboni and Santhanam, Rahul},
  title =	{{Conspiracies Between Learning Algorithms, Circuit Lower Bounds, and Pseudorandomness}},
  booktitle =	{32nd Computational Complexity Conference (CCC 2017)},
  pages =	{18:1--18:49},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-040-8},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{79},
  editor =	{O'Donnell, Ryan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2017.18},
  URN =		{urn:nbn:de:0030-drops-75327},
  doi =		{10.4230/LIPIcs.CCC.2017.18},
  annote =	{Keywords: boolean circuits, learning theory, pseudorandomness}
}
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 About DROPS Imprint Privacy Contact