Sitemap
A list of all the posts and pages found on the site. For you robots out there is an XML version available for digesting as well.
Pages
Posts
projects
Worms in Coq
A Coq implementation of the Worm Calculus, the closed fragment of the Reflection Calculus, and the relationship between them.
Tree automata theory in Coq
Formalization of basic concepts from tree automata theory.
Coq Gitlab templates
Configuration and other boilerplate templates for Coq projects hosted on Gitlab, adapted from coq-community’s templates project.
FormalV Library
Libraries for the conversion between Coq primitive integers and MathComp unary numbers, boolean goal automation, and UTC time management.
Coq development
Contributions to Coq.
QRC1 in Coq
A Coq formalization of the Quantified Reflection Calculus with one modality.
3, 2, 5, Can you count?
A game in which you need to count how many goats are on the screen!
publications
On the herbrandised interpretation for nonstandard arithmetic
Instituto Superior Técnico, Universidade de Lisboa, 2016
Citation: de Almeida Borges, A. (2016). On the herbrandised interpretation for nonstandard arithmetic (Master's thesis). Instituto Superior Técnico, Universidade de Lisboa.
The Worm Calculus
Advances in Modal Logic 12, 2018
Citation: de Almeida Borges, A. & Joosten, J. J. (2018). Bezhanishvili, G., D'Agostino, G., Metcalfe, G., & Studer, T. (Eds.). The Worm Calculus. Advances in Modal Logic 12 (pp. 13–27). College Publications. URL: http://www.aiml.net/volumes/volume12/deAlmeidaBorges-Joosten.pdf
The Second Order Traffic Fine: Temporal Reasoning in European Transport Regulations
26th International Symposium on Temporal Representation and Reasoning (TIME 2019), 2019
Citation: de Almeida Borges, A., Conejero Rodríguez, J., Fernández-Duque, D., González Bedmar, M., & Joosten, J. J. (2019). Gamper, J., Pinchinat, S., & Sciavicco, G. (Eds.). The second order traffic fine: temporal reasoning in European transport regulations. 26th International Symposium on Temporal Representation and Reasoning (TIME 2019) (pp. 6:1–6:16). Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. URL: https://drops.dagstuhl.de/storage/00lipics/lipics-vol147-time2019/LIPIcs.TIME.2019.6/LIPIcs.TIME.2019.6.pdf, doi:10.4230/LIPIcs.TIME.2019.6
Quantified Reflection Calculus with one modality
Advances in Modal Logic 13, 2020
Citation: de Almeida Borges, A. & Joosten, J. J. (2020). Olivetti, N., Verbrugge, R., Negri, S., & Sandu, G. (Eds.). Quantified Reflection Calculus with one modality. Advances in Modal Logic 13 (pp. 13–32). College Publications. URL: http://www.aiml.net/volumes/volume13/deAlmeidaBorges-Joosten.pdf
To drive or not to drive: A logical and computational analysis of European transport regulations
Information and Computation, 2021
Citation: de Almeida Borges, A., Conejero Rodríguez, J., Fernández-Duque, D., González Bedmar, M., & Joosten, J. J. (2021). To drive or not to drive: a logical and computational analysis of European transport regulations. Information and Computation, 280, 104636. doi:10.1016/j.ic.2020.104636
Towards a Coq formalization of a quantified modal logic
Proceedings of the 4th International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2022), 2022
Citation: de Almeida Borges, A. (2022). Benzmüller, C. & Otten, J. (Eds.). Towards a Coq formalization of a quantified modal logic. Proceedings of the 4th International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2022) (pp. 13–27). CEUR. URL: https://ceur-ws.org/Vol-3326/ARQNL2022_paper1.pdf
An Escape from Vardanyan's Theorem
The Journal of Symbolic Logic, 2023
Citation: de Almeida Borges, A. & Joosten, J. J. (2023). An escape from Vardanyan's Theorem. The Journal of Symbolic Logic, 88(4), 1613–1638. URL: https://www.cambridge.org/core/services/aop-cambridge-core/content/view/03E13D4C282563F918AF77CF6E2830DA/S002248122200038Xa.pdf/an-escape-from-vardanyans-theorem.pdf, doi:10.1017/jsl.2022.38
Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users
14th International Conference on Interactive Theorem Proving (ITP 2023), 2023
Citation: de Almeida Borges, A., Casanueva Artís, A., Falleri, J.-R., Gallego Arias, E. J., Martin-Dorel, É., Palmskog, K., Serebrenik, A., & Zimmermann, T. (2023). Naumowicz, A. & Thiemann, R. (Eds.). Lessons for interactive theorem proving researchers from a survey of Coq users. 14th International Conference on Interactive Theorem Proving (ITP 2023) (pp. 12:1–12:18). Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.12/LIPIcs.ITP.2023.12.pdf
Suitable logics: provability, temporal laws, and formalization
University of Barcelona, 2023
Citation: de Almeida Borges, A. (2023). Suitable logics: provability, temporal laws, and formalization (Doctoral dissertation). University of Barcelona.
Strictly Positive Fragments of the Provability Logic of Heyting Arithmetic
Studia Logica, 2024
Citation: de Almeida Borges, A. & Joosten, J. J. (2024). Strictly positive fragments of the provability logic of Heyting Arithmetic. Studia Logica. URL: https://link.springer.com/content/pdf/10.1007/s11225-024-10152-y.pdf
UTC Time, Formally Verified
Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’24), January 15--16, 2024, London, UK, 2024
Citation: de Almeida Borges, A., González Bedmar, M., Conejero Rodríguez, J., Hermo Reyes, E., Casals Buñuel, J., & Joosten, J. J. (2024). UTC time, formally verified. Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’24), January 15–16, 2024, London, UK (p. ). ACM. URL: https://arxiv.org/pdf/2209.14227, doi:10.1145/3636501.3636958