Sotabase

Career

· Arthur J. Conner (1888) Professor of Computer Science, Massachusetts Institute of Technology2024–
· Instructor, Harvard University2008–2009
· Postdoctoral Researcher, Harvard University2008–2011
· OCaml Hacker, Jane Street Capital2007–2008
· Instructor, University of California, Berkeley2006–2006
· Research Intern, Microsoft Research Redmond2005–2005
· PhD in Computer Science, University of California, Berkeley2003–2007
· Research Assistant, University of California, Berkeley2003–2007
· BS, Computer Science, Carnegie Mellon University2000–2003

Publications (274)

Using Crash Hoare logic for certifying the FSCQ file system
USENIX Annual Technical Conference · 2015
276
cited
Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant
2013
271
cited
Generating tests from counterexamples
Proceedings. 26th International Conference on Software Engineering · 2004
237
cited
Parametric higher-order abstract syntax for mechanized semantics
ACM SIGPLAN International Conference on Functional Programming · 2008
227
cited
Mostly-automated verification of low-level programs in computational separation logic
ACM-SIGPLAN Symposium on Programming Language Design and Implementation · 2011
185
cited
Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises
IEEE Symposium on Security and Privacy · 2019
141
cited
A verified compiler for an impure functional language
ACM-SIGACT Symposium on Principles of Programming Languages · 2010
124
cited
Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant
ACM-SIGACT Symposium on Principles of Programming Languages · 2015
118
cited
The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier
ACM SIGPLAN International Conference on Functional Programming · 2013
117
cited
Kami: a platform for high-level parametric hardware specification and its modular verification
Proc. ACM Program. Lang. · 2017
113
cited
A certified type-preserving compiler from lambda calculus to assembly language
ACM-SIGPLAN Symposium on Programming Language Design and Implementation · 2007
108
cited
Static Checking of Dynamically-Varying Security Policies in Database-Backed Applications
USENIX Symposium on Operating Systems Design and Implementation · 2010
104
cited
Effective interactive proofs for higher-order imperative programs
ACM SIGPLAN International Conference on Functional Programming · 2009
101
cited
Chapar: certified causally consistent distributed key-value stores
ACM-SIGACT Symposium on Principles of Programming Languages · 2016
98
cited
Ur: statically-typed metaprogramming with type-level record computation
ACM-SIGPLAN Symposium on Programming Language Design and Implementation · 2010
97
cited
Ur/Web: A Simple Model for Programming the Web
ACM-SIGACT Symposium on Principles of Programming Languages · 2015
92
cited
The Blast Query Language for Software Verification
Sensors Applications Symposium · 2004
89
cited
Jitk: A Trustworthy In-Kernel Interpreter Infrastructure
USENIX Symposium on Operating Systems Design and Implementation · 2014
75
cited
Verifying a high-performance crash-safe file system using a tree specification
Symposium on Operating Systems Principles · 2017
75
cited
The essence of Bluespec: a core language for rule-based hardware design
ACM-SIGPLAN Symposium on Programming Language Design and Implementation · 2020
63
cited
Sotabase