A few open-source contributions and personal projects in Lean

Cslib

• Free Monads.¹
• Phase Semantics of Linear Logic.²

Mathlib

• Turing Degrees of Partial Recursive Functions.³

Personal projects

• zxLean – in progress formalization of the ZX-calculus for formal reasoning about quantum circuits https://github.com/tannerduve/zxLean
• zkflow – prototyping a verified pipeline from a small declarative language to zero-knowledge constraint systems, with Lean proofs for the compiler’s soundness.
  https://github.com/tannerduve/zkflow

1. Source: leanprover/cslib – Foundations/Control/Monad. ↩︎

2. Source: leanprover/cslib – LinearLogic/CLL/PhaseSemantics/Basic.lean. ↩︎

3. Source: leanprover-community/mathlib4 – Computability/TuringDegree.lean. ↩︎