@inproceedings{10.1145/3133956.3134078,
author = {Almeida, Jos\'{e} Bacelar and Barbosa, Manuel and Barthe, Gilles and Blot, Arthur and Gr\'{e}goire, Benjamin and Laporte, Vincent and Oliveira, Tiago and Pacheco, Hugo and Schmidt, Benedikt and Strub, Pierre-Yves},
title = {Jasmin: High-Assurance and High-Speed Cryptography},
year = {2017},
isbn = {9781450349468},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
doi = {10.1145/3133956.3134078},
abstract = {Jasmin is a framework for developing high-speed and high-assurance cryptographic software.
The framework is structured around the Jasmin programming language and its compiler.
The language is designed for enhancing portability of programs and for simplifying
verification tasks. The compiler is designed to achieve predictability and efficiency
of the output code (currently limited to x64 platforms), and is formally verified
in the Coq proof assistant. Using the supercop framework, we evaluate the Jasmin compiler
on representative cryptographic routines and conclude that the code generated by the
compiler is as efficient as fast, hand-crafted, implementations. Moreover, the framework
includes highly automated tools for proving memory safety and constant-time security
(for protecting against cache-based timing attacks). We also demonstrate the effectiveness
of the verification tools on a large set of cryptographic routines.},
booktitle = {Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security},
pages = {1807–1823},
numpages = {17},
keywords = {constant-time security, safety, cryptographic implementations, verified compiler},
location = {Dallas, Texas, USA},
series = {CCS '17}
}


@inproceedings{hal/01238879,
  author = {Leroy, Xavier and Blazy, Sandrine and K\"astner, Daniel
            and Schommer, Bernhard and Pister, Markus and Ferdinand, Christian},
  title = {CompCert -- A Formally Verified Optimizing Compiler},
  booktitle = {ERTS 2016: Embedded Real Time Software and Systems},
  publisher = {SEE},
  year = 2016,
  url = {https://hal.inria.fr/hal-01238879},
  xtopic = {compcert},
  abstract = {CompCert is the first commercially available
optimizing compiler that is formally verified, using machine-assisted
mathematical proofs, to be exempt from mis-compilation.
The executable code it produces is proved
to behave exactly as specified by the semantics of the
source C program. This article gives an overview of
the design of CompCert and its proof concept and then
focuses on aspects relevant for industrial application.
We briefly summarize practical experience and give an
overview of recent CompCert development aiming at industrial usage.
CompCert’s intended use is the compilation of life-critical
and mission-critical software meeting high levels of assurance.
In this context tool qualification is of paramount importance. We
summarize the confidence argument of CompCert and give an overview of
relevant qualification strategies.}
}

@article{10.46586/tches.v2022.i1.482-505,
author={Becker, Hanno and Bermudo Mera, Jose Maria and Karmakar, Angshuman and Yiu, Joseph and Verbauwhede, Ingrid},
title={Polynomial multiplication on embedded vector architectures},
journal={IACR Transactions on Cryptographic Hardware and Embedded Systems},
publisher={Ruhr-Universität Bochum},
volume={2022, Issue 1},
pages={482-505},
doi={10.46586/tches.v2022.i1.482-505},
year=2021
}

@manual{arm/DDI0553B.s,
title = {Armv8-M Architecture Reference Manual},
author = {{Arm Limited}},
shortauthor = {Arm},
date = {2022-04-01},
version = {B.s},
organsization = {Arm Limited},
url = {https://developer.arm.com/documentation/ddi0553/bs/},
}

@InProceedings{10.1007/978-3-642-03359-9_6,
author="Bove, Ana
and Dybjer, Peter
and Norell, Ulf",
editor="Berghofer, Stefan
and Nipkow, Tobias
and Urban, Christian
and Wenzel, Makarius",
title="A Brief Overview of Agda -- A Functional Language with Dependent Types",
booktitle="Theorem Proving in Higher Order Logics",
date="2009",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="73--78",
abstract="We give an overview of Agda, the latest in a series of dependently typed programming languages developed in Gothenburg. Agda is based on Martin-L{\"o}f's intuitionistic type theory but extends it with numerous programming language features. It supports a wide range of inductive data types, including inductive families and inductive-recursive types, with associated flexible pattern-matching. Unlike other proof assistants, Agda is not tactic-based. Instead it has an Emacs-based interface which allows programming by gradual refinement of incomplete type-correct terms.",
isbn="978-3-642-03359-9",
doi={10.1007/978-3-642-03359-9_6}
}