A mechanisation of name-carrying syntax up to alpha-conversion
- 1 January 1994
- book chapter
- Published by Springer Nature
Abstract
No abstract availableKeywords
This publication has 8 references indexed in Scilit:
- Higher-Order Abstract Syntax with induction in CoqPublished by Springer Nature ,1994
- Closure under alpha-conversionPublished by Springer Nature ,1994
- Representing higher-order logic proofs in HOLPublished by Springer Nature ,1994
- A Proof of the Church-Rosser Theorem and its Representation in a Logical FrameworkPublished by Defense Technical Information Center (DTIC) ,1992
- Explicit substitutionsJournal of Functional Programming, 1991
- 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
- Some properties of conversionTransactions of the American Mathematical Society, 1936