Page under construction.

Type-checkers for the λΠ-calculus modulo theory

  • Dkcheck: type-checker
  • Kontroli: parallel version of dkcheck
  • Lambdapi: interactive extension of dkcheck with metavariables and tactics

Proof data bases

Proof translation tools

Interactive theorem provers

Automated theorem provers

  • ArchSAT: SMT solver generating Dedukti/FOL
  • cvc5: efficient versatile SMT solver generating proof traces
  • z3: efficient SMT solver that generates proofs (for a subset of checks, at least).
  • veriT: SMT solver generating detailed proof traces
  • ZenonModulo: ATP generating Dedukti/FOL or Lambdapi/FOL