Introduction to FOL and SMT
Introduction to Semantic Subtyping and Recursive Types
Automation of Induction Proofs
Introduction to FOL and SMT
Introduction to Semantic Subtyping and Recursive Types
Automation of Induction Proofs
An Implementation of Pattern Matching for Lists in Emacs Lisp An Implementation of User-Defined Datatypes in Emacs Lisp
Combinatorial Game Theory (Project for CMU's Undergraduate Discrete Math Research course)
Tutorial for Haskell's "brick" CUI Library
Tutorial for Haskell's "scotty" Server Framework
Visualzing Schedule Goals with Haskell's "diagrams" Library
Proving walk(v,w) ⇒ path(v,w) for Graphs in Lean
(Project for CMU's Interactive Theorem Proving course)
Modeling a Rubik's Cube in Lean
(Project for CMU's Interactive Theorem Proving course)