Gabbay, Murdoch J.; Mathijssen, Aad Capture-avoiding substitution as a nominal algebra. (English) Zbl 1152.68025 Formal Asp. Comput. 20, No. 4-5, 451-479 (2008). MSC: 68Q42 03B70 PDFBibTeX XMLCite \textit{M. J. Gabbay} and \textit{A. Mathijssen}, Formal Asp. Comput. 20, No. 4--5, 451--479 (2008; Zbl 1152.68025) Full Text: DOI
Dybjer, Peter Inductive families. (English) Zbl 0808.03044 Formal Asp. Comput. 6, No. 4, 440-465 (1994). MSC: 03F35 03B70 PDFBibTeX XMLCite \textit{P. Dybjer}, Formal Asp. Comput. 6, No. 4, 440--465 (1994; Zbl 0808.03044) Full Text: DOI
Weber, Matthias Definition and basic properties of the Deva meta-calculus. (English) Zbl 0783.68031 Formal Asp. Comput. 5, No. 5, 391-431 (1993). Reviewer: M.Weber MSC: 68N99 68N01 68Q60 PDFBibTeX XMLCite \textit{M. Weber}, Formal Asp. Comput. 5, No. 5, 391--431 (1993; Zbl 0783.68031) Full Text: DOI
Seldin, Jonathan P. Coquand’s calculus of constructions: A mathematical foundation for a proof development system. (English) Zbl 0766.03007 Formal Asp. Comput. 4, No. 5, 425-441 (1992). MSC: 03B40 03F03 03F05 68N15 68Q99 PDFBibTeX XMLCite \textit{J. P. Seldin}, Formal Asp. Comput. 4, No. 5, 425--441 (1992; Zbl 0766.03007) Full Text: DOI