LogiCoC
An implementation of the calculus of constructions as a logic program
Projects
Software
Expository Papers
Graded Monoidal Categories and Internalization
A general categorical framework for internalizing graded monoidal products into classical monoidal products.
The Homotopy Hypothesis Via Kan Complexes
An introduction to model categories, used to prove the homotopy hypothesis by way of Kan complexes.
Topoi and Internal Logic in Algebraic Geometry
An expository paper on some applications of topoi and their internal logic in algebraic geometry.
Categorical Quantum Logic and the ZX-Calculus
An exposition on the ZX-calculus and its applications to quantum computing.
The Serre Spectral Sequence
An introduction to spectral sequences, and an overview of some immediate topological applications of the Serre spectral sequence.