14 citations · 30 across the 16 of their papers we have counts for
19 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…
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.…
From Tractatus to Later Writings and Back -- New Implications from the Nachlass
Ruy J. G. B. de Queiroz
As a celebration of the \emph{Tractatus} 100th anniversary it might be worth revisiting its relation to the later writings. From the former to the latter, David Pears recalls that…
The Theory of an Arbitrary Higher -Model
Daniel O. Martínez-Rivillas, Ruy J. G. B. de Queiroz
One takes advantage of some basic properties of every homotopic -model (e.g.\ extensional Kan complex) to explore the higher -conversions, which would correspond to proofs o…
Solving Homotopy Domain Equations
Daniel O. Martínez-Rivillas, Ruy J. G. B. de Queiroz
In order to get -models with a rich structure of -groupoid, which we call "homotopy -models", a general technique is described for solving domain equations on any car…
Towards a Homotopy Domain Theory
Daniel O. Martínez-Rivillas, Ruy J. G. B. de Queiroz
An appropriate framework is put forward for the construction of -models with -groupoid structure, which we call \textit{homotopic -models}, through the use of an $\in…
Computational Paths -- An approach in the system
Tiago M. L. Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz +1
We use a labelled deduction system ( LNDTRS ) based on the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type, which al…
A Topological Application of Labelled Natural Deduction
Tiago M. L. Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz +1
We use a labelled deduction system based on the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type. We also define a term rewri…
Explicit Computational Paths
Arthur Freitas Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira
The treatment of equality as a type in type theory gives rise to an interesting type-theoretic structure known as `identity type'. The idea is that, given terms of a type …
Formalization of context-free language theory
Marcus V. M. Ramos, Ruy J. G. B. de Queiroz, Nelma Moreira +1
Context-free language theory is a subject of high importance in computer language processing technology as well as in formal language theory. This paper presents a formalization, u…
Formalization of simplification for context-free grammars
Marcus V. M. Ramos, Ruy J. G. B. de Queiroz
Context-free grammar simplification is a subject of high importance in computer language processing technology as well as in formal language theory. This paper presents a formaliza…
On Computational Paths and the Fundamental Groupoid of a Type
Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina de Oliveira
The main objective of this work is to study mathematical properties of computational paths. Originally proposed by de Queiroz \& Gabbay (1994) as `sequences of rewrites', computati…
On the Groupoid Model of Computational Paths
Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira
The main objective of this work is to study mathematical properties of computational paths. Originally proposed by de Queiroz \& Gabbay (1994) as `sequences or rewrites', computati…
Sequences of Rewrites: A Categorical Interpretation
Arthur Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira
In Martin-Löf's Intensional Type Theory, identity type is a heavily used and studied concept. The reason for that is the fact that it's responsible for the recently discovered conn…
Propositional equality, identity types, and direct computational paths
Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira
In proof theory the notion of canonical proof is rather basic, and it is usually taken for granted that a canonical proof of a sentence must be unique up to certain minor syntactic…