Miller, Dale Mechanized metatheory revisited. (English) Zbl 1468.68303 J. Autom. Reasoning 63, No. 3, 625-665 (2019). MSC: 68V15 03B35 PDFBibTeX XMLCite \textit{D. Miller}, J. Autom. Reasoning 63, No. 3, 625--665 (2019; Zbl 1468.68303) Full Text: DOI HAL
Andrews, Peter B.; Brown, Chad E. TPS: A hybrid automatic-interactive system for developing proofs. (English) Zbl 1107.68091 J. Appl. Log. 4, No. 4, 367-395 (2006). MSC: 68T15 PDFBibTeX XMLCite \textit{P. B. Andrews} and \textit{C. E. Brown}, J. Appl. Log. 4, No. 4, 367--395 (2006; Zbl 1107.68091) Full Text: DOI
Andrews, Peter B.; Bishop, Matthew; Issar, Sunil; Nesmith, Dan; Pfenning, Frank; Xi, Hongwei TPS: A theorem-proving system for classical type theory. (English) Zbl 0858.03017 J. Autom. Reasoning 16, No. 3, 321-353 (1996). Reviewer: M.P.Bonacina (Iowa City) MSC: 03B35 03B15 68T15 PDFBibTeX XMLCite \textit{P. B. Andrews} et al., J. Autom. Reasoning 16, No. 3, 321--353 (1996; Zbl 0858.03017) Full Text: DOI
Longo, Giuseppe On Church’s formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory. (English) Zbl 0673.03009 Ann. Pure Appl. Logic 40, No. 2, 93-133 (1988). Reviewer: P.Bankston MSC: 03B40 03D65 03G30 03F10 03-02 PDFBibTeX XMLCite \textit{G. Longo}, Ann. Pure Appl. Logic 40, No. 2, 93--133 (1988; Zbl 0673.03009) Full Text: DOI