5 papers
Topological Semantics for Scoped Computational Paths
Arthur Freitas Ramos, Ruy J. G. B. de Queiroz, Anjolina Grisi de Oliveira +1
Computational paths record equality as explicit finite traces of primitive steps. We give a topological semantics for a scoped rewrite presentation whose steps have continuous geom…
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 abs…
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…