Cody Roux

name-the-biggest-number. Coq

broad-coq-tutorial. Some unstructured notes concerning the Broad tutorial to take place in March 2020

traat-lean. Lean formalization of selected lemmas from "Term Rewriting and All That"

hoare-toy. A tiny toy formalization of Hoare logic for IMP with a proof of soundness

tinymatch. A teeny language with nats, lists and pattern matching, static and dynamic semantics and a proof of progress and preservation.

knuth-bendix. A naive knuth-bendix completion implementation

simple-prolog. Lean

lean-to-python. A little metaprograming script to emit python from lean defs. Not suitable for real work.

ny-haskell. The source files for the NY Haskell Lean talk

equational_theories. A project to map out the relations between different equational theories of Magmas.

lean0.1. Snapshot of Lean 0.1, before major kernel changes in Lean 0.2. It contains a working binary, examples, and documentation.

compact-php. A proof of a finitary pigeon hole principle via compactness and the infinitary version, in Lean.

FrontC. An OCaml library providing a C parser and lexer

catnapp. the Categorical Nearly Automatic Property Prover

toy-reflect. A tiny example of reflection in lean, using quote4

NbE-experiments. Coq

stupidsat. A python interface for minisat

Strata. Lean