projects I've worked on
formal logic
- L4.verified
verifying a high-performance mirco-kernel - AFP
the archive of formal proofs - Isabelle
generic theorem proving - Verificard
theorem proving for JavaCard
tools
computer algebra
- Spock
fast algorithms for sparse polynomials
