Author of the publication

Normalization by evaluation for sized dependent types.

, , and . Proc. ACM Program. Lang., 1 (ICFP): 33:1-33:30 (2017)

Please choose a person to relate this publication to

To differ between persons with the same name, the academic degree and the title of an important publication will be displayed. You can also use the button next to the name to display some publications already assigned to the person.

 

Other publications of authors with the same name

Eliminating reflection from type theory., , and . CPP, page 91-103. ACM, (2019)From Rewrite Rules to Axioms in the $\varPi $-Calculus Modulo Theory., , , and . FoSSaCS (2), volume 14575 of Lecture Notes in Computer Science, page 3-23. Springer, (2024)Randomized Mixed-Radix Scalar Multiplication., , and . IACR Cryptology ePrint Archive, (2016)The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography., , , , , and . CPP, page 30-44. ACM, (2024)Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti., and . FSCD, volume 299 of LIPIcs, page 21:1-21:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, (2024)Randomizing Scalar Multiplication Using Exact Covering Systems of Congruences., , and . IACR Cryptology ePrint Archive, (2015)The MetaCoq Project., , , , , , , , and . J. Autom. Reason., 64 (5): 947-999 (2020)The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant., , , and . ITP, volume 309 of LIPIcs, page 26:1-26:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, (2024)SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq., , , , , , , and . CSF, page 1-15. IEEE, (2021)Randomized Mixed-Radix Scalar Multiplication., , and . IEEE Trans. Computers, 67 (3): 418-431 (2018)