5 papers
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-…
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…
Exterior-Model Spinors in Split Rank: Exact Levi Images and Square-Determinant Obstructions
Arthur F. Ramos, David B. Hulak, Ruy J. G. B. de Queiroz
Let be a field with , and let denote the standard hyperbolic form on . We study the exterior spinor model together with…
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 Homotopy -Model
Daniel O. Martínez-Rivillas, Ruy J. G. B. de Queiroz
We extend the complete ordered set Dana Scott's to a complete weakly ordered Kan complex , with properties that guarantee the non-equivalence of the interpreta…