Reference

2001
    Human-Readable Machine-Verifiable Proofs for Teaching Constructive Logic
    Andreas Abel, Bor-Yuh Evan Chang, and Frank Pfenning
    PTP 2001: Workshop on Proof Transformations, Proof Presentations, and Complexity of Proofs

    BibTeX

    @string{PTP = "Workshop on 
	Proof Transformations, Proof Presentations, and Complexity of Proofs
       (PTP)"}
@inproceedings{tutch-ptp01,
  author = {Andreas Abel and Bor-Yuh Evan Chang and Frank Pfenning},
  title = {
       Human-Readable Machine-Verifiable Proofs for Teaching Constructive Logic
     },
  booktitle = PTP,
  year = {2001},
}