AR
Arthur
cs.LOmath.COmath.ATcs.FLcs.PLmath.ACmath.CTmath.DGmath.RA
On Valency
published · living versionsW_7yhnzhrm·v1 · currentpublished
A Lean Certificate for the Single Source Unsplittable Flow Cost Counterexample
with David Barros Hulak, Ruy J. G. B. de Queiroz
1 version
Preprints & journals
25 papers in the corpus · 2014–2026A Sharp Product Bound for Disjoint Cross-Intersecting 3-Graphs with Covering Number Three2609.26206v1 · Arthur F. Ramos, David B. Hulak, Ruy J. G. B. de Queiroz2026 · 0 citationsarXiv
A Theory of a Two-Dimensional Typed Lambda Calculus2609.19479v1 · Daniel O. Mart'inez-Rivillas, Arthur F. Ramos, Ruy J. G. B. de Queiroz2026 · 0 citationsarXiv
Topological Semantics for Scoped Computational Paths2608.04228v3 · Arthur Freitas Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira et al.2026 · 0 citationsarXiv
Optimal Finite Interval Discrepancy via Binary Refinement2608.08431v1 · Arthur F. Ramos, David B. Hulak, Ruy J. G. B. de Queiroz2026 · 0 citationsarXiv
Formalizing Singer Sidon Constructions and Sidon Set Infrastructure in Lean 42605.03274v2 · David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz2026 · 0 citationsarXiv
Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=02605.01028v1 · David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz2026 · 0 citationsarXiv
Certified Qualitative Analysis of the SIR ODE and Reusable Scalar Lemmas in Isabelle/HOL2605.02474v1 · David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz2026 · 0 citationsarXiv
Token-Sensitive Enclosure Semantics for Measurement-Bearing Expressions2604.07626v2 · David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz2026 · 0 citationsarXiv
Exterior-Model Spinors in Split Rank: Exact Levi Images and Square-Determinant Obstructions2604.26155v1 · Arthur F. Ramos, David B. Hulak, Ruy J. G. B. de Queiroz2026 · 0 citationsarXiv
Pair-Trace Absorption Certificates for Regular Induced Subgraphs2604.23882v1 · Arthur F. Ramos, David Barros Hulak, Ruy J. G. B. de Queiroz2026 · 0 citationsarXiv
Recursive Completion in Higher K-Models: Front-Seed Semantics, Proof-Relevant Witnesses, and the K-Infinity Model2604.12981v1 · Daniel O. Martinez-Rivillas, Arthur F. Ramos, Ruy J. G. B. de Queiroz2026 · 0 citationsarXiv
A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 42604.05238v1 · Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira2026 · 0 citationsarXiv
The Seifert-van Kampen Theorem via Computational Paths: A Formalized Approach to Computing Fundamental Groups2512.03175v3 · Arthur F. Ramos, Tiago M. L. de Veras, Ruy J. G. B. de Queiroz et al.2025 · 0 citationsarXiv
A Modular Lean 4 Framework for Confluence and Strong Normalization of Lambda Calculi with Products and Sums2512.09280v1 · Arthur Ramos, Anjolina Oliveira, Ruy de Queiroz et al.2025 · 0 citationsarXiv
Computational Paths Form a Weak {\omega}-Groupoid2512.00657v1 · Arthur F. Ramos, Tiago M. L. de Veras, Ruy J. G. B. de Queiroz et al.2025 · 0 citationsarXiv
Formalizing Computational Paths and Fundamental Groups in Lean2511.19142v2 · Arthur F. Ramos, Anjolina G. de Oliveira, Ruy J. G. B. de Queiroz et al.2025 · 0 citationsarXiv
Computational Paths -- An approach in the $LND_{EQ}-TRS_{2}$ system2007.07769v3 · Tiago M. L. Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz et al.2020 · 0 citationsarXiv
A Topological Application of Labelled Natural Deduction1906.09105v4 · Tiago M. L.Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz et al.2019 · 6 citationsarXiv
An alternative approach to the calculation of fundamental groups based on labeled natural deduction1906.09107v1 · Tiago M. L. de Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz et al.2019 · 3 citationsarXiv
On the Calculation of Fundamental Groups in Homotopy Type Theory by Means of Computational Paths1804.01413v2 · Tiago Mendonca Lucena de Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz et al.2018 · 1 citationarXiv
Explicit Computational Paths1609.05079v3 · Arthur Freitas Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira2016 · 3 citationsarXiv
On the Use of Computational Paths in Path Spaces of Homotopy Type Theory1803.01709v1 · Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira et al.2018 · 0 citationsarXiv
On the Groupoid Model of Computational Paths1506.02721v2 · Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira2015 · 1 citationarXiv
On Computational Paths and the Fundamental Groupoid of a Type1509.06429v1 · Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina de Oliveira2015 · 2 citationsarXiv
Sequences of Rewrites: A Categorical Interpretation1412.2105v2 · Arthur Ramos, Ruy J. G. B. de Queiroz, Anjolina G. de Oliveira2014 · 1 citationarXiv
Career total: 47 works. 25 are in this corpus.
Profile built from the corpus for this byline.
Author records are still filling in while the Hub is in alpha. If this is your page, you'll be able to claim it soon. Spot a mistake? Tell us.