14 citations · 30 across the 16 of their papers we have counts for
6 papers · 1 filter
A Theory of a Two-Dimensional Typed Lambda Calculus
Daniel O. Martínez-Rivillas, Arthur F. Ramos, Ruy J. G. B. de Queiroz
We present a typed two-dimensional -calculus whose equality evidence is \emph{computational}: a path between two terms is an explicit finite sequence of one-step conversions (th…
Topological Computational Paths: Presentation Invariance and Observable Quotients
Arthur Freitas Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira +1
A computational path records the steps used to establish an equality. Topologies on computational equality witnesses can depend on the chosen generators and execution schedule, eve…
A Sharp Product Bound for Disjoint Cross-Intersecting 3-Graphs with Covering Number Three
Arthur F. Ramos, David B. Hulak, Ruy J. G. B. de Queiroz
Lin, Frankl, and Wu proved that the product of the sizes of two cross-intersecting 3-uniform hypergraphs with covering number three is at most 121. They conjectured that requiring…
Optimal Finite Interval Discrepancy via Binary Refinement
Arthur F. Ramos, David B. Hulak, Ruy J. G. B. de Queiroz
DeLeo, Henderschedt, and Wells introduced a finite-horizon version of the classical de Bruijn--Erdos interval discrepancy problem. Starting from the unit interval, one repeatedly s…
Multiplier obstructions for Legendre pairs of length 333
Arthur F. Ramos, David B. Hulak, Ruy J. G. B. de Queiroz
A Legendre pair of length 333 would yield a Hadamard matrix of order 668, the smallest order presently unresolved by the Hadamard conjecture. We study the structured case in which…
Formalizing Singer Sidon Constructions and Sidon Set Infrastructure in Lean 4
David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz
Erdős Problem 30 asks for sharp asymptotics of the Sidon extremal function , and Singer's construction is the classical source of lower-bound examples matching the main term.…