Document Open Access Logo

Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory

Authors Benedikt Ahrens, Régis Spadotti

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2014.1.pdf
  • Filesize: 0.57 MB
  • 26 pages

Document Identifiers

Author Details

Benedikt Ahrens
Régis Spadotti

Cite As Get BibTex

Benedikt Ahrens and Régis Spadotti. Terminal Semantics for Codata Types in Intensional Martin-Löf Type Theory. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 1-26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.TYPES.2014.1

Abstract

We study the notions of relative comonad and comodule over a relative comonad. We use these notions to give categorical semantics for the coinductive type families of streams and of infinite triangular matrices and their respective cosubstitution operations in intensional Martin-Löf type theory. Our results are mechanized in the proof assistant Coq.

Subject Classification

Keywords
  • relative comonad
  • Martin-Löf type theory
  • coinductive type
  • computer theorem proving

Metrics

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

References

  1. Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. Copatterns: programming infinite structures by observations. In Roberto Giacobazzi and Radhia Cousot, editors, Principles of Programming Languages, pages 27-38. ACM, 2013. URL: http://doi.acm.org/10.1145/2429069.2429075.
  2. Peter Aczel. Galois: A Theory Development Project, 1993. Technical Report for the 1993 Turin meeting on the Representation of Mathematics in Logical Frameworks. http://www.cs.man.ac.uk/~petera/papers.html.
  3. Benedikt Ahrens. Modules over relative monads for syntax and semantics. Mathematical Structures in Computer Science, FirstView:1-35, 2014. URL: http://dx.doi.org/10.1017/S0960129514000103.
  4. Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti. Non-Wellfounded Trees in Homotopy Type Theory. In Thorsten Altenkirch, editor, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), volume 38 of Leibniz International Proceedings in Informatics (LIPIcs), pages 17-30, Dagstuhl, Germany, 2015. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://hott.github.io/M-types/.
  5. Benedikt Ahrens and Régis Spadotti. Terminal semantics for codata types in intensional Martin-Löf type theory: Coq code. URL: http://benediktahrens.github.io/coinductives/.
  6. Thorsten Altenkirch, James Chapman, and Tarmo Uustalu. Monads need not be endofunctors. In C.-H. Luke Ong, editor, Foundations of Software Science and Computational Structures, volume 6014 of LNCS, pages 297-311. Springer, 2010. Google Scholar
  7. Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, and Peter Morris. Indexed Containers. Unpublished version, URL: http://www.cs.nott.ac.uk/~txa/publ/jcont.pdf.
  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, Proceedings of Computer Science Logic, 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. Steve Awodey, Nicola Gambino, and Kristina Sojakova. Inductive Types in Homotopy Type Theory. In Proceedings of Symposium on Logic in Computer Science, pages 95-104. IEEE, 2012. URL: http://dx.doi.org/10.1109/LICS.2012.21.
  10. The Coq Development Team. The Coq Proof Assistant. http://coq.inria.fr, 2015.
  11. Thierry Coquand. Infinite objects in type theory. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs 1993, volume 806 of Lecture Notes in Computer Science, pages 62-78. Springer, 1993. URL: http://dx.doi.org/10.1007/3-540-58085-9_72.
  12. Peter Dybjer. Representing Inductively Defined Sets by Wellorderings in Martin-Löf’s Type Theory. Theor. Comput. Sci., 176(1-2):329-335, 1997. URL: http://dx.doi.org/10.1016/S0304-3975(96)00145-4.
  13. Marcelo Fiore, Gordon Plotkin, and Daniele Turi. Abstract syntax and variable binding. In Proceedings of the Symposium on Logic in Computer Science, pages 193-202, Washington, DC, USA, 1999. IEEE Computer Society. URL: http://dx.doi.org/10.1109/LICS.1999.782615.
  14. 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.
  15. Gérard P. Huet and Amokrane Saïbi. Constructive category theory. In Gordon D. Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, Language, and Interaction, Essays in Honour of Robin Milner, pages 239-276. The MIT Press, 2000. Google Scholar
  16. Bart Jacobs and Jan Rutten. A tutorial on (co) algebras and (co) induction. Bulletin-European Association for Theoretical Computer Science, 62:222-259, 1997. Google Scholar
  17. Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984. Google Scholar
  18. Ralph Matthes and Celia Picard. Verification of redecoration for infinite triangular matrices using coinduction. In Nils Anders Danielsson and Bengt Nordström, editors, Workshop on Types for Proofs and Programs, volume 19 of LIPIcs, pages 55-69. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: http://dx.doi.org/10.4230/LIPIcs.TYPES.2011.5.
  19. Ieke Moerdijk and Erik Palmgren. Wellfounded trees in categories. Ann. Pure Appl. Logic, 104(1-3):189-218, 2000. URL: http://dx.doi.org/10.1016/S0168-0072(00)00012-9.
  20. John Power. Abstract syntax: Substitution and binders. Electron. Notes Theor. Comput. Sci., 173:3-16, 4 2007. URL: http://dx.doi.org/10.1016/j.entcs.2007.02.024.
  21. Matthieu Sozeau and Nicolas Tabareau. Universe polymorphism in coq. In Gerwin Klein and Ruben Gamboa, editors, Proceedings of Interactive Theorem Proving, volume 8558 of Lecture Notes in Computer Science, pages 499-514. Springer, 2014. Google Scholar
  22. Miki Tanaka and John Power. A unified category-theoretic formulation of typed binding signatures. In Proceedings of the workshop on Mechanized reasoning about languages with variable binding, MERLIN'05, pages 13-24. ACM, 2005. URL: http://doi.acm.org/10.1145/1088454.1088457.
  23. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  24. Tarmo Uustalu and Varmo Vene. The dual of substitution is redecoration. In Kevin Hammond and Sharon Curtis, editors, Scottish Functional Programming Workshop, volume 3 of Trends in Functional Programming, pages 99-110. Intellect, 2001. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact