We use generic programming techniques to generate well-typed lambda terms. We encode well-typed terms by means of generalized algebraic datatypes (GADTs) and existential types. The Spine approach to generic programming supports GADTs, but it does not support the definition of generic producers for existentials. We describe how to extend the Spine approach to support existentials and we use the improved Spine to define a generic enumeration function. We show that the enumeration function can be used to generate the terms of simply typed lambda calculus. © 2010 Springer-Verlag.
CITATION STYLE
Rodriguez Yakushev, A., & Jeuring, J. (2010). Enumerating well-typed terms generically. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5812 LNCS, pp. 93–116). Springer Verlag. https://doi.org/10.1007/978-3-642-11931-6_5
Mendeley helps you to discover research relevant for your work.