A Verified Implementation of the Berlekamp–Zassenhaus Factorization Algorithm

Referencias bibliográficas

• Abbott, J.: Bounds on factors in $$Z[x]$$. J. Symb. Comput. 50, 532–563 (2013)
• Axler, S.J.: Linear Algebra Done Right. Undergraduate Texts in Mathematics. Springer, Berlin (1997)
• Ballarin, C.: Locales: a module system for mathematical theories. J. Autom. Reason. 52(2), 123–153 (2014)
• Barthe, G., Grégoire, B., Heraud, S., Olmedo, F., Béguelin, S.Z.: Verified indifferentiable hashing into elliptic curves. In: Degano, P., Guttman, J.D. (eds.) Principles of Security and Trust. POST 2012, Volume 7215 of LNCS, pp. 209–228. Springer, Berlin (2012)
• Berlekamp, E.R.: Factoring polynomials over finite fields. Bell Syst. Tech. J. 46(8), 1853–1859 (1967)
• Blanchette, J.C., Meier, F., Popescu, A., Traytel, D.: Foundational nonuniform (co)datatypes for higher-order logic. In: ACM/IEEE Symposium on Logic in Computer Science, LICS 32, pp. 1–12. IEEE Computer Society (2017). Cross-type induction is explained in Appendix D of the extended report version at http://matryoshka.gforge.inria.fr/pubs/nonuniform_report.pdf
• Bottesch, R., Haslbeck, M.W., Thiemann, R.: A verified efficient implementation of the LLL basis reduction algorithm. In: Barthe, G., Sutcliffe, G., Veanes, M. (eds.) Logic for Programming, Artificial Intelligence and Reasoning. LPAR 22, Volume 57 of EPiC Series in Computing, pp. 164–180. EasyChair (2018)
• Cantor, D.G., Zassenhaus, H.: A new algorithm for factoring polynomials over finite fields. Math. Comput. 36(154), 587–592 (1981)
• Cerlienco, L., Mignotte, M., Piras, F.: Computing the measure of a polynomial. J. Symb. Comput. 4(1), 21–33 (1987)
• Divasón, J., Joosten, S.J.C., Thiemann, R., Yamada, A.: A formalization of the Berlekamp–Zassenhaus factorization algorithm. In: Bertot, Y., Vafeiadis, V. (eds.) Certified Programs and Proofs. CPP 2017, pp. 17–29. ACM (2017)
• Divasón, J., Joosten, S.J.C., Thiemann, R., Yamada, A.: A formalization of the LLL basis reduction algorithm. In: Avigad, J., Mahboubi, A. (eds.) Interactive Theorem Proving. ITP 2018, Volume 10895 of LNCS, pp. 160–177. Springer, Berlin (2018)
• Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) Functional and Logic Programming. FLOPS 2010, Volume 6009 of LNCS, pp. 103–117. Springer, Berlin (2010)
• Harrison, J.: The HOL light theory of Euclidean space. J. Autom. Reason. 50(2), 173–190 (2013)
• van Hoeij, M.: Factoring polynomials and the knapsack problem. J. Number Theory 95(2), 167–189 (2002)
• Huffman, B., Kunčar, O.: Lifting and transfer: a modular design for quotients in Isabelle/HOL. In: Certified Programs and Proofs. CPP 2013, Volume 8307 of LNCS, pp. 131–146. Springer, Berlin (2013)
• Karatsuba, A., Ofman, Y.: Multiplication of multidigit numbers on automata. Sov. Phys. Dokl. 7(7), 595–596 (1963)
• Kirkels, B.: Irreducibility certificates for polynomials with integer coefficients. Master’s thesis, Radboud Universiteit Nijmegen (2004)
• Knuth, D.E.: The Art of Computer Programming, Volume 2: Seminumerical Algorithms, 3rd edn. Addison-Wesley, Reading (1998)
• Kobayashi, H., Suzuki, H., Ono, Y.: Formalization of Hensel’s lemma. In: Hurd, J., Smith, E., Darbari, A. (eds.) Theorem Proving in Higher Order Logics: Emerging Trends Proceedings, pp. 114–118. Oxford University Computing Laboratory (2005)
• Krauss, A.: Recursive definitions of monadic functions. In: Bove, A., Komendantskaya, E., Niqui, M. (eds.) Partiality and Recursion in Interactive Theorem Provers. PAR 2010, Volume 43 of EPTCS, pp. 1–13 (2010)
• Kunčar, O., Popescu, A.: From types to sets by local type definition in higher-order logic. J. Autom. Reason. 62(2), 237–260 (2019)
• Lee, H.: Vector spaces. Archive of Formal Proofs, Formal proof development. http://isa-afp.org/entries/VectorSpace.html (2014)
• Lenstra, A.K., Lenstra, H.W., Lovász, L.: Factoring polynomials with rational coefficients. Math. Ann. 261, 515–534 (1982)
• Lochbihler, A.: Fast machine words in Isabelle/HOL. In: Avigad, J., Mahboubi, A. (eds.) Interactive Theorem Proving. ITP 2018, Volume 10895 of LNCS, pp. 388–410. Springer, Berlin (2018)
• Maple 2017.3. Maplesoft, a division of Waterloo Maple Inc. Waterloo (2017)
• Martin-Dorel, É., Hanrot, G., Mayero, M., Théry, L.: Formally verified certificate checkers for hardest-to-round computation. J. Autom. Reason. 54(1), 1–29 (2015)
• Mignotte, M.: An inequality about factors of polynomials. Math. Comput. 28(128), 1153–1157 (1974)
• Miola, A., Yun, D.Y.: Computational aspects of Hensel-type univariate polynomial greatest common divisor algorithms. ACM SIGSAM Bull. 8(3), 46–54 (1974)
• Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic, Volume 2283 of LNCS. Springer, Berlin (2002)
• Thiemann, R.: Computing n-th roots using the Babylonian method. Archive of Formal Proofs, Formal proof development. http://isa-afp.org/entries/Sqrt_Babylonian.html (2013)
• Thiemann, R., Yamada, A.: Algebraic numbers in Isabelle/HOL. In: Blanchette, J., Merz, S. (eds.) Interactive Theorem Proving. ITP 2016, Volume 9807 of LNCS, pp. 391–408. Springer, Berlin (2016)
• Thiemann, R., Yamada, A.: Formalizing Jordan normal forms in Isabelle/HOL. In: Avigad, J., Chlipala, A. (eds.) Certified Programs and Proofs. CPP 2016, pp. 88–99. ACM (2016)
• von zur Gathen, J., Gerhard, J.: Modern Computer Algebra, 3rd edn. Cambridge University Press, Cambridge (2013)
• Mathematica Version 11.2. Wolfram Research, Inc. Champaign (2017)
• Yun, D.Y.: On square-free decomposition algorithms. In: Symbolic and Algebraic Computation. SYMSAC 1976, pp. 26–35. ACM (1976)
• Zassenhaus, H.: On Hensel factorization, I. J. Number Theory 1(3), 291–311 (1969)