Appel, Andrew W.; Felty, Amy P. Polymorphic lemmas and definitions in \(\lambda\)Prolog and Twelf. (English) Zbl 1085.68015 Theory Pract. Log. Program. 4, No. 1-2, 1-39 (2004). MSC: 68N17 68N18 PDFBibTeX XMLCite \textit{A. W. Appel} and \textit{A. P. Felty}, Theory Pract. Log. Program. 4, No. 1--2, 1--39 (2004; Zbl 1085.68015) Full Text: DOI
Felty, Amy Implementing tactics and tacticals in a higher-order logic programming language. (English) Zbl 0783.68117 J. Autom. Reasoning 11, No. 1, 43-81 (1993). MSC: 68T99 68N17 68T15 PDFBibTeX XMLCite \textit{A. Felty}, J. Autom. Reasoning 11, No. 1, 43--81 (1993; Zbl 0783.68117) Full Text: DOI
Felty, A.; Miller, O. Encoding a dependent-type \(\lambda\)-calculus in a logic programming language. (English) Zbl 0708.68090 Automated deduction, Proc. 10th Int. Conf., Kaiserslautern/FRG 1990, Lect. Notes Comput. Sci. 449, 221-235 (1990). Reviewer: G.Mints MSC: 68T99 03B40 68N17 PDFBibTeX XML
Felty, Amy; Miller, Dale Specifying theorem provers in a higher-order logic programming language. (English) Zbl 0645.68097 Automated deduction, Proc. 9th Int. Conf., Argonne/Ill. 1988, Lect. Notes Comput. Sci. 310, 61-80 (1988). MSC: 68T15 03B35 68N01 03B15 PDFBibTeX XML