Deliverable 5
Release of software for translating proofs coming from important proof systems based on type theory like Isabelle, Agda, PVS, Lean or Minlog, to Dedukti and back.
- hol2dk: HOL-Light to Dedukti and Lambdapi
- lambdapi: Dedukti/HOL and Lambdapi/HOL to Coq
- isabelle_dedukti: Isabelle to Dedukti and Lambdapi
- Personoj: PVS to Lambdapi
- Agda2dedukti: Agda to Dedukti
- Coqine: Coq to Dedukti
- Holide: OpenTheory to Dedukti
- HOLLightToDk: HOL-Light to Dedukti via OpenTheory
- STTfaXport: Dedukti/STTfa to Coq, Lean, PVS, Matita, OpenTheory
- Krajono: Matita to Dedukti
- Predicativize: translate Dedukti proofs to Dedukti proofs with universe polymorphism, and translate them to Agda
- Lean2dk: Lean4 to Dedukti
- B-pog-translator: translator from Atelier B proof obligation files to Lambdapi
- Hol2dk: HOL-Light to Dedukti and Lambdapi