Duper: A Proof-Producing Superposition Theorem Prover for Dependent Type Theory.

Joshua Clune, Yicheng Qian, Alexander Bentkamp, Jeremy Avigad

Browse the full ITP paper archive.