I'm a PhD student at MIT CSAIL, advised by Prof. Adam Chlipala.
Email: My last name at mit dot edu
Office address:
32-G886
MIT CSAIL, Stata Center
32 Vassar Street
Cambridge MA 02139
USA
Full CV: here

Research Interests

I’m interested in Programming Languages and Verification, Interactive Theorem Proving, Language Design, Compilers, Specifications, and Software Engineering.

Currently, I’m working on the Bedrock2 project. It includes a very simple C-like source language, a program logic for it, and a compiler to RISC-V machine code, as specified by riscv-coq. Another project of our group, Kami, developed a RISC-V processor and proved it correct against the same riscv-coq spec, which enabled us to prove an end-to-end theorem about the behavior of a whole software-hardware stack. The first milestone of this project is the IoT lightbulb, which we presented at PLDI’21 (see paper and video). Earlier, I also gave a talk about it at the RISC-V Summit 2019, and you can find the video recording here.

Trouble combining undefined behavior and nondeterminism? ➔ Try omnisemantics!

While working on Bedrock2, my colleague Andres Erbsen and me came up with a style of programming language semantics that we think works much better in the presence of undefined behavior and nondeterminism than using traditional smallstep or bigstep operational semantics would. A little later, our advisor Adam Chlipala chatted with Arthur Charguéraud and they found out that he had discovered the same style of semantics as well, but was using it for functional languages, while we were using it for imperative languages. Together, we wrote a paper about it, and you can find a preprint here, or if you prefer just a short introduction, you can also check out this blog post.

Past Projects

Publications

[7] Thomas Bourgeat, Ian Clester, Andres Erbsen, Samuel Gruetter, Pratap Singh, Andy Wright, and Adam Chlipala. Flexible Instruction-Set Semantics via Abstract Monads (Experience Report). Proceedings of the ACM on Programming Languages, 7(ICFP):192:108--192:124, August 2023.
DOI | PDF | code ]
[6] Arthur Charguéraud, Adam Chlipala, Andres Erbsen, and Samuel Gruetter. Omnisemantics: Smooth Handling of Nondeterminism. ACM Transactions on Programming Languages and Systems, 45(1):5:1--5:43, March 2023.
DOI | PDF | code ]
[5] Andres Erbsen, Samuel Gruetter, Joonwon Choi, Clark Wood, and Adam Chlipala. Integration Verification Across Software and Hardware for a Simple Embedded System. PLDI'21, June 2021.
DOI | PDF | code ]
[4] Qinxiang Cao, Lennart Beringer, Samuel Gruetter, Josiah Dodds, and Andrew W. Appel. VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs. Journal of Automated Reasoning, 61(1-4):367--422, June 2018.
DOI | PDF | code ]
[3] Samuel Gruetter and Toby Murray. Short Paper: Towards Information Flow Reasoning about Real-World C Code. In Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security - PLAS '17, pages 43--48, Dallas, Texas, USA, 2017. ACM Press.
DOI | PDF | code ]
[2] Samuel Gruetter, Daniel Graf, and Benjamin Schmid. Watch them Fight! Creativity Task Tournaments of the Swiss Olympiad in Informatics. Olympiads in Informatics, 10(1):73--85, July 2016.
DOI | PDF | code ]
[1] Nada Amin, Samuel Gruetter, Martin Odersky, Tiark Rompf, and Sandro Stucki. The Essence of Dependent Object Types. A List of Successes That Can Change the World: Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, pages 249--272, 2016.
DOI | PDF | code ]

Preprints and Reports

[8] Samuel Gruetter. Counterexamples for Coq Conjectures. CoqPL'19, January 2019.
PDF | code ]
[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.
PDF | code ]
[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.
PDF | code ]
[5] Samuel Gruetter. Connecting Scala to DOT. MSc semester project, EPFL, June 2016.
PDF | code ]
[4] Samuel Gruetter. Dependent Object Types With Existential Quantification Over Objects. Research report, EPFL, July 2015.
PDF | code ]
[3] Samuel Gruetter. Improving Leon's Termination Checker. Project report, EPFL, June 2015.
PDF | code ]
[2] Samuel Gruetter. Machine-checked typesafety proofs. MSc semester project, EPFL, June 2014.
PDF | code ]
[1] Samuel Gruetter. Explorations of type systems. BSc semester project, EPFL, June 2013.
PDF | code ]

Education

Industry Experience