2025
Deterministically Iterating over a set within Dafny functions
Verifying Proofs with Type Checkers
2024
Polymorphic Functions w/ Wildcard Matching in Lean 4
Functions and Inductive Propositions in Lean 4
Working with integer sets in Lean 4
Coercing Ints to Nats for Induction in Lean 4
2023
Induction in Lean 3: Three Techniques
2022
Obtaining Multiple Solutions Z3
Reasoning through Loops in Dafny
Program Verification with Hoare Logic and Dafny
2021
2019