{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:57:15Z","timestamp":1743141435606,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030994600"},{"type":"electronic","value":"9783030994617"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-030-99461-7_8","type":"book-chapter","created":{"date-parts":[[2022,5,2]],"date-time":"2022-05-02T23:02:40Z","timestamp":1651532560000},"page":"133-151","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Unified Program Generation and\u00a0Verification: A Case Study on\u00a0Number-Theoretic Transform"],"prefix":"10.1007","author":[{"given":"Masahiro","family":"Masuda","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yukiyoshi","family":"Kameyama","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,5,3]]},"reference":[{"unstructured":"ANSI\/ISO C specification language. https:\/\/frama-c.com\/html\/acsl.html","key":"8_CR1"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/978-3-540-30494-4_4","volume-title":"Formal Methods in Computer-Aided Design","author":"B Akbarpour","year":"2004","unstructured":"Akbarpour, B., Tahar, S.: A methodology for the formal verification of FFT algorithms in HOL. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 37\u201351. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30494-4_4"},{"unstructured":"Alkim, E., Ducas, L., P\u00f6ppelmann, T., Schwabe, P.: Post-quantum key exchange: a new hope. In: Proceedings of the 25th USENIX Conference on Security Symposium, SEC 2016, pp. 327\u2013343. USENIX Association, USA (2016)","key":"8_CR3"},{"doi-asserted-by":"publisher","unstructured":"Almeida, J.B., et al.: Jasmin: high-assurance and high-speed cryptography. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, pp. 1807\u20131823. Association for Computing Machinery, New York (2017). https:\/\/doi.org\/10.1145\/3133956.3134078","key":"8_CR4","DOI":"10.1145\/3133956.3134078"},{"doi-asserted-by":"publisher","unstructured":"Amin, N., Rompf, T.: LMS-Verify: abstraction without regret for verified systems programming. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 18\u201320 January 2017. pp. 859\u2013873. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009867","key":"8_CR5","DOI":"10.1145\/3009837.3009867"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/3-540-47721-7_24","volume-title":"Advances in Cryptology \u2014 CRYPTO\u2019 86","author":"P Barrett","year":"1987","unstructured":"Barrett, P.: Implementing the rivest shamir and adleman public key encryption algorithm on a standard digital signal processor. In: Odlyzko, A.M. (ed.) CRYPTO 1986. LNCS, vol. 263, pp. 311\u2013323. Springer, Heidelberg (1987). https:\/\/doi.org\/10.1007\/3-540-47721-7_24"},{"unstructured":"B\u00fchler, D.: Structuring an abstract interpreter through value and state abstractions: EVA, an LC. (Structurer un interpr\u00e9teur abstrait au moyen d\u2019abstractions de valeurs et d\u2019\u00e9tats: Eva, une analyse de valeur \u00e9volu\u00e9e pour Frama-C). Ph.D. thesis, University of Rennes 1, France (2017), https:\/\/tel.archives-ouvertes.fr\/tel-01664726","key":"8_CR7"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/3-540-44755-5_12","volume-title":"Theorem Proving in Higher Order Logics","author":"V Capretta","year":"2001","unstructured":"Capretta, V.: Certifying the fast fourier transform with Coq. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 154\u2013168. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44755-5_12"},{"issue":"5","key":"8_CR9","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1017\/S0956796809007205","volume":"19","author":"J Carette","year":"2009","unstructured":"Carette, J., Kiselyov, O., Shan, C.: Finally tagless, partially evaluated: tagless staged interpreters for simpler typed languages. J. Funct. Program. 19(5), 509\u2013543 (2009). https:\/\/doi.org\/10.1017\/S0956796809007205","journal-title":"J. Funct. Program."},{"key":"8_CR10","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"2009","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. The MIT Press, Cambridge (2009)","edition":"3"},{"doi-asserted-by":"publisher","unstructured":"Erbsen, A., Philipoom, J., Gross, J., Sloan, R., Chlipala, A.: Simple high-level code for cryptographic arithmetic - with proofs, without compromises. In: 2019 IEEE Symposium on Security and Privacy, SP 2019, San Francisco, CA, USA, 19\u201323 May 2019, pp. 1202\u20131219. IEEE (2019). https:\/\/doi.org\/10.1109\/SP.2019.00005","key":"8_CR11","DOI":"10.1109\/SP.2019.00005"},{"doi-asserted-by":"crossref","unstructured":"Gamboa, R.A.: The correctness of the fast fourier transform: a structured proof in ACL2. Form. Methods Syst. Des. 20(1), 91\u2013106 (2002). https:\/\/doi.org\/10.1023\/A:1012912614285","key":"8_CR12","DOI":"10.1023\/A:1012912614285"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-642-38616-9_5","volume-title":"Post-Quantum Cryptography","author":"T G\u00fcneysu","year":"2013","unstructured":"G\u00fcneysu, T., Oder, T., P\u00f6ppelmann, T., Schwabe, P.: Software speed records for lattice-based signatures. In: Gaborit, P. (ed.) PQCrypto 2013. LNCS, vol. 7932, pp. 67\u201382. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38616-9_5"},{"doi-asserted-by":"publisher","unstructured":"Kiselyov, O., Biboudis, A., Palladinos, N., Smaragdakis, Y.: Stream fusion, to completeness. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pp. 285\u2013299. Association for Computing Machinery, New York (2017). https:\/\/doi.org\/10.1145\/3009837.3009880","key":"8_CR14","DOI":"10.1145\/3009837.3009880"},{"doi-asserted-by":"publisher","unstructured":"Krishnaswami, N.R., Yallop, J.: A typed, algebraic approach to parsing. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, pp. 379\u2013393. Association for Computing Machinery, New York (2019). https:\/\/doi.org\/10.1145\/3314221.3314625","key":"8_CR15","DOI":"10.1145\/3314221.3314625"},{"doi-asserted-by":"publisher","unstructured":"Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View, Second Edition. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-50497-0","key":"8_CR16","DOI":"10.1007\/978-3-662-50497-0"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-319-48965-0_8","volume-title":"Cryptology and Network Security","author":"P Longa","year":"2016","unstructured":"Longa, P., Naehrig, M.: Speeding up the number theoretic transform for faster ideal lattice-based cryptography. In: Foresti, S., Persiano, G. (eds.) CANS 2016. LNCS, vol. 10052, pp. 124\u2013139. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48965-0_8"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-13190-5_1","volume-title":"Advances in Cryptology \u2013 EUROCRYPT 2010","author":"V Lyubashevsky","year":"2010","unstructured":"Lyubashevsky, V., Peikert, C., Regev, O.: On ideal lattices and learning with errors over rings. In: Gilbert, H. (ed.) EUROCRYPT 2010. LNCS, vol. 6110, pp. 1\u201323. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13190-5_1"},{"key":"8_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-030-85987-9_9","volume-title":"Advances in Information and Computer Security","author":"M Masuda","year":"2021","unstructured":"Masuda, M., Kameyama, Y.: FFT program generation for ring LWE-based cryptography. In: Nakanishi, T., Nojima, R. (eds.) IWSEC 2021. LNCS, vol. 12835, pp. 151\u2013171. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85987-9_9"},{"key":"8_CR20","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1090\/S0025-5718-1985-0777282-X","volume":"44","author":"PL Montgomery","year":"1985","unstructured":"Montgomery, P.L.: Modular multiplication without trial division. Math. Comput. 44, 519\u2013521 (1985)","journal-title":"Math. Comput."},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-030-63618-0_9","volume-title":"Software Verification","author":"JA Navas","year":"2020","unstructured":"Navas, J.A., Dutertre, B., Mason, I.A.: Verification of an optimized NTT algorithm. In: Christakis, M., Polikarpova, N., Duggirala, P.S., Schrammel, P. (eds.) NSV\/VSTTE -2020. LNCS, vol. 12549, pp. 144\u2013160. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-63618-0_9"},{"doi-asserted-by":"publisher","unstructured":"Protzenko, J., et al.: Evercrypt: a fast, verified, cross-platform cryptographic provider. In: 2020 IEEE Symposium on Security and Privacy (SP), pp. 983\u20131002 (2020). https:\/\/doi.org\/10.1109\/SP40000.2020.00114","key":"8_CR22","DOI":"10.1109\/SP40000.2020.00114"},{"key":"8_CR23","first-page":"39","volume":"2018","author":"G Seiler","year":"2018","unstructured":"Seiler, G.: Faster AVX2 optimized NTT multiplication for Ring-LWE lattice cryptography. IACR Cryptol. ePrint Arch. 2018, 39 (2018)","journal-title":"IACR Cryptol. ePrint Arch."},{"doi-asserted-by":"publisher","unstructured":"Shaikhha, A., Klonatos, Y., Koch, C.: Building efficient query engines in a high-level language. ACM Trans. Database Syst. 43(1) (2018). https:\/\/doi.org\/10.1145\/3183653","key":"8_CR24","DOI":"10.1145\/3183653"},{"doi-asserted-by":"publisher","unstructured":"Wei, G., Chen, Y., Rompf, T.: Staged abstract interpreters: fast and modular whole-program analysis via meta-programming. Proc. ACM Program. Lang. 3(OOPSLA), 126:1\u2013126:32 (2019). https:\/\/doi.org\/10.1145\/3360552","key":"8_CR25","DOI":"10.1145\/3360552"},{"doi-asserted-by":"publisher","unstructured":"Zinzindohou\u00e9, J.K., Bhargavan, K., Protzenko, J., Beurdouche, B.: HACL*: a verified modern cryptographic library. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, pp. 1789\u20131806. Association for Computing Machinery, New York (2017). https:\/\/doi.org\/10.1145\/3133956.3134043","key":"8_CR26","DOI":"10.1145\/3133956.3134043"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99461-7_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,2]],"date-time":"2022-05-02T23:03:38Z","timestamp":1651532618000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99461-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030994600","9783030994617"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99461-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"3 May 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FLOPS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Functional and Logic Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Kyoto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 May 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 May 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"flops2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/flops-2022","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"50% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}