Title: Proof-term synthesis on dependent-type systems via explicit substitutions
First published: 1999
Subjects: Mathematical models, Proving