Arthur F. Ramos

According to our database, Arthur F. Ramos authored at least 28 papers between 2014 and 2026.

Collaborative distances:

• Dijkstra number of five.
• Erdős number of four.

2026

Certified Qualitative Analysis of the SIR ODE and Reusable Scalar Lemmas in Isabelle/HOL.

David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz

CoRR, May, 2026

Stokes' Theorem for Smooth Singular Cubes in Lean 4: True Pullback, Bridges to mathlib4, and Chain-Level d^2=0.

David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz

CoRR, May, 2026

Recursive Completion in Higher K-Models: Front-Seed Semantics, Proof-Relevant Witnesses, and the K-Infinity Model.

Daniel O. Martínez-Rivillas, Arthur F. Ramos, Ruy J. G. B. de Queiroz

CoRR, April, 2026

Token-Sensitive Enclosure Semantics for Measurement-Bearing Expressions.

David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz

CoRR, April, 2026

A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 4.

Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira

CoRR, April, 2026

Alon's Combinatorial Nullstellensatz.

Arthur Freitas Ramos, Ruy José Guerra Barretto de Queiroz, David B. Hulak

Arch. Formal Proofs, 2026

The Mostowski Collapse Theorem.

Arthur Freitas Ramos, David B. Hulak, Ruy José Guerra Barretto de Queiroz

Arch. Formal Proofs, 2026

Andrew's Monotone Chain Convex Hull Algorithm.

Arthur Freitas Ramos, David B. Hulak, Ruy José Guerra Barretto de Queiroz

Arch. Formal Proofs, 2026

Nash Equilibria for Finite Games in Isabelle/HOL.

Arthur Freitas Ramos, David B. Hulak, Ruy José Guerra Barretto de Queiroz

Arch. Formal Proofs, 2026

The Banach-Tarski Paradox in Isabelle/HOL.

Arthur Freitas Ramos, David B. Hulak, Ruy José Guerra Barretto de Queiroz

Arch. Formal Proofs, 2026

Aho-Corasick String Matching.

Arthur Freitas Ramos, David B. Hulak, Ruy José Guerra Barretto de Queiroz

Arch. Formal Proofs, 2026

Nagata Factoriality.

Arthur Freitas Ramos, David B. Hulak, Ruy José Guerra Barretto de Queiroz

Arch. Formal Proofs, 2026

2025

A Modular Lean 4 Framework for Confluence and Strong Normalization of Lambda Calculi with Products and Sums.

Arthur F. Ramos, Anjolina Grisi de Oliveira, Ruy J. G. B. de Queiroz, Tiago Mendonça Lucena de Veras

CoRR, December, 2025

The Seifert-van Kampen Theorem via Computational Paths: A Formalized Approach to Computing Fundamental Groups.

Arthur F. Ramos, Tiago Mendonça Lucena de Veras, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira

CoRR, December, 2025

Computational Paths Form a Weak ω-Groupoid.

Arthur F. Ramos, Tiago M. L. de Veras, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira

CoRR, December, 2025

Formalizing Computational Paths and Fundamental Groups in Lean.

Arthur F. Ramos, Anjolina Grisi de Oliveira, Ruy J. G. B. de Queiroz, Tiago M. L. de Veras

CoRR, November, 2025

Computational paths - a weak groupoid.

Tiago M. L. de Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira

J. Log. Comput., 2025

2020

Computational Paths - A Weak Groupoid.

Tiago M. L. de Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz, Thiago D. O. Silva, Anjolina Grisi de Oliveira

CoRR, 2020

2019

An alternative approach to the calculation of fundamental groups based on labeled natural deduction.

Tiago Mendonça Lucena de Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira

CoRR, 2019

A Topological Application of Labelled Natural Deduction.

Tiago Mendonça Lucena de Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira

CoRR, 2019

Explicit Computational Paths in Type Theory.

Arthur Freitas Ramos

Bull. Symb. Log., 2019

2018

On the Calculation of Fundamental Groups in Homotopy Type Theory by Means of Computational Paths.

Tiago Mendonça Lucena de Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira

CoRR, 2018

On the Use of Computational Paths in Path Spaces of Homotopy Type Theory.

Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira, Tiago Mendonça Lucena de Veras

CoRR, 2018

2017

On the identity type as the type of computational paths.

Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira

Log. J. IGPL, 2017

2016

Computational Paths and Identity Types.

Arthur Freitas Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira

CoRR, 2016

2015

On Computational Paths and the Fundamental Groupoid of a Type.

Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira

CoRR, 2015

On the Groupoid Model of Computational Paths.

Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira

CoRR, 2015

2014

Sequences of Rewrites: A Categorical Interpretation.

Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira

CoRR, 2014