3 citations · 3 across the 18 of their papers we have counts for
4 papers · 2 filters
The Seifert-van Kampen Theorem via Computational Paths: A Formalized Approach to Computing Fundamental Groups
Arthur F. Ramos, Tiago M. L. de Veras, Ruy J. G. B. de Queiroz +1
The Seifert-van Kampen theorem computes the fundamental group of a space from the fundamental groups of its constituents. We develop a modular SVK framework within the setting of c…
A Modular Lean 4 Framework for Confluence and Strong Normalization of Lambda Calculi with Products and Sums
Arthur Ramos, Anjolina Oliveira, Ruy de Queiroz +1
We present Metatheory, a comprehensive library for programming language foundations in Lean 4. The library features a modular framework for proving confluence of abstract rewriting…
Computational Paths Form a Weak ω-Groupoid
Arthur F. Ramos, Tiago M. L. de Veras, Ruy J. G. B. de Queiroz +1
Lumsdaine (2010) and van den Berg-Garner (2011) proved that types in Martin-Löf type theory carry the structure of weak ω-groupoids. Their proofs, while foundational, rely on abstr…
Formalizing Computational Paths and Fundamental Groups in Lean
Arthur F. Ramos, Anjolina G. de Oliveira, Ruy J. G. B. de Queiroz +1
Computational paths treat propositional equality as explicit paths built from labelled deduction steps and rewrite rules. This view originates in work by de Queiroz and collaborato…