Unified program generation and verification: a case study on number-theoretic transform

DOI10.1007/978-3-030-99461-7_8OpenAlexW4285123129MaRDI QIDQ2163165

Masahiro Masuda, Yukiyoshi Kameyama

Publication date: 10 August 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-99461-7_8

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic programming (68N17)

Uses Software

• Strymonas
• HACL*
• Jasmin

Cites Work

• Unnamed Item
• Unnamed Item
• Decision procedures. An algorithmic point of view
• Speeding up the number theoretic transform for faster ideal lattice-based cryptography
• FFT program generation for ring LWE-based cryptography
• Modular Multiplication Without Trial Division
• On Ideal Lattices and Learning with Errors over Rings
• Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages
• Software Speed Records for Lattice-Based Signatures
• Stream fusion, to completeness
• LMS-Verify: abstraction without regret for verified systems programming
• Formal Methods in Computer-Aided Design
• The correctness of the fast Fourier transform: A structured proof in ACL2

This page was built for publication: Unified program generation and verification: a case study on number-theoretic transform