| Publication | Date of Publication | Type |
|---|
| Verifying software emulation of an unsupported hardware instruction | 2026-02-10 | Paper |
Towards a scalable proof engine: a performant Prototype rewriting primitive for Coq
Journal of Automated Reasoning | 2024-09-27 | Paper |
| Automatic test-case reduction in proof assistants: a case study in Coq | 2024-07-15 | Paper |
| Accelerating verified-compiler development with a verified rewriting engine | 2024-07-15 | Paper |
Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs
Automated Reasoning | 2022-11-09 | Paper |
Computable decision making on the reals and other spaces. Via partiality and nondeterminism
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-20 | Paper |
Mostly automated formal verification of loop dependencies with applications to distributed stencil algorithms
Journal of Automated Reasoning | 2019-02-18 | Paper |
| Reification by parametricity -- fast setup for proof by reflection, in two lines of \textsc{Ltac} | 2018-10-04 | Paper |
| Modular deductive verification of multiprocessor hardware designs | 2018-03-01 | Paper |
A program optimization for automatic database result caching
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages | 2017-10-20 | Paper |
Fiat: deductive synthesis of abstract data types in a proof assistant
Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2016-09-29 | Paper |
A verified compiler for an impure functional language
Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-06-11 | Paper |
Parametric higher-order abstract syntax for mechanized semantics
Proceedings of the 13th ACM SIGPLAN international conference on Functional programming | 2015-03-16 | Paper |
Effective interactive proofs for higher-order imperative programs
Proceedings of the 14th ACM SIGPLAN international conference on Functional programming | 2015-01-06 | Paper |
Compositional computational reflection
Interactive Theorem Proving | 2014-09-08 | Paper |
Experience implementing a performant category-theory library in Coq
Interactive Theorem Proving | 2014-09-08 | Paper |
| scientific article; zbMATH DE number 6296049 (Why is no real title available?) | 2014-05-16 | Paper |
| An introduction to programming and proving with dependent types in Coq | 2011-02-10 | Paper |
Modular development of certified program verifiers with a proof assistant,
Journal of Functional Programming | 2008-12-18 | Paper |
Verification, Model Checking, and Abstract Interpretation
Lecture Notes in Computer Science | 2007-02-12 | Paper |
Static Analysis
Lecture Notes in Computer Science | 2005-08-24 | Paper |
