• Home
• Research
• Teaching
• Software

Software

Main projects

• Camelide: a type checker for Dedukti, a language with dependent types and term rewriting.
• Holide: a translator of HOL proofs from OpenTheory to Dedukti.
• Coqine: a translator of Coq proofs to Dedukti.
• Krajono: a translator of Matita proofs to Dedukti. new

Side projects

• Algorithm X in 30 lines: an original and lightweight implementation of Knuth’s Algorithm X in Python.
• Prime numbers: simple and efficient prime number generation in Python.
• Preparen: a Latex package for pretty-printing precedence parentheses.