{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,2]],"date-time":"2026-06-02T20:05:48Z","timestamp":1780430748299,"version":"3.54.1"},"reference-count":27,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2027,4,10]],"date-time":"2027-04-10T00:00:00Z","timestamp":1807315200000},"content-version":"am","delay-in-days":313,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-017"},{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"},{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-012"},{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T00:00:00Z","timestamp":1780272000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-004"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Journal of Logical and Algebraic Methods in Programming"],"published-print":{"date-parts":[[2026,6]]},"DOI":"10.1016\/j.jlamp.2026.101127","type":"journal-article","created":{"date-parts":[[2026,4,2]],"date-time":"2026-04-02T16:02:10Z","timestamp":1775145730000},"page":"101127","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["Nothing new under the sum: A formal model of fast Fourier algorithms"],"prefix":"10.1016","volume":"150","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-3774-0029","authenticated-orcid":false,"given":"William","family":"Scarbro","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sanjay","family":"Rajopadhye","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/j.jlamp.2026.101127_bib0001","series-title":"To H. B. Curry: essays on Combinatory Logic, Lambda Calculus and Formalism","first-page":"479","article-title":"The formulae-as-types notion of construction","author":"Howard","year":"1980"},{"key":"10.1016\/j.jlamp.2026.101127_bib0002","series-title":"Software Foundations","author":"Pierce","year":"2024"},{"key":"10.1016\/j.jlamp.2026.101127_bib0003","series-title":"Studies in Logic and the Foundations of Mathematics. Logic, Methodology and Philosophy of Science, VI (Hannover, 1979)","first-page":"153","article-title":"Constructive mathematics and computer programming","volume":"104","author":"Martin-L\u00f6f","year":"1982"},{"key":"10.1016\/j.jlamp.2026.101127_bib0004","series-title":"Automated Deduction \u2013 CADE-25","first-page":"378","article-title":"The Lean Theorem Prover (System Description)","volume":"9195","author":"de Moura","year":"2015"},{"key":"10.1016\/j.jlamp.2026.101127_bib0005","unstructured":"P. Wadler, W. Kokke, J.G. Siek, Programming Language Foundations in Agda, 2022. https:\/\/plfa.inf.ed.ac.uk\/22.08\/."},{"key":"10.1016\/j.jlamp.2026.101127_bib0006","series-title":"Types and Programming Languages","author":"Pierce","year":"2002"},{"key":"10.1016\/j.jlamp.2026.101127_bib0007","series-title":"Programming and Reasoning with Dependent Types","author":"Brady","year":"2021"},{"issue":"4","key":"10.1016\/j.jlamp.2026.101127_bib0008","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1109\/TAU.1970.1162132","article-title":"A linear filtering approach to the computation of discrete Fourier transform","volume":"18","author":"Bluestein","year":"1970","journal-title":"IEEE Trans. Audio Electroacoust."},{"key":"10.1016\/j.jlamp.2026.101127_bib0009","series-title":"Proceedings of the December 9\u201311, 1968, Fall Joint Computer Conference, Part I","first-page":"115","article-title":"An economical method for calculating the discrete Fourier transform","author":"Yavne","year":"1968"},{"key":"10.1016\/j.jlamp.2026.101127_bib0010","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/BF02242355","article-title":"Schnelle Multiplikation gro\u00dfer Zahlen","volume":"7","author":"Sch\u00f6nhage","year":"1971","journal-title":"Computing"},{"key":"10.1016\/j.jlamp.2026.101127_bib0011","series-title":"Progress in Cryptology \u2013 LATINCRYPT 2015","first-page":"346","article-title":"High-Performance Ideal Lattice-Based Cryptography on 8-Bit ATxmega Microcontrollers","author":"P\u00f6ppelmann","year":"2015"},{"key":"10.1016\/j.jlamp.2026.101127_bib0012","unstructured":"G. Seiler, Faster AVX2 optimized NTT multiplication for Ring-LWE lattice cryptography, 2018, (Cryptology ePrint Archive, Paper 2018\/039). https:\/\/eprint.iacr.org\/2018\/039."},{"key":"10.1016\/j.jlamp.2026.101127_bib0013","series-title":"Algebra","author":"Artin","year":"2015"},{"issue":"11","key":"10.1016\/j.jlamp.2026.101127_bib0014","doi-asserted-by":"crossref","first-page":"1935","DOI":"10.1109\/JPROC.2018.2873289","article-title":"SPIRAL: extreme performance portability","volume":"106","author":"Franchetti","year":"2018","journal-title":"Proc. IEEE"},{"key":"10.1016\/j.jlamp.2026.101127_bib0015","series-title":"Proceedings 35th Annual Symposium on Foundations of Computer Science","first-page":"124","article-title":"Algorithms for quantum computation: discrete logarithms and factoring","author":"Shor","year":"1994"},{"key":"10.1016\/j.jlamp.2026.101127_bib0016","unstructured":"J.W. Cooley, J.W. Tukey, An Algorithm for the Machine Calculation of Complex Fourier Series, 1965. https:\/\/www.jstor.org\/stable\/2003354?seq=1&cid=pdf-."},{"key":"10.1016\/j.jlamp.2026.101127_bib0017","series-title":"Fourth Annual ACM Symposium on Theory of Computing","article-title":"Polynomial evaluation via the division algorithm: the fast Fourier transform revisited","author":"Fiduccia","year":"1972"},{"key":"10.1016\/j.jlamp.2026.101127_bib0018","unstructured":"D.J. Bernstein, Multidigit multiplication for mathematicians, 2001."},{"key":"10.1016\/j.jlamp.2026.101127_bib0019","series-title":"Symposium on Theory of Computing","first-page":"84","article-title":"On Lattices, Learning With Errors, Random Linear Codes, and Cryptography","author":"Regev","year":"2005"},{"key":"10.1016\/j.jlamp.2026.101127_bib0020","series-title":"Proceedings - 3rd IEEE European Symposium on Security and Privacy, EURO S and P 2018","first-page":"353","article-title":"CRYSTALS - Kyber: a CCA-secure module-lattice-based KEM","author":"Bos","year":"2018"},{"key":"10.1016\/j.jlamp.2026.101127_bib0021","series-title":"Post-Quantum Cryptography","first-page":"234","article-title":"Fast NEON-Based Multiplication for Lattice-Based NIST Post-quantum Cryptography Finalists","author":"Nguyen","year":"2021"},{"issue":"17","key":"10.1016\/j.jlamp.2026.101127_bib0022","doi-asserted-by":"crossref","DOI":"10.1587\/elex.17.20200234","article-title":"A pure hardware implementation of CRYSTALS-KYBER PQC algorithm through resource reuse","volume":"17","author":"Huang","year":"2020","journal-title":"IEICE Electron. Express"},{"key":"10.1016\/j.jlamp.2026.101127_bib0023","series-title":"Proceedings of the 16th International Workshop on Cryptographic Hardware and Embedded Systems \u2014 CHES 2014 - Volume 8731","first-page":"371","article-title":"Compact Ring-LWE Cryptoprocessor","author":"Roy","year":"2014"},{"key":"10.1016\/j.jlamp.2026.101127_bib0024","unstructured":"D. Coppersmith, An approximate Fourier transform useful in quantum factoring, 1994."},{"key":"10.1016\/j.jlamp.2026.101127_bib0025","series-title":"The Calculi of Lambda-Conversion","author":"Church","year":"1941"},{"key":"10.1016\/j.jlamp.2026.101127_bib0026","series-title":"Categories for the Working Mathematician: second Edition","author":"Lane","year":"1998"},{"key":"10.1016\/j.jlamp.2026.101127_bib0027","unstructured":"W. Scarbro, TCG2, 2025. Software Heritage persistent identifier: swh:1:dir:c7e0dc1c6f28d4e093c85e7a35e56dff7f9b8553."}],"container-title":["Journal of Logical and Algebraic Methods in Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2352220826000192?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S2352220826000192?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,6,2]],"date-time":"2026-06-02T19:24:23Z","timestamp":1780428263000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S2352220826000192"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,6]]},"references-count":27,"alternative-id":["S2352220826000192"],"URL":"https:\/\/doi.org\/10.1016\/j.jlamp.2026.101127","relation":{},"ISSN":["2352-2208"],"issn-type":[{"value":"2352-2208","type":"print"}],"subject":[],"published":{"date-parts":[[2026,6]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Nothing new under the sum: A formal model of fast Fourier algorithms","name":"articletitle","label":"Article Title"},{"value":"Journal of Logical and Algebraic Methods in Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.jlamp.2026.101127","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2026 Elsevier Inc. All rights are reserved, including those for text and data mining, AI training, and similar technologies.","name":"copyright","label":"Copyright"}],"article-number":"101127"}}