Showing 1–1 of 1 results for author: Érdi, G

Generic Description of Well-Scoped, Well-Typed Syntaxes

Authors: Gergő Érdi

Abstract: We adapt the technique of type-generic programming via descriptions pointing into a universe to the domain of typed languages with binders and variables, implementing a notion of "syntax-generic programming" in a dependently typed programming language. We present an Agda library implementation of type-preserving renaming and substitution (including proofs about their behaviour) "once and for all"… ▽ More We adapt the technique of type-generic programming via descriptions pointing into a universe to the domain of typed languages with binders and variables, implementing a notion of "syntax-generic programming" in a dependently typed programming language. We present an Agda library implementation of type-preserving renaming and substitution (including proofs about their behaviour) "once and for all" over all applicable languages using our technique. △ Less

Submitted 31 March, 2018; originally announced April 2018.