Mechanizing the metatheory of LF
From MaRDI portal
Publication:2946633
DOI10.1145/1877714.1877721zbMath1351.68250arXiv0804.1667OpenAlexW2077128347MaRDI QIDQ2946633
James Cheney, Stefan Berghofer, Christian Urban
Publication date: 17 September 2015
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/0804.1667
Related Items
Formalising Observer Theory for Environment-Sensitive Bisimulation, Formalizing adequacy: a case study for higher-order abstract syntax, αCheck: A mechanized metatheory model checker, POPLMark reloaded: Mechanizing proofs by logical relations, The Isabelle Framework, Structural recursion with locally scoped names, Formal SOS-Proofs for the Lambda-Calculus, Mechanizing proofs with logical relations – Kripke-style, General Bindings and Alpha-Equivalence in Nominal Isabelle, Mechanised Computability Theory, Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem, Mechanizing the Metatheory of mini-XQuery, Mechanized metatheory revisited, \texttt{slepice}: towards a verified implementation of type theory in type theory
Uses Software
