Document Open Access Logo

Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics

Authors Ambrus Kaposi , Szumi Xie

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2024.10.pdf
  • Filesize: 0.8 MB
  • 24 pages

Document Identifiers

Author Details

Ambrus Kaposi
  • Eötvös Loránd University, Budapest, Hungary
Szumi Xie
  • Eötvös Loránd University, Budapest, Hungary

Funding

  • Kaposi, Ambrus: The author was supported by project no. TKP2021-NVA-29 which has been implemented with the support provided by the Ministry of Culture and Innovation of Hungary from the National Research, Development and Innovation Fund, financed under the TKP2021-NVA funding scheme.

Cite AsGet BibTex

Ambrus Kaposi and Szumi Xie. Second-Order Generalised Algebraic Theories: Signatures and First-Order Semantics. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 10:1-10:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.FSCD.2024.10

Abstract

Programming languages can be defined from the concrete to the abstract by abstract syntax trees, well-scoped syntax, well-typed (intrinsic) syntax, algebraic syntax (well-typed syntax quotiented by conversion). Another aspect is the representation of binding structure for which nominal approaches, De Bruijn indices/levels and higher order abstract syntax (HOAS) are available. In HOAS, binders are given by the function space of an internal language of presheaves. In this paper, we show how to combine the algebraic approach with the HOAS approach: following Uemura, we define languages as second-order generalised algebraic theories (SOGATs). Through a series of examples we show that non-substructural languages can be naturally defined as SOGATs. We give a formal definition of SOGAT signatures (using the syntax of a particular SOGAT) and define two translations from SOGAT signatures to GAT signatures (signatures for quotient inductive-inductive types), based on parallel and single substitutions, respectively.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Type theory
  • universal algebra
  • inductive types
  • quotient inductive types
  • higher-order abstract syntax
  • logical framework

Metrics

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

Supplementary Materials

References

  1. Benedikt Ahrens, Jacopo Emmenegger, Paige Randall North, and Egbert Rijke. B-systems and C-systems are equivalent. The Journal of Symbolic Logic, pages 1-9, 2023. URL: https://doi.org/10.1017/jsl.2023.41.
  2. Benedikt Ahrens, André Hirschowitz, Ambroise Lafont, and Marco Maggesi. Modular specification of monads through higher-order presentations. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany, volume 131 of LIPIcs, pages 6:1-6:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPICS.FSCD.2019.6.
  3. Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, and James McKinna. A type- and scope-safe universe of syntaxes with binding: their semantics and proofs. J. Funct. Program., 31:e22, 2021. URL: https://doi.org/10.1017/S0956796820000076.
  4. Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. Extending homotopy type theory with strict equality. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France, volume 62 of LIPIcs, pages 21:1-21:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPICS.CSL.2016.21.
  5. Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, and Michael Shulman. Internal parametricity, without an interval. Proc. ACM Program. Lang., 8(POPL):2340-2369, 2024. URL: https://doi.org/10.1145/3632920.
  6. Thorsten Altenkirch and Ambrus Kaposi. Normalisation by evaluation for dependent types. In Delia Kesner and Brigitte Pientka, editors, 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, June 22-26, 2016, Porto, Portugal, volume 52 of LIPIcs, pages 6:1-6:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPICS.FSCD.2016.6.
  7. Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In Rastislav Bodík and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 18-29. ACM, 2016. URL: https://doi.org/10.1145/2837614.2837638.
  8. Thorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs, and Tamás Végh. Combinatory logic and lambda calculus are equal, algebraically. In Marco Gaboardi and Femke van Raamsdonk, editors, 8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023, July 3-6, 2023, Rome, Italy, volume 260 of LIPIcs, pages 24:1-24:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.FSCD.2023.24.
  9. 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: https://doi.org/10.1007/3-540-48168-0_32.
  10. Danil Annenkov, Paolo Capriotti, Nicolai Kraus, and Christian Sattler. Two-level type theory and applications. Mathematical Structures in Computer Science, 33(8):688-743, 2023. URL: https://doi.org/10.1017/S0960129523000130.
  11. Samy Avrillon. Logic as a second-order generalized algebraic theory, 2023. Report on the 3-month research internship at the Faculty of Informatics of ELTE. URL: https://github.com/MysaaJava/m1-internship/releases/download/project-report/Avrillon-02.pdf.
  12. Henk Barendregt. Introduction to generalized type systems. Journal of Functional Programming, 1(2):125-154, 1991. URL: https://doi.org/10.1017/S0956796800020025.
  13. Andrej Bauer, Philipp G. Haselwarter, and Peter LeFanu Lumsdaine. A general definition of dependent type theories. CoRR, abs/2009.05539, 2020. URL: https://arxiv.org/abs/2009.05539.
  14. Rafaël Bocquet. External univalence for second-order generalized algebraic theories. CoRR, abs/2211.07487, 2022. URL: https://doi.org/10.48550/arXiv.2211.07487.
  15. Rafaël Bocquet. Towards coherence theorems for equational extensions of type theories. CoRR, abs/2304.10343, 2023. URL: https://doi.org/10.48550/arXiv.2304.10343.
  16. Rafaël Bocquet, Ambrus Kaposi, and Christian Sattler. For the metatheory of type theory, internal sconing is enough. In Marco Gaboardi and Femke van Raamsdonk, editors, 8th International Conference on Formal Structures for Computation and Deduction, FSCD 2023, July 3-6, 2023, Rome, Italy, volume 260 of LIPIcs, pages 18:1-18:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.FSCD.2023.18.
  17. Paolo Capriotti. Notions of type formers. In Ambrus Kaposi, editor, 23rd International Conference on Types for Proofs and Programs, TYPES 2017. Eötvös Loránd University, 2017. URL: http://types2017.elte.hu/proc.pdf#page=77.
  18. John Cartmell. Generalised algebraic theories and contextual categories. Ann. Pure Appl. Log., 32:209-243, 1986. URL: https://doi.org/10.1016/0168-0072(86)90053-9.
  19. Simon Castellan, Pierre Clairambault, and Peter Dybjer. Categories with families: Unityped, simply typed, and dependently typed. CoRR, abs/1904.00827, 2019. URL: https://arxiv.org/abs/1904.00827.
  20. Thierry Coquand. Canonicity and normalization for dependent type theory. Theor. Comput. Sci., 777:184-191, 2019. URL: https://doi.org/10.1016/J.TCS.2019.01.015.
  21. Marcelo P. Fiore and Chung-Kil Hur. Second-order equational logic (extended abstract). In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of Lecture Notes in Computer Science, pages 320-335. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15205-4_26.
  22. Marcelo P. Fiore, Andrew M. Pitts, and S. C. Steenkamp. Quotients, inductive types, and quotient inductive types. Log. Methods Comput. Sci., 18(2), 2022. URL: https://doi.org/10.46298/LMCS-18(2:15)2022.
  23. Marcelo P. Fiore, Gordon D. Plotkin, and Daniele Turi. Abstract syntax and variable binding. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 193-202. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/LICS.1999.782615.
  24. Jonas Frey. Duality for clans: a refinement of gabriel-ulmer duality. CoRR, abs/2308.11967, 2023. URL: https://doi.org/10.48550/arXiv.2308.11967.
  25. Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. Definitional proof-irrelevance without K. Proc. ACM Program. Lang., 3(POPL):3:1-3:28, 2019. URL: https://doi.org/10.1145/3290316.
  26. Daniel Gratzer. Normalization for multimodal type theory. In Christel Baier and Dana Fisman, editors, LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, pages 2:1-2:13. ACM, 2022. URL: https://doi.org/10.1145/3531130.3532398.
  27. Robert Harper. Practical Foundations for Programming Languages (2nd. Ed.). Cambridge University Press, 2016. URL: https://www.cs.cmu.edu/%7Erwh/pfpl/index.html.
  28. Robert Harper. An equational logical framework for type theories. CoRR, abs/2106.01484, 2021. URL: https://arxiv.org/abs/2106.01484.
  29. Robert Harper, Furio Honsell, and Gordon D. Plotkin. A framework for defining logics. J. ACM, 40(1):143-184, 1993. URL: https://doi.org/10.1145/138027.138060.
  30. Philipp G. Haselwarter and Andrej Bauer. Finitary type theories with and without contexts. J. Autom. Reason., 67(4):36, 2023. URL: https://doi.org/10.1007/S10817-023-09678-Y.
  31. Martin Hofmann. Syntax and semantics of dependent types. In Semantics and Logics of Computation, pages 79-130. Cambridge University Press, 1997. Google Scholar
  32. Martin Hofmann. Semantical analysis of higher-order abstract syntax. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 204-213. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/LICS.1999.782616.
  33. Jasper Hugunin. Why not W? In Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch, editors, 26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy, volume 188 of LIPIcs, pages 8:1-8:9. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPICS.TYPES.2020.8.
  34. Jonas Kaiser, Steven Schäfer, and Kathrin Stark. Binder aware recursion over well-scoped de Bruijn syntax. In June Andronick and Amy P. Felty, editors, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018, pages 293-306. ACM, 2018. URL: https://doi.org/10.1145/3167098.
  35. Ambrus Kaposi. Formalisation of type checking into algebraic syntax. https://bitbucket.org/akaposi/tt-in-tt/src/master/Typecheck.agda, 2018.
  36. Ambrus Kaposi. Quotient inductive-inductive types and higher friends. Talk given at the Homotopy Type Theory Electronic Seminar Talks (HoTTEST), October 2020. URL: https://akaposi.github.io/pres_hottest.pdf.
  37. Ambrus Kaposi, Simon Huber, and Christian Sattler. Gluing for type theory. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany, volume 131 of LIPIcs, pages 25:1-25:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPICS.FSCD.2019.25.
  38. Ambrus Kaposi and András Kovács. A syntax for higher inductive-inductive types. In Hélène Kirchner, editor, 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK, volume 108 of LIPIcs, pages 20:1-20:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPICS.FSCD.2018.20.
  39. Ambrus Kaposi, András Kovács, and Thorsten Altenkirch. Constructing quotient inductive-inductive types. Proc. ACM Program. Lang., 3(POPL):2:1-2:24, 2019. URL: https://doi.org/10.1145/3290315.
  40. Ambrus Kaposi, András Kovács, and Ambroise Lafont. For finitary induction-induction, induction is enough. In Marc Bezem and Assia Mahboubi, editors, 25th International Conference on Types for Proofs and Programs, TYPES 2019, June 11-14, 2019, Oslo, Norway, volume 175 of LIPIcs, pages 6:1-6:30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPICS.TYPES.2019.6.
  41. Ambrus Kaposi and Szumi Xie. Type theory in type theory using single substitutions. In 30th International Conference on Types for Proofs and Programs. IT University of Copenhagen, 2024. Google Scholar
  42. András Kovács and Ambrus Kaposi. Large and infinitary quotient inductive-inductive types. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 648-661. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394770.
  43. András Kovács. Type-Theoretic Signatures for Algebraic Theories and Inductive Types. PhD thesis, Eötvös Loránd University, Hungary, 2022. https://arxiv.org/abs/2302.08837.
  44. Paul Blain Levy, John Power, and Hayo Thielecke. Modelling environments in call-by-value programming languages. Inf. Comput., 185(2):182-210, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00088-9.
  45. Hugo Moeneclaey. Parametricity and semi-cubical types. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-11. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470728.
  46. Pierre-Marie Pédrot. Russian constructivism in a prefascist theory. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 782-794. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394740.
  47. Brigitte Pientka and Jana Dunfield. Beluga: A framework for programming and reasoning with deductive systems (system description). In Jürgen Giesl and Reiner Hähnle, editors, Automated Reasoning, pages 15-21, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. Google Scholar
  48. Benjamin C. Pierce. Types and programming languages. MIT Press, 2002. Google Scholar
  49. Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, Cătălin Hriţcu, Vilhelm Sjöberg, Andrew Tolmach, and Brent Yorgey. Programming Language Foundations, volume 2 of Software Foundations. Electronic textbook, 2024. Version 6.5, URL: http://softwarefoundations.cis.upenn.edu.
  50. Jonathan Sterling. First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory. PhD thesis, Carnegie Mellon University, USA, 2022. URL: https://doi.org/10.1184/R1/19632681.V1.
  51. Jonathan Sterling and Carlo Angiuli. Normalization for cubical type theory. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021, pages 1-15. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470719.
  52. Taichi Uemura. Abstract and Concrete Type Theories. PhD thesis, University of Amsterdam, 2021. Google Scholar
  53. Philip Wadler, Wen Kokke, and Jeremy G. Siek. Programming Language Foundations in Agda. Online, August 2022. URL: https://plfa.inf.ed.ac.uk/22.08/.
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 Imprint Privacy Contact