14 citations · 23 across the 2 of their papers we have counts for
3 papers
cs.MS2011★ 9 cited
The MathScheme Library: Some Preliminary Experiments
Jacques Carette, William M. Farmer, Filip Jeremic +3
We present some of the experiments we have performed to best test our design for a library for MathScheme, the mechanized mathematics software system we are building. We wish for o…
cs.PL2011★ 14 cited
Functor is to Lens as Applicative is to Biplate: Introducing Multiplate
Russell O'Connor
This paper gives two new categorical characterisations of lenses: one as a coalgebra of the store comonad, and the other as a monoidal natural transformation on a category of a cer…
cs.LO2005
Essential Incompleteness of Arithmetic Verified by Coq
Russell O'Connor
A constructive proof of the Goedel-Rosser incompleteness theorem has been completed using the Coq proof assistant. Some theory of classical first-order logic over an arbitrary lang…