Larry Darryl Lee Jr.

functional-algebra. This package provides a Coq formalization of abstract algebra using a functional programming style. The modules contained within the package span monoids, groups, rings, and fields and provides both axiom definitions for these structures and proofs of foundational results. The current package contains over 800 definitions and proofs.

pigeons. A proof of the Pigeonhole principle. The Pigeonhole principle is a fundamental theorem that is used widely in Computer Science and Combinatorics, it asserts that if you put n things into m containers, and n > m, then at least one of the containers contains more than one thing.

soaring. A collection of mathematical models, data sets, and data collection utilities related to the wonderful sport of Soaring.

ocaml_constraints_essay. This package contains an essay that I wrote explaining how to use OCaml's GADTs and Monads to represent and enforce constraints and to represent and track assumptions within statistical analysis and numerical programs.