Publications

A. A. Borges, M. González Bedmar, J. Conejero Rodríguez, E. Hermo Reyes, J. Casals Buñuel, and J. J. Joosten
UTC Time, Formally Verified
Certified Programs and Proofs (CPP 2024)
doi: 10.1145/3636501.3636958
2024
Coq code

A. A. Borges and J. J. Joosten
An Escape from Vardanyan’s Theorem
The Journal of Symbolic Logic 88(4): 1613-1638
doi: 10.1017/jsl.2022.38
2023

A. A. Borges , A. Casanueva Artís , J.-R. Falleri, E. J. Gallego Arias, É. Martin-Dorel, K. Palmskog, A. Serebrenik, and T. Zimmermann
Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users
14th International Conference on Interactive Theorem Proving (ITP 2023)
2023

A. A. Borges
Towards a Coq formalization of a quantified modal logic
Proceedings of the 4th Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2022): 13-27
2022
Coq code

A. A. Borges, J. J. Conejero Rodríguez, D. Fernández-Duque, M. González. Bedmar, and J. J. Joosten
To drive or not to drive: A logical and computational analysis of European transport regulations
Information and Computation 280
doi: 10.1016/j.ic.2020.104636
2021

A. A. Borges, and J. J. Joosten
Quantified Reflection Calculus with one modality
Advances in Modal Logic 13: 13-32
2020

A. A. Borges, J. J. Conejero Rodríguez, D. Fernández-Duque, M. González Bedmar, and J. J. Joosten
The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations
26th International Symposium on Temporal Representation and Reasoning (TIME 2019): 6:1-6:16
2019

A. A. Borges, and J. J. Joosten
The Worm Calculus
Advances in Modal Logic 12: 13-27
2018
This paper was partly formalized in Coq.

Theses