6 citations · 15 across the 25 of their papers we have counts for
28 papers
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 Semantics for Scoped Computational Paths
Arthur Freitas Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira +1
Computational paths record the steps of an equality derivation. We give them a topological semantics that distinguishes derivable rewrites from arbitrary homotopies. Coherent repre…
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…
From Rules to Nash Equilibria: A Lean 4 Case Study in Game-Theoretic Analysis of a Competitive Trading Card Game
Arthur F. Ramos, Tulio Soria
We present a metagame analysis of the competitive Pokemon Trading Card Game, machine-checked in Lean 4 over real tournament data. The headline game-theoretic results, including Nas…