[10] Arthur Charguéraud, Adam Chlipala, Andres Erbsen, and Samuel Gruetter. Omnisemantics: Smooth Handling of Nondeterminism. September 2022.
bib | pdf ]
[9] Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Andrew Wright, and Adam Chlipala. A Multipurpose Formal RISC-V Specification. 2021.
bib | arXiv | pdf ]
[8] Samuel Gruetter. Counterexamples for Coq Conjectures. CoqPL'19, January 2019.
bib | pdf ]
[7] Samuel Gruetter and Toby C. Murray. VST-Flow: Fine-grained low-level reasoning about real-world C code. Technical report, University of Melbourne, September 2017.
bib | pdf ]
[6] Samuel Gruetter. Improving the Coq proof automation tactics of the Verified Software Toolchain, based on a case study on verifying a C implementation of the AES encryption algorithm. MSc thesis, EPFL/Princeton University, April 2017.
bib | pdf ]
[5] Samuel Gruetter. Connecting Scala to DOT. MSc semester project, EPFL, June 2016.
bib | pdf ]
[4] Samuel Gruetter. Dependent Object Types With Existential Quantification Over Objects. Research report, EPFL, July 2015.
bib | pdf ]
[3] Samuel Gruetter. Improving Leon's Termination Checker. Project report, EPFL, June 2015.
bib | pdf ]
[2] Samuel Gruetter. Machine-checked typesafety proofs. MSc semester project, EPFL, June 2014.
bib | pdf ]
[1] Samuel Gruetter. Explorations of type systems. BSc semester project, EPFL, June 2013.
bib | pdf ]