Heterogeneous Substitution Systems Revisited

Authors Benedikt Ahrens, Ralph Matthes

Thumbnail PDF


  • Filesize: 0.59 MB
  • 23 pages

Document Identifiers

Author Details

Benedikt Ahrens
Ralph Matthes

Cite AsGet BibTex

Benedikt Ahrens and Ralph Matthes. Heterogeneous Substitution Systems Revisited. In 21st International Conference on Types for Proofs and Programs (TYPES 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 69, pp. 2:1-2:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Matthes and Uustalu (TCS 327(1--2):155--174, 2004) presented a categorical description of substitution systems capable of capturing syntax involving binding which is independent of whether the syntax is made up from least or greatest fixed points. We extend this work in two directions: we continue the analysis by creating more categorical structure, in particular by organizing substitution systems into a category and studying its properties, and we develop the proofs of the results of the cited paper and our new ones in UniMath, a recent library of univalent mathematics formalized in the Coq theorem prover.
  • formalization of category theory
  • nested datatypes
  • Mendler-style recursion schemes
  • representation of substitution in languages with variable binding


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. A. Abel. A Polymorphic Lambda-Calculus with Sized Higher-Order Types. Doktorarbeit (PhD thesis), LMU München, 2006. Google Scholar
  2. Andreas Abel. Termination checking with types. ITA, 38(4):277-319, 2004. URL: http://dx.doi.org/10.1051/ita:2004015.
  3. Andreas Abel, Ralph Matthes, and Tarmo Uustalu. Iteration and coiteration schemes for higher-order and nested datatypes. Theor. Comput. Sci., 333(1-2):3-66, 2005. URL: http://dx.doi.org/10.1016/j.tcs.2004.10.017.
  4. B. Ahrens, K. Kapulkin, and M. Shulman. Univalent categories and the Rezk completion. Math. Struct. Comput. Sci., 25(5):1010-1039, 2015. URL: http://dx.doi.org/10.1017/s0960129514000486.
  5. B. Ahrens, R. Matthes, and A. Mörtberg. From signatures to monads in UniMath, 2016. arXiv preprint 1612.00693. URL: https://arxiv.org/abs/1612.00693.
  6. Benedikt Ahrens and Anders Mörtberg. Some wellfounded trees in UniMath - extended abstract. In Gert-Martin Greuel, Thorsten Koch, Peter Paule, and Andrew J. Sommese, editors, Mathematical Software - ICMS 2016 - 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings, volume 9725 of Lecture Notes in Computer Science, pages 9-17. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-42432-3_2.
  7. T. Altenkirch, J. Chapman, and T. Uustalu. Monads need not be endofunctors. Log. Methods Comput. Sci., 11(1):article 3, 2015. URL: http://dx.doi.org/10.2168/lmcs-11(1:3)2015.
  8. Thorsten Altenkirch and Bernhard Reus. Monadic presentations of lambda terms using generalized inductive types. In Jörg Flum and Mario Rodríguez-Artalejo, editors, Computer Science Logic, 13th International Workshop, CSL '99, 8th Annual Conference of the EACSL, Madrid, Spain, September 20-25, 1999, Proceedings, volume 1683 of Lecture Notes in Computer Science, pages 453-468. Springer, 1999. URL: http://dx.doi.org/10.1007/3-540-48168-0_32.
  9. Françoise Bellegarde and James Hook. Subsitution: A formal methods case study using monads and transformations. Sci. Comput. Program., 23(2-3):287-311, 1994. URL: http://dx.doi.org/10.1016/0167-6423(94)00022-0.
  10. R. Bird and L. Meertens. Nested datatypes. In J. Jeuring, editor, Proc. of 4th Int. Conf. on Mathematics of Program Construction, MPC '98, volume 1422 of Lect. Notes in Comput. Sci., pages 52-67. Springer, 1998. URL: http://dx.doi.org/10.1007/bfb0054285.
  11. R. S. Bird and R. Paterson. De Bruijn notation as a nested datatype. J. Funct. Program., 9(1):77-91, 1999. URL: http://dx.doi.org/10.1017/s0956796899003366.
  12. Richard S. Bird and Ross Paterson. Generalised folds for nested datatypes. Formal Asp. Comput., 11(2):200-222, 1999. URL: http://dx.doi.org/10.1007/s001650050047.
  13. The Coq Development Team. The Coq proof assistant reference manual, version 8.6, 2016. URL: https://coq.inria.fr/distrib/current/refman/.
  14. M. Fiore. Second-order and dependently-sorted abstract syntax. In Proc. of 23rd Ann. IEEE Symp. on Logic in Computer Science, LICS 2008. IEEE, 2008. URL: http://dx.doi.org/10.1109/lics.2008.38.
  15. M. Fiore, G. Plotkin, and D. Turi. Abstract syntax and variable binding. In Proc. of 14th Ann. IEEE Symp. on Logic in Computer Science, LICS '99, pages 193-202. IEEE, 1999. URL: http://dx.doi.org/10.1109/lics.1999.782615.
  16. Ryu Hasegawa. Parametricity of extensionally collapsed term models of polymorphism and their categorical properties. In Takayasu Ito and Albert R. Meyer, editors, Theoretical Aspects of Computer Software, International Conference TACS '91, Sendai, Japan, September 24-27, 1991, Proceedings, volume 526 of Lecture Notes in Computer Science, pages 495-512. Springer, 1991. URL: http://dx.doi.org/10.1007/3-540-54415-1_61.
  17. A. Hirschowitz and M. Maggesi. Initial semantics for strengthened signatures. In D. Miller and Z. Ésik, editors, Proc. of 8th Wksh. on Fixed Points in Computer Science, FICS 2012, volume 77 of Electron. Proc. in Theor. Comput. Sci., pages 31-38. Open Publishing Assoc., 2012. URL: http://dx.doi.org/10.4204/eptcs.77.5.
  18. André Hirschowitz and Marco Maggesi. Modules over monads and linearity. In Daniel Leivant and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information and Computation, 14th International Workshop, WoLLIC 2007, Rio de Janeiro, Brazil, July 2-5, 2007, Proceedings, volume 4576 of Lecture Notes in Computer Science, pages 218-237. Springer, 2007. URL: http://dx.doi.org/10.1007/978-3-540-73445-1_16.
  19. André Hirschowitz and Marco Maggesi. Modules over monads and initial semantics. Inf. Comput., 208(5):545-564, 2010. URL: http://dx.doi.org/10.1016/j.ic.2009.07.003.
  20. M. Hofmann and T. Streicher. The groupoid interpretation of type theory. In G. Sambin and J. M. Smith, editors, Twenty-Five Years of Constructive Type Theory, volume 36 of Oxford Logic Guides, pages 127-172. Clarendon Press, 1998. Google Scholar
  21. G. Huet and A. Saïbi. Constructive category theory: Essays in honour of Robin Milner. In G. Plotkin, C. Stirling, and M. Tofte, editors, Proof, Language, and Interaction, Foundations of Computing Series, pages 239-275. MIT Press, 2000. Google Scholar
  22. Clare E. Martin, Jeremy Gibbons, and Ian Bayley. Disciplined, efficient, generalised folds for nested datatypes. Formal Asp. Comput., 16(1):19-35, 2004. URL: http://dx.doi.org/10.1007/s00165-003-0013-6.
  23. Ralph Matthes. Map fusion for nested datatypes in intensional type theory. Sci. Comput. Program., 76(3):204-224, 2011. URL: http://dx.doi.org/10.1016/j.scico.2010.05.008.
  24. Ralph Matthes and Tarmo Uustalu. Substitution in non-wellfounded syntax with variable binding. Theor. Comput. Sci., 327(1-2):155-174, 2004. URL: http://dx.doi.org/10.1016/j.tcs.2004.07.025.
  25. N. P. Mendler. Inductive types and type constraints in the second-order lambda calculus. Ann. Pure Appl. Log., 51(1-2):159-172, 1991. URL: http://dx.doi.org/10.1016/0168-0072(91)90069-x.
  26. Marino Miculan and Ivan Scagnetto. A framework for typed HOAS and semantics. In Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 27-29 August 2003, Uppsala, Sweden, pages 184-194. ACM, 2003. URL: http://dx.doi.org/10.1145/888251.888269.
  27. E. Palmgren and O. Wilander. Constructing categories and setoids of setoids in type theory. Log. Methods Comput. Sci., 10(3):article 25, 2014. URL: http://dx.doi.org/10.2168/lmcs-10(3:25)2014.
  28. Matthieu Sozeau and Nicolas Tabareau. Universe polymorphism in Coq. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8558 of Lecture Notes in Computer Science, pages 499-514. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-319-08970-6_32.
  29. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. URL: http://homotopytypetheory.org/book.
  30. V. Voevodsky. An experimental library of formalized mathematics based on the univalent foundations. Math. Struct. Comput. Sci., 25:1278-1294, 2015. URL: http://dx.doi.org/10.1017/s0960129514000577.
  31. V. Voevodsky. C-system of a module over a Jf-relative monad, 2016. arXiv preprint 1602.00352. URL: https://arxiv.org/abs/1602.00352.
  32. V. Voevodsky, B. Ahrens, D. Grayson, and Others. UniMath: Univalent mathematics. URL: https://github.com/UniMath.