Coq mechanization of Richard Bird's Introduction to a Theory of Lists. Completed under the mentorship of Stephanie Weirich and Jessica Shi at University of Pennsylvania.
Theoretical papers by Bird: https://www.cs.ox.ac.uk/files/3378/PRG56.pdf https://www.cs.tufts.edu/~nr/cs257/archive/richard-bird/sudoku.pdf