Publicaciones en las que colabora con René Thiemann (12)

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

2021

  1. Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation

    Archive of Formal Proofs, pp. 1-418

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. A verified LLL algorithm

    Archive of Formal Proofs, pp. 1-251

  4. A verified factorization algorithm for integer polynomials with polynomial complexity

    Archive of Formal Proofs, pp. 1-80

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

2016

  1. Perron-Frobenius Theorem for Spectral Radius Analysis

    Archive of Formal Proofs, pp. 1-132

  2. The Factorization Algorithm of Berlekamp and Zassenhaus

    Archive of Formal Proofs, pp. 1-481