Found 2 Possible Name Variants:

Document

**Published in:** LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

AC^0 o MOD_2 circuits are AC^0 circuits augmented with a layer of parity gates just above the input layer. We study AC^0 o MOD2 circuit lower bounds for computing the Boolean Inner Product functions. Recent works by Servedio and Viola (ECCC TR12-144) and Akavia et al. (ITCS 2014) have highlighted this problem as a frontier problem in circuit complexity that arose both as a first step towards solving natural special cases of the matrix rigidity problem and as a candidate for constructing pseudorandom generators of minimal complexity. We give the first superlinear lower bound for the Boolean Inner Product function against AC^0 o MOD2 of depth four or greater. Specifically, we prove a superlinear lower bound for circuits of arbitrary constant depth, and an ~Omega(n^2) lower bound for the special case of depth-4 AC^0 o MOD_2. Our proof of the depth-4 lower bound employs a new "moment-matching" inequality for bounded, nonnegative integer-valued random variables that may be of independent interest: we prove an optimal bound on the maximum difference between two discrete distributions’ values at 0, given that their first d moments match.

Mahdi Cheraghchi, Elena Grigorescu, Brendan Juba, Karl Wimmer, and Ning Xie. AC^0 o MOD_2 Lower Bounds for the Boolean Inner Product. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 35:1-35:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{cheraghchi_et_al:LIPIcs.ICALP.2016.35, author = {Cheraghchi, Mahdi and Grigorescu, Elena and Juba, Brendan and Wimmer, Karl and Xie, Ning}, title = {{AC^0 o MOD\underline2 Lower Bounds for the Boolean Inner Product}}, booktitle = {43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)}, pages = {35:1--35:14}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-013-2}, ISSN = {1868-8969}, year = {2016}, volume = {55}, editor = {Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.35}, URN = {urn:nbn:de:0030-drops-63150}, doi = {10.4230/LIPIcs.ICALP.2016.35}, annote = {Keywords: Boolean analysis, circuit complexity, lower bounds} }

Document

**Published in:** LIPIcs, Volume 3, 26th International Symposium on Theoretical Aspects of Computer Science (2009)

We consider the task of testing properties of Boolean functions that are invariant under linear transformations of the Boolean cube. Previous work in property testing, including the linearity test and the test for Reed-Muller codes, has mostly focused on such tasks for linear properties. The one exception is a test due to Green for {}``triangle freeness'': A function $f:\mathbb{F}_{2}^{n}\to\mathbb{F}_{2}$ satisfies this property if $f(x),f(y),f(x+y)$ do not all equal $1$, for any pair $x,y\in\mathbb{F}_{2}^{n}$.
Here we extend this test to a more systematic study of testing for linear-invariant non-linear properties. We consider properties that are described by a single forbidden pattern (and its linear transformations), i.e., a property is given by $k$ points $v_{1},\ldots,v_{k}\in\mathbb{F}_{2}^{k}$ and $f:\mathbb{F}_{2}^{n}\to\mathbb{F}_{2}$ satisfies the property that if for all linear maps $L:\mathbb{F}_{2}^{k}\to\mathbb{F}_{2}^{n}$ it is the case that $f(L(v_{1})),\ldots,f(L(v_{k}))$ do not all equal $1$. We show that this property is testable if the underlying matroid specified by $v_{1},\ldots,v_{k}$ is a graphic matroid. This extends Green's result to an infinite class of new properties.
Our techniques extend those of Green and in particular we establish a link between the notion of {}``1-complexity linear systems'' of Green and Tao, and graphic matroids, to derive the results.

Arnab Bhattacharyya, Victor Chen, Madhu Sudan, and Ning Xie. Testing Linear-Invariant Non-Linear Properties. In 26th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 3, pp. 135-146, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{bhattacharyya_et_al:LIPIcs.STACS.2009.1823, author = {Bhattacharyya, Arnab and Chen, Victor and Sudan, Madhu and Xie, Ning}, title = {{Testing Linear-Invariant Non-Linear Properties}}, booktitle = {26th International Symposium on Theoretical Aspects of Computer Science}, pages = {135--146}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-09-5}, ISSN = {1868-8969}, year = {2009}, volume = {3}, editor = {Albers, Susanne and Marion, Jean-Yves}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2009.1823}, URN = {urn:nbn:de:0030-drops-18235}, doi = {10.4230/LIPIcs.STACS.2009.1823}, annote = {Keywords: } }

Document

**Published in:** Dagstuhl Seminar Proceedings, Volume 8341, Sublinear Algorithms (2008)

For Boolean functions that are $epsilon$-far from the set of linear functions,
we study the lower bound on the rejection probability (denoted by $extsc{rej}(epsilon)$) of the linearity test suggested by Blum, Luby and Rubinfeld.
This problem is arguably the most fundamental and extensively studied problem in property testing of Boolean functions.
The previously best bounds for $extsc{rej}(epsilon)$ were obtained by Bellare,
Coppersmith, H{{a}}stad, Kiwi and Sudan. They used Fourier analysis
to show that $ extsc{rej}(epsilon) geq e$ for every $0 leq epsilon leq
frac{1}{2}$. They also conjectured that this bound might not be tight for
$epsilon$'s which are close to $1/2$. In this paper we show that this indeed is
the case. Specifically, we improve the lower bound of $ extsc{rej}(epsilon) geq
epsilon$ by an additive constant that depends only on $epsilon$:
$extsc{rej}(epsilon) geq epsilon + min {1376epsilon^{3}(1-2epsilon)^{12},
frac{1}{4}epsilon(1-2epsilon)^{4}}$, for every $0 leq epsilon leq frac{1}{2}$.
Our analysis is based on a relationship between $extsc{rej}(epsilon)$ and the
weight distribution of a coset of the Hadamard code. We use both Fourier
analysis and coding theory tools to estimate this weight distribution.

Tali Kaufman, Simon Litsyn, and Ning Xie. Breaking the $\epsilon$-Soundness Bound of the Linearity Test over GF(2). In Sublinear Algorithms. Dagstuhl Seminar Proceedings, Volume 8341, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{kaufman_et_al:DagSemProc.08341.3, author = {Kaufman, Tali and Litsyn, Simon and Xie, Ning}, title = {{Breaking the \$\backslashepsilon\$-Soundness Bound of the Linearity Test over GF(2)}}, booktitle = {Sublinear Algorithms}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2008}, volume = {8341}, editor = {Artur Czumaj and S. Muthu Muthukrishnan and Ronitt Rubinfeld and Christian Sohler}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08341.3}, URN = {urn:nbn:de:0030-drops-16971}, doi = {10.4230/DagSemProc.08341.3}, annote = {Keywords: Linearity test, Fourier analysis, coding theory} }

Document

Artifact

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

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.

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

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

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.

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

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

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.

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} }