Hostname: page-component-cd9895bd7-dzt6s Total loading time: 0 Render date: 2024-12-18T02:26:31.949Z Has data issue: false hasContentIssue false
  • English
  • Français

Modules over relative monads for syntax and semantics

Published online by Cambridge University Press:  05 December 2014

BENEDIKT AHRENS
BENEDIKT AHRENS*
Affiliation:
Laboratoire J. A. Dieudonné, Université Nice Sophia Antipolis, France
Get access Rights & Permissions [Opens in a new window]

Abstract

We give an algebraic characterization of the syntax and semantics of a class of untyped functional programming languages.

To this end, we introduce a notion of 2-signature: such a signature specifies not only the terms of a language, but also reduction rules on those terms. To any 2-signature (S, A) we associate a category of ‘models’. We then prove that this category has an initial object, which integrates the terms freely generated by S, and which is equipped with reductions according to the rules given in A. We call this initial object the programming language generated by (S, A). Models of a 2-signature are built from relative monads and modules over such monads. Through the use of monads, the models – and in particular, the initial model – come equipped with a substitution operation that is compatible with reduction in a suitable sense.

The initiality theorem is formalized in the proof assistant Coq, yielding a machinery which, when fed with a 2-signature, provides the associated programming language with reduction relation and certified substitution.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 26 , Special Issue 1: Special Issue: Dependently Typed Programming , January 2016 , pp. 3 - 37
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Ahrens, B. (2012) Extended initiality for typed abstract syntax. Logical Methods in Computer Science 8.2 1–35. (doi: 10.2168/LMCS-8(2:1)2012.)Google Scholar
Ahrens, B. and Zsidó, J. (2011) Initial semantics for higher–order typed syntax in Coq. Journal of Formalized Reasoning 4.1 25–69.Google Scholar
Altenkirch, T. and Reus, B. (1999) Monadic presentations of lambda terms using generalized inductive types. In: Computer Science Logic, 13th International Workshop, CSL '99 453–468.Google Scholar
Altenkirch, T. et al. (2010) Monads need not be endofunctors. In: Luke Ong, C.-H. (ed.) FOSSACS. Springer Lecture Notes in Computer Science 6014 297–311. ISBN: 978-3-642-12031-2.Google Scholar
Barendregt, H. and Barendsen, E. (1994) Introduction to lambda calculus. Available at: ftp://ftp.cs.ru.nl/pub/CompMath.Found/lambda.pdf. revised 2000.Google Scholar
Bird, R. S. and Meertens, L. (1998) Nested datatypes. In: Jeuring, J. (ed.) Proceedings of Mathematics of Program Construction. Springer Lecture Notes in Computer Science 1422 52–67.CrossRefGoogle Scholar
Coq (2010) The coq proof assistant. Available at: http://coq.inria.fr. URL: http://coq.inria.fr.Google Scholar
Fernández, M. and Gabbay, M. J. (2007) Nominal rewriting. Information and Computation 205.6 917–965. doi: 10.1016/j.ic.2006.12.002.Google Scholar
Fiore, M. (2002) Semantic analysis of normalisation by evaluation for typed lambda calculus. In: Proceedings of the 4th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming. PPDP'02, Pittsburgh, PA, USA: ACM 26–37. ISBN: 1-58113-528-9. doi: http://doi.acm.org/10.1145/571157.571161.Google Scholar
Fiore, M. (2005) Mathematical models of computational and combinatorial structures. In: Sassone, V. (ed.) FoSSaCS. Springer Lecture Notes in Computer Science 3441 25–46. ISBN: 3-540-25388-2.Google Scholar
Fiore, M. and Hur, C.-K. (2007) Equational systems and free constructions (extended abstract). In: Arge, L. et al. (ed.) ICALP. Springer Lecture Notes in Computer Science 4596 607–618. ISBN: 978-3-540-73419-2.CrossRefGoogle Scholar
Fiore, M. et al. (1999) Abstract syntax and variable binding. In: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science. LICS '99, Washington, DC, USA: IEEE Computer Society 193–202. ISBN: 0-7695-0158-3.CrossRefGoogle Scholar
Gabbay, M. and Pitts, A. (1999) A new approach to abstract syntax involving binders. In: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science. LICS '99, Washington, DC, USA: IEEE Computer Society 214–224. ISBN: 0-7695-0158-3.Google Scholar
Gabbay, M. J. and Pitts, A. M. (2001) A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13.3–5 341–363. doi: http://doi.ieeecomputersociety.org/10.1109/LICS.1999.782617.Google Scholar
Ghani, N. and Lüth, C. (2003) Rewriting via coinserters. Nordic Journal of Computing 10.4 290–312.Google Scholar
Hirschowitz, A. and Maggesi, M. (2007a) Modules over monads and linearity. In: Leivant, D. and de Queiroz, R. J. G. B. (eds.) WoLLIC. Springer Lecture Notes in Computer Science 4576 218–237. ISBN: 978-3-540-73443-7.CrossRefGoogle Scholar
Hirschowitz, A. and Maggesi, M. (2007b) The algebraicity of the lambda-calculus. In: CoRR abs/0704.2900. Available at http://arxiv.org/abs/0704.2900.Google Scholar
Hirschowitz, A. and Maggesi, M. (2010) Modules over monads and initial semantics. Information and Computation 208.5 545–564.Google Scholar
Hirschowitz, T. (2013) Cartesian closed 2-categories and permutation equivalence in higher-order rewriting. Logical Methods in Computer Science 9 (3). Available at: http://dx.doi.org/10.2168/LMCS9(3:10)2013.Google Scholar
Hofmann, M. (1999) Semantical analysis of higher-order syntax. In: 14th Annual Symposium on Logic in Computer Science, IEEE Computer Society Press 204–213.Google Scholar
Hur, C.-K. (2010) Categorical Equational Systems: Algebraic Models and Equational Reasoning, Ph.D. thesis, University of Cambridge, UK.Google Scholar
Mac Lane, S. (1998) Categories for the Working Mathematician, Second. Graduate Texts in Mathematics volume 5, New York: Springer-Verlag xii+314. ISBN: 0-387-98403-8.Google Scholar
Miculan, M. and Scagnetto, I. (2003) A framework for typed HOAS and semantics. In: Principles and Practice of Declarative Programming, ACM 184–194. ISBN: 1-58113-705-2.Google Scholar
Pitts, A. M. (2003) Nominal logic, a first order theory of names and binding. Information and Computation 186 165–193.Google Scholar
Power, J. (2007) Abstract syntax: Substitution and binders. Electronic Notes in Theoretical Computer Science 173 3–16. ISSN: . doi: 10.1016/j.entcs.2007.02.024.Google Scholar
Tanaka, M. and Power, J. (2005) A unified category-theoretic formulation of typed binding signatures. In: Proceedings of the 3rd ACM SIGPLAN Workshop on Mechanized Reasoning about Languages with Variable Binding. MERLIN '05, Tallinn, Estonia: ACM, 13–24. ISBN: 1-59593-072-8. doi: http://doi.acm.org/10.1145/1088454.1088457.Google Scholar
Zsidó, J. (2010) Typed abstract syntax. Available at http://tel.archives-ouvertes.fr/tel-00535944/. Ph.D. thesis, University of Nice, France.Google Scholar