Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming
No abstract available.
Related papers
- Contextual equivalence for inductive definitions with binders in higher order typed functional programming JFP 2013
- Coq à la carte: a practical approach to modular syntax with binders CPP 2020
- A relational framework for higher-order shape analysis ICFP 2014
- A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions POPL 2008
- Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl) ICFP 2021
- Binder aware recursion over well-scoped de Bruijn syntax CPP 2018
- Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism JFP 2008
- A Fresh Approach to Representing Syntax with Static Binders in Functional Programming ICFP 2001