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
Coq code

A. A. Borges and J. J. Joosten
Strictly Positive Fragments of the Provability Logic of Heyting Arithmetic
arXiv:2312.14727 [math.LO]

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

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)

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
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

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

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

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


A. A. Borges
Suitable logics: provability, temporal laws, and formalization
PhD Thesis, Universitat de Barcelona

A. A. Borges
On the herbrandised interpretation for nonstandard arithmetic
Master’s Thesis, Universidade de Lisboa