Arthur F. Ramos

15 papers Journal 15
YearRankTypeTitle / Venue / Authors
2025 J jnl
A Modular Lean 4 Framework for Confluence and Strong Normalization of Lambda Calculi with Products and Sums.
CoRR
Arthur F. Ramos, Anjolina Grisi de Oliveira, Ruy J. G. B. de Queiroz, Tiago Mendonça Lucena de Veras
2025 J jnl
Computational Paths Form a Weak ω-Groupoid.
CoRR
Arthur F. Ramos, Tiago M. L. de Veras, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira
2025 J jnl
Computational paths - a weak groupoid.
J. Log. Comput.
Tiago M. L. de Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira
2025 J jnl
Formalizing Computational Paths and Fundamental Groups in Lean.
CoRR
Arthur F. Ramos, Anjolina Grisi de Oliveira, Ruy J. G. B. de Queiroz, Tiago M. L. de Veras
2025 J jnl
The Seifert-van Kampen Theorem via Computational Paths: A Formalized Approach to Computing Fundamental Groups.
CoRR
Arthur F. Ramos, Tiago Mendonça Lucena de Veras, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira
2020 J jnl
Computational Paths - A Weak Groupoid.
CoRR
Tiago M. L. de Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz, Thiago D. O. Silva, Anjolina Grisi de Oliveira
2019 J jnl
A Topological Application of Labelled Natural Deduction.
CoRR
Tiago Mendonça Lucena de Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira
2019 J jnl
An alternative approach to the calculation of fundamental groups based on labeled natural deduction.
CoRR
Tiago Mendonça Lucena de Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira
2018 J jnl
On the Calculation of Fundamental Groups in Homotopy Type Theory by Means of Computational Paths.
CoRR
Tiago Mendonça Lucena de Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira
2018 J jnl
On the Use of Computational Paths in Path Spaces of Homotopy Type Theory.
CoRR
Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira, Tiago Mendonça Lucena de Veras
2017 J jnl
On the identity type as the type of computational paths.
Log. J. IGPL
Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira
2015 J jnl
On Computational Paths and the Fundamental Groupoid of a Type.
CoRR
Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira
2015 J jnl
On the Groupoid Model of Computational Paths.
CoRR
Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira
2015 J jnl
On the Identity Type as the Type of Computational Paths.
CoRR
Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira
2014 J jnl
Sequences of Rewrites: A Categorical Interpretation.
CoRR
Arthur F. Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira