Tanner Duve
Proof Engineer, Logician
Hi! I’m Tanner. I am a research engineer at Logical Intelligence, working on formal verification and compilers. I graduated from the University of Pennsylvania with an MSE in computer science and a BA in mathematical logic. My academic interests include formal verification, programming languages, category theory, type theory, and all things logic.
Previously I worked as a software engineer writing Rust at Nexus. I have done research in applied category theory with Georgios Bakirtzis and Michail Savvas, and in programming languages and formal verification with Amazon’s Automated Reasoning Group.
I am an avid user of the Lean theorem prover and I have done formalization work with Harmonic and Project Numina. Independently I have made contributions to both Mathlib and CSLib and I enjoy formalizing things related to logic and programming languages.
Outside of work I enjoy reading philosophy, in particular analytic philosophy, philosophy of mind and consciousness, metaphysics, and Eastern philosophy and mysticism. I played 2 years of D1 football at Penn and I enjoy lifting weights, yoga, and running. I am also learning guitar, and am passionate about veganism and total liberation for all beings.
Favorite PLs: Rust, OCaml, Haskell, Lean