Programs Using Syntax with First-Class Binders
Abstract elided by the publisher.
Related papers
- A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions POPL 2008
- Boxes go bananas: encoding higher-order abstract syntax with parametric polymorphism ICFP 2003
- Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism JFP 2008
- Binder aware recursion over well-scoped de Bruijn syntax CPP 2018
- Coq à la carte: a practical approach to modular syntax with binders CPP 2020
- A unified treatment of syntax with binders JFP 2012
- Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl) ICFP 2021
- Binders unbound ICFP 2011