Urban, Christian; Cheney, James; Berghofer, Stefan Mechanizing the metatheory of LF. (English) Zbl 1351.68250 ACM Trans. Comput. Log. 12, No. 2, Article No. 15, 42 p. (2011). Cited in 14 Documents MSC: 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) 68N18 Functional programming and lambda calculus Keywords:logical frameworks; Nominal Isabelle; theorem provers Software:Twelf; Isabelle/HOL; Nominal Isabelle PDFBibTeX XMLCite \textit{C. Urban} et al., ACM Trans. Comput. Log. 12, No. 2, Article No. 15, 42 p. (2011; Zbl 1351.68250) Full Text: DOI arXiv