Abstract syntax with variable binding is known to be characterised as an initial algebra in a presheaf category. This paper extends it to the case of polymorphic typed abstract syntax with binding. We consider two variations, second-order and higher-order polymorphic syntax. The central idea is to apply Fiore's initial algebra characterisation of typed abstract syntax with binding repeatedly, i.e. first to the type structure and secondly to the term structure of polymorphic system. In this process, we use the Grothendieck construction to combine differently staged categories of polymorphic contexts. © 2011 Springer-Verlag.
CITATION STYLE
Hamana, M. (2011). Polymorphic abstract syntax via Grothendieck construction. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6604 LNCS, pp. 381–395). https://doi.org/10.1007/978-3-642-19805-2_26
Mendeley helps you to discover research relevant for your work.