Publications

You can also find my articles on my Google Scholar profile.

Journal articles


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

Conference papers


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

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

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

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

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

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

Theses