Engineering formal metatheory
- 7 January 2008
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM)
- Vol. 43 (1), 3-15
- https://doi.org/10.1145/1328438.1328443
Abstract
No abstract availableKeywords
This publication has 25 references indexed in Scilit:
- Mechanizing metatheory in a logical frameworkJournal of Functional Programming, 2007
- A machine-checked model for a Java-like language, virtual machine, and compilerACM Transactions on Programming Languages and Systems, 2006
- Consistency of the theory of contextsJournal of Functional Programming, 2006
- A formalised first-order confluence proof for the λ-calculus using one-sorted variable namesInformation and Computation, 2003
- Inductive familiesFormal Aspects of Computing, 1994
- Residual theory in λ-calculus: a formal developmentJournal of Functional Programming, 1994
- A framework for defining logicsJournal of the ACM, 1993
- Substitution revisitedTheoretical Computer Science, 1988
- A mechanical proof of the Church-Rosser theoremJournal of the ACM, 1988
- Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theoremIndagationes Mathematicae, 1972