9 papers · 1 filter
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…
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
We present a mechanically checked Isabelle/HOL bridge from the Picard-Lindelof flow infrastructure in the Archive of Formal Proofs (AFP) to selected qualitative facts for the mass-…
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
We present a sorry-free Lean 4/mathlib4 formalization of Stokes' theorem for smooth singular cubes in arbitrary dimension, using true differential-form pullback via the Frechet der…
Token-Sensitive Enclosure Semantics for Measurement-Bearing Expressions
David B. Hulak, Arthur F. Ramos, Ruy J. G. B. de Queiroz
Token identity is semantic information for measurement-bearing expressions. Intervals, dimension tags, and token-erased syntax can say what values a measured leaf may take, but the…
Recursive Completion in Higher K-Models: Front-Seed Semantics, Proof-Relevant Witnesses, and the K-Infinity Model
Daniel O. Martinez-Rivillas, Arthur F. Ramos, Ruy J. G. B. de Queiroz
Martinez-Rivillas and de Queiroz gave extensional Kan semantics for the untyped lambda-calculus and later constructed the concrete K-infinity homotopy-model. The two main mathemati…
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…