Abstract
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.
Chapter PDF
Similar content being viewed by others
References
Aczel, P.: A general Church-Rosser theorem. Technical report, University of Manchester (1978)
Altenkirch, T., Hofmann, M., Streicher, T.: Reduction-free normalisation for a polymorphic system. In: Proc. of LICS 1996, pp. 98–106 (1996)
de Bruijn, N.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae 34, 381–391 (1972)
Fiore, M., Hur, C.-K.: Second-order equational logic. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 320–335. Springer, Heidelberg (2010)
Fiore, M.: Semantic analysis of normalisation by evaluation for typed lambda calculus. In: Proc. of PPDP 2002, pp. 26–37. ACM Press, New York (2002)
Fiore, M.: Second-order and dependently-sorted abstract syntax. In: Proc. of LICS 2008, pp. 57–68 (2008)
Fiore, M.: Algebraic meta-theories and synthesis of equational logics (2009), Research Programme
Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: Proc. of LICS 1999, pp. 193–202 (1999)
Grothendieck, A.: Catégories fibrées et descente (exposé VI). In: Grothendieck, A. (ed.) Revêtement Etales et Groupe Fondamental (SGA1). Lecture Notes in Mathematics, vol. 224, pp. 145–194. Springer, Heidelberg (1970)
Goguen, J., Thatcher, J., Wagner, E.: An initial algebra approach to the specification, correctness and implementation of abstract data types. Technical Report RC 6487, IBM T. J. Watson Research Center (1976)
Ghani, N., Uustalu, T., Hamana, M.: Explicit substitutions and higher-order syntax. Higher-Order and Symbolic Computation 19(2/3), 263–282 (2006)
Hamana, M.: Free Σ-monoids: A higher-order syntax with metavariables. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol. 3302, pp. 348–363. Springer, Heidelberg (2004)
Hamana, M.: Universal algebra for termination of higher-order rewriting. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 135–149. Springer, Heidelberg (2005)
Hamana, M.: Higher-order semantic labelling for inductive datatype systems. In: Proc. of PPDP 2007, pp. 97–108. ACM Press, New York (2007)
Hamana, M.: Initial algebra semantics for cyclic sharing tree structures. Logical Methods in Computer Science 6(3) (2010)
Hofmann, M.: Semantical analysis of higher-order abstract syntax. In: Proc. of LICS 1999, pp. 204–213 (1999)
Katsumata, S.: A generalisation of pre-logical predicates to simply typed formal systems. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 831–845. Springer, Heidelberg (2004)
Morris, P., Altenkirch, T.: Indexed containers. In: LICS 2009, pp. 277–285 (2009)
Miculan, M.: A categorical model of the Fusion calculus. In: Proc. of MFPS XXIV. ENTCS, vol. 218, pp. 275–293. Elsevier, Amsterdam (2008)
Miculan, M., Scagnetto, I.: A framework for typed HOAS and semantics. In: Proc. of PPDP 2003, pp. 184–194. ACM Press, New York (2003)
Smyth, M.B., Plotkin, G.D.: The category-theoretic solution of recursive domain equations. SIAM J. Comput 11(4), 763–783 (1982)
Tanaka, M., Power, J.: Category theoretic semantics for typed binding signatures with recursion. Fundam. Inform. 84(2), 221–240 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hamana, M. (2011). Polymorphic Abstract Syntax via Grothendieck Construction. In: Hofmann, M. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2011. Lecture Notes in Computer Science, vol 6604. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19805-2_26
Download citation
DOI: https://doi.org/10.1007/978-3-642-19805-2_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19804-5
Online ISBN: 978-3-642-19805-2
eBook Packages: Computer ScienceComputer Science (R0)