2 citations · 6 across the 3 of their papers we have counts for
3 papers
cs.SE2022★ 2 cited
UTC Time, Formally Verified
Ana de Almeida Borges, Mireia González Bedmar, Juan Conejero Rodríguez +3
FV Time is a small-scale verification project developed in the Coq proof assistant using the Mathematical Components libraries. It is a library for managing conversions between tim…
cs.LO2022★ 2 cited
Towards a Coq formalization of a quantified modal logic
Ana de Almeida Borges
We present a Coq formalization of the Quantified Reflection Calculus with one modality, or . This is a decidable, strictly positive, and quantified modal logic prev…
math.LO2021★ 2 cited
An Escape from Vardanyan's Theorem
Ana de Almeida Borges, Joost J. Joosten
Vardanyan's Theorems state that - the quantified provability logic of Peano Arithmetic - is complete, and in particular that this already holds…