More Church-Rosser proofs (in Isabelle/HOL)
- 1 January 1996
- book chapter
- Published by Springer Nature
Abstract
No abstract availableKeywords
This publication has 8 references indexed in Scilit:
- Eta-conversion for the languages of explicit substitutionsPublished by Springer Nature ,2005
- Pure type systems formalizedPublished by Springer Nature ,2005
- Parallel Reductions in λ-CalculusInformation and Computation, 1995
- An explicit Eta rewrite rulePublished by Springer Nature ,1995
- Metamathematics, Machines and Gödel's ProofPublished by Cambridge University Press (CUP) ,1994
- Residual theory in λ-calculus: a formal developmentJournal of Functional Programming, 1994
- IsabellePublished by Springer Nature ,1994
- Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theoremIndagationes Mathematicae, 1972