4 citations · 7 across the 6 of their papers we have counts for
5 papers · 1 filter
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…
An alternative approach to the calculation of fundamental groups based on labeled natural deduction
Tiago M. L. de Veras, Arthur F. Ramos, Ruy J. G. B. de Queiroz +1
In this work, we use a labelled deduction system based on the concept of computational paths (sequence of rewrites) as equalities between two terms of the same type. We also define…