Below are some of my selected research and educational projects.

Research

[DSoftKI]: Scalable Gaussian process that fits full derivative observations.

[SoftKI]: Scalable Gaussian process for high-dimensional regression.

[MadGP]: AI surrogate models for modeling atomic potential energy surfaces.

[PusH]: Bayesian deep learning with concurrent GPU programming.

[Gamepad]: Theorem proving with neural networks (neuro-symbolic).

[Augurv2]: A probabilistic programming language that compiles to GPUs.

[VSafecode]: Formal verification of SAFECode for LLVM memory safety.

Educational

[The Annotated Hamiltonian]: An introduction to analog quantum computing.

[The Annotated Qubit]: An introduction to quantum computing and information.

[The Annotated GP]: An introduction to Gaussian processes.

[PAPL]: An introductory course on programming and programming languages.

[FMS]: Formal models and semantics course in the Coq proof assistant.