7 Search Results for "Cerna, David M."


Document
Spectral Norm, Economical Sieve, and Linear Invariance Testing of Boolean Functions

Authors: Swarnalipa Datta, Arijit Ghosh, Chandrima Kayal, Manaswi Paraashar, and Manmatha Roy

Published in: LIPIcs, Volume 364, 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)


Abstract
Given Boolean functions f, g : 𝔽₂ⁿ → {-1,+1}, we say they are linearly isomorphic if there exists A ∈ GL_n(𝔽₂) such that f(x) = g(Ax) for all x. We study this problem in the tolerant property testing framework under the known-unknown model, where g is given explicitly and f is accessible only via oracle queries, meaning the algorithm may adaptively request the value of f(x) for inputs x ∈ 𝔽₂ⁿ of its choice. Given parameters ε ≥ 0 and ω > 0, the goal is to distinguish whether there exists A ∈ GL_n(𝔽₂) such that the normalized Hamming distance between f and g(Ax) is at most ε, or whether for every A ∈ GL_n(𝔽₂) the distance is at least ε+ω. Our main result is a tolerant tester making Õ ((m/ω) ⁴) queries to f, where m is an upper bound on the spectral norm of g, improving the previous Õ ((m/ω) ^{24}) bound of Wimmer and Yoshida. We complement this with a nearly matching lower bound of Ω(m²) for constant ω (for example, ω = 1/4), improving the prior Ω(log m) lower bound of Grigorescu, Wimmer and Xie. A key technical ingredient on the algorithmic side is a query-efficient local list corrector. For the lower bound, we give a reduction from communication complexity using a novel subclass of Maiorana-McFarland functions from symmetric-key cryptography.

Cite as

Swarnalipa Datta, Arijit Ghosh, Chandrima Kayal, Manaswi Paraashar, and Manmatha Roy. Spectral Norm, Economical Sieve, and Linear Invariance Testing of Boolean Functions. In 43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 364, pp. 30:1-30:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)


Copy BibTex To Clipboard

@InProceedings{datta_et_al:LIPIcs.STACS.2026.30,
  author =	{Datta, Swarnalipa and Ghosh, Arijit and Kayal, Chandrima and Paraashar, Manaswi and Roy, Manmatha},
  title =	{{Spectral Norm, Economical Sieve, and Linear Invariance Testing of Boolean Functions}},
  booktitle =	{43rd International Symposium on Theoretical Aspects of Computer Science (STACS 2026)},
  pages =	{30:1--30:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-412-3},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{364},
  editor =	{Mahajan, Meena and Manea, Florin and McIver, Annabelle and Thắng, Nguy\~{ê}n Kim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2026.30},
  URN =		{urn:nbn:de:0030-drops-255194},
  doi =		{10.4230/LIPIcs.STACS.2026.30},
  annote =	{Keywords: Boolean Function, Isomorphism of Boolean Function, Fourier Analysis, Sublinear Algorithm, Property Testing}
}
Document
(Can't) Fly Me to the Moon or Mars? Context of Use Analysis Approaches for Space Exploration

Authors: Tilo Mentler

Published in: OASIcs, Volume 130, Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)


Abstract
Contexts of use are a central concept of research and development in human-computer interaction (HCI). Their in-depth understanding is a key for usable and acceptable computer-aided solutions and a particular challenge in connection with space exploration. It is necessary to examine which of the established approaches can be implemented here and where methodological adjustments are necessary. This article provides a systematic consideration of three perspectives to understand space contexts of use: theory and literature, imparted experiential knowledge, and personal experience. Potentials and risks are evaluated. The findings of HCI research in safety-critical contexts and under COVID-19 conditions that can be transferred to space HCI are taken up.

Cite as

Tilo Mentler. (Can't) Fly Me to the Moon or Mars? Context of Use Analysis Approaches for Space Exploration. In Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025). Open Access Series in Informatics (OASIcs), Volume 130, pp. 23:1-23:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{mentler:OASIcs.SpaceCHI.2025.23,
  author =	{Mentler, Tilo},
  title =	{{(Can't) Fly Me to the Moon or Mars? Context of Use Analysis Approaches for Space Exploration}},
  booktitle =	{Advancing Human-Computer Interaction for Space Exploration (SpaceCHI 2025)},
  pages =	{23:1--23:7},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-384-3},
  ISSN =	{2190-6807},
  year =	{2025},
  volume =	{130},
  editor =	{Bensch, Leonie and Nilsson, Tommy and Nisser, Martin and Pataranutaporn, Pat and Schmidt, Albrecht and Sumini, Valentina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SpaceCHI.2025.23},
  URN =		{urn:nbn:de:0030-drops-240135},
  doi =		{10.4230/OASIcs.SpaceCHI.2025.23},
  annote =	{Keywords: Context of Use, Experiential Knowledge, Remote Contextual Inquiry}
}
Document
RANDOM
Testing Isomorphism of Boolean Functions over Finite Abelian Groups

Authors: Swarnalipa Datta, Arijit Ghosh, Chandrima Kayal, Manaswi Paraashar, and Manmatha Roy

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


Abstract
Let f and g be Boolean functions over a finite Abelian group 𝒢, where g is fully known and f is accessible via queries; that is, given any x ∈ 𝒢, we can obtain the value f(x). We study the problem of tolerant isomorphism testing: given parameters ε ≥ 0 and τ > 0, the goal is to determine, using as few queries as possible, whether there exists an automorphism σ of 𝒢 such that the fractional Hamming distance between f∘σ and g is at most ε, or whether for every automorphism σ, the distance is at least ε + τ. We design an efficient tolerant property testing algorithm for this problem over finite Abelian groups with constant exponent. The exponent of a finite group refers to the largest order of any element in the group. The query complexity of our algorithm is polynomial in s and 1/τ, where s bounds the spectral norm of the function g, and τ is the tolerance parameter. In addition, we present an improved algorithm in the case where g is Fourier sparse, meaning that its Fourier expansion contains only a small number of nonzero coefficients. Our approach draws on key ideas from Abelian group theory and Fourier analysis, including the annihilator of a subgroup, Pontryagin duality, and a pseudo inner product defined over finite Abelian groups. We believe that these techniques will be useful more broadly in the design of property testing algorithms.

Cite as

Swarnalipa Datta, Arijit Ghosh, Chandrima Kayal, Manaswi Paraashar, and Manmatha Roy. Testing Isomorphism of Boolean Functions over Finite Abelian Groups. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 353, pp. 66:1-66:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{datta_et_al:LIPIcs.APPROX/RANDOM.2025.66,
  author =	{Datta, Swarnalipa and Ghosh, Arijit and Kayal, Chandrima and Paraashar, Manaswi and Roy, Manmatha},
  title =	{{Testing Isomorphism of Boolean Functions over Finite Abelian Groups}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2025)},
  pages =	{66:1--66:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-397-3},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{353},
  editor =	{Ene, Alina and Chattopadhyay, Eshan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2025.66},
  URN =		{urn:nbn:de:0030-drops-244328},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2025.66},
  annote =	{Keywords: Analysis of Boolean functions, Abelian groups, Automorphism group, Function isomorphism, Spectral norm}
}
Document
Combining Generalization Algorithms in Regular Collapse-Free Theories

Authors: Mauricio Ayala-Rincón, David M. Cerna, Temur Kutsia, and Christophe Ringeissen

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)


Abstract
We look at the generalization problem modulo some equational theories. This problem is dual to the unification problem: given two input terms, we want to find a common term whose respective two instances are equivalent to the original terms modulo the theory. There exist algorithms for finding generalizations over various equational theories. We focus on modular construction of equational generalization algorithms for the union of signature-disjoint theories. Specifically, we consider the class of regular and collapse-free theories, showing how to combine existing generalization algorithms to produce specific solutions in these cases. Additionally, we identify a class of theories that admit a generalization algorithm based on the application of axioms to resolve the problem. To define this class, we rely on the notion of syntactic theories, a concept originally introduced to develop unification procedures similar to the one known for syntactic unification. We demonstrate that syntactic theories are also helpful in developing generalization procedures similar to those used for syntactic generalization.

Cite as

Mauricio Ayala-Rincón, David M. Cerna, Temur Kutsia, and Christophe Ringeissen. Combining Generalization Algorithms in Regular Collapse-Free Theories. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 7:1-7:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{ayalarincon_et_al:LIPIcs.FSCD.2025.7,
  author =	{Ayala-Rinc\'{o}n, Mauricio and Cerna, David M. and Kutsia, Temur and Ringeissen, Christophe},
  title =	{{Combining Generalization Algorithms in Regular Collapse-Free Theories}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{7:1--7:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.7},
  URN =		{urn:nbn:de:0030-drops-236228},
  doi =		{10.4230/LIPIcs.FSCD.2025.7},
  annote =	{Keywords: Generalization, Anti-unification, Equational theories, Combination}
}
Document
Unital Anti-Unification: Type and Algorithms

Authors: David M. Cerna and Temur Kutsia

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)


Abstract
Unital equational theories are defined by axioms that assert the existence of the unit element for some function symbols. We study anti-unification (AU) in unital theories and address the problems of establishing generalization type and designing anti-unification algorithms. First, we prove that when the term signature contains at least two unital functions, anti-unification is of the nullary type by showing that there exists an AU problem, which does not have a minimal complete set of generalizations. Next, we consider two special cases: the linear variant and the fragment with only one unital symbol, and design AU algorithms for them. The algorithms are terminating, sound, complete, and return tree grammars from which the set of generalizations can be constructed. Anti-unification for both special cases is finitary. Further, the algorithm for the one-unital fragment is extended to the unrestricted case. It terminates and returns a tree grammar which produces an infinite set of generalizations. At the end, we discuss how the nullary type of unital anti-unification might affect the anti-unification problem in some combined theories, and list some open questions.

Cite as

David M. Cerna and Temur Kutsia. Unital Anti-Unification: Type and Algorithms. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{cerna_et_al:LIPIcs.FSCD.2020.26,
  author =	{Cerna, David M. and Kutsia, Temur},
  title =	{{Unital Anti-Unification: Type and Algorithms}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{26:1--26:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.26},
  URN =		{urn:nbn:de:0030-drops-123482},
  doi =		{10.4230/LIPIcs.FSCD.2020.26},
  annote =	{Keywords: Anti-unification, tree grammars, unital theories, collapse theories}
}
Document
A Generic Framework for Higher-Order Generalizations

Authors: David M. Cerna and Temur Kutsia

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)


Abstract
We consider a generic framework for anti-unification of simply typed lambda terms. It helps to compute generalizations which contain maximally common top part of the input expressions, without nesting generalization variables. The rules of the corresponding anti-unification algorithm are formulated, and their soundness and termination are proved. The algorithm depends on a parameter which decides how to choose terms under generalization variables. Changing the particular values of the parameter, we obtained four new unitary variants of higher-order anti-unification and also showed how the already known pattern generalization fits into the schema.

Cite as

David M. Cerna and Temur Kutsia. A Generic Framework for Higher-Order Generalizations. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{cerna_et_al:LIPIcs.FSCD.2019.10,
  author =	{Cerna, David M. and Kutsia, Temur},
  title =	{{A Generic Framework for Higher-Order Generalizations}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{10:1--10:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.10},
  URN =		{urn:nbn:de:0030-drops-105175},
  doi =		{10.4230/LIPIcs.FSCD.2019.10},
  annote =	{Keywords: anti-unification, typed lambda calculus, least general generalization}
}
Document
Higher-Order Equational Pattern Anti-Unification

Authors: David M. Cerna and Temur Kutsia

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)


Abstract
We consider anti-unification for simply typed lambda terms in associative, commutative, and associative-commutative theories and develop a sound and complete algorithm which takes two lambda terms and computes their generalizations in the form of higher-order patterns. The problem is finitary: the minimal complete set of generalizations contains finitely many elements. We define the notion of optimal solution and investigate special fragments of the problem for which the optimal solution can be computed in linear or polynomial time.

Cite as

David M. Cerna and Temur Kutsia. Higher-Order Equational Pattern Anti-Unification. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{cerna_et_al:LIPIcs.FSCD.2018.12,
  author =	{Cerna, David M. and Kutsia, Temur},
  title =	{{Higher-Order Equational Pattern Anti-Unification}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{12:1--12:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.12},
  URN =		{urn:nbn:de:0030-drops-91826},
  doi =		{10.4230/LIPIcs.FSCD.2018.12},
  annote =	{Keywords: Simply typed lambda calculus, anti-unification, equational theories}
}
  • Refine by Type
  • 7 Document/PDF
  • 4 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 3 2025
  • 1 2020
  • 1 2019
  • 1 2018

  • Refine by Author
  • 4 Cerna, David M.
  • 4 Kutsia, Temur
  • 2 Datta, Swarnalipa
  • 2 Ghosh, Arijit
  • 2 Kayal, Chandrima
  • Show More...

  • Refine by Series/Journal
  • 6 LIPIcs
  • 1 OASIcs

  • Refine by Classification
  • 3 Theory of computation → Rewrite systems
  • 2 Theory of computation → Boolean function learning
  • 2 Theory of computation → Equational logic and rewriting
  • 2 Theory of computation → Higher order logic
  • 1 Computing methodologies → Symbolic and algebraic manipulation
  • Show More...

  • Refine by Keyword
  • 2 Anti-unification
  • 2 anti-unification
  • 1 Abelian groups
  • 1 Analysis of Boolean functions
  • 1 Automorphism group
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail