Tools

I developed the following software:

iProver Modulo

The integration of polarized resolution modulo into the automated theorem prover iProver

CoqInE

A translator of Coq proofs into Dedukti, a universal proof checker based on the lambda-Pi-calculus modulo formalism.