Quantum Algorithms in Lean
Formalizing and verifying textbook quantum algorithms in the query-combinator model
Tanner Duve
Latest posts
Currying in Categories
Cartesian closed categories and the Curry-Howard correspondence
Partiality in a Total Type Theory
Modeling divergence and nontermination in Lean
Foundations of Algorithmic Randomness and Computability
An introduction to computability theory, Turing degrees, and randomness
The Free Monad
A three-part series on free monads in Lean
Verified Dynamic Programming with Σ-types in Lean
Solving a competitive programming problem and proving it correct with dependent types