Publicaciones en colaboración con investigadores/as de University of Innsbruck (8)

2022

  1. A Formalization of the Smith Normal Form in Higher-Order Logic

    Journal of Automated Reasoning

  2. Correction to: A Formalization of the Smith Normal Form in Higher-Order Logic (Journal of Automated Reasoning, (2022), 66, 4, (1065-1095), 10.1007/s10817-022-09631-5)

    Journal of Automated Reasoning

2020

  1. Formalizing the LLL Basis Reduction Algorithm and the LLL Factorization Algorithm in Isabelle/HOL

    Journal of Automated Reasoning, Vol. 64, Núm. 5, pp. 827-856

2018

  1. A Formalization of the LLL Basis Reduction Algorithm

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

  2. A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving

    WST 2018 16th International Workshop on Termination

  3. Efficient certification of complexity proofs formalizing the Perron-Frobenius theorem (invited talk paper)

    CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018

2017

  1. A formalization of the Berlekamp-Zassenhaus factorization algorithm

    CPP 2017 - Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, pp. 17-29

2008

  1. A mechanized proof of the Basic Perturbation Lemma

    Journal of Automated Reasoning, Vol. 40, Núm. 4, pp. 271-292