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
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
de Almeida Borges, A. (2023). Suitable logics: provability, temporal laws, and formalization (Doctoral dissertation). University of Barcelona.
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
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
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
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
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
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
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
de Almeida Borges, A. (2016). On the herbrandised interpretation for nonstandard arithmetic (Master's thesis). Instituto Superior Técnico, Universidade de Lisboa.