Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Transpiling Programming Computable Functions to Answer Set Programs Read chapter Read first chapter

2019 | OriginalPaper | Chapter

Code Generation for Higher Inductive Types

A Study in Agda Metaprogramming

Author : Paventhan Vivekanandan

Published in: Functional and Constraint Logic Programming

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Higher inductive types are inductive types that include nontrivial higher-dimensional structure, represented as identifications that are not reflexivity. While work proceeds on type theories with a computational interpretation of univalence and higher inductive types, it is convenient to encode these structures in more traditional type theories with mature implementations. However, these encodings involve a great deal of error-prone additional syntax. We present a library that uses Agda’s metaprogramming facilities to automate this process, allowing higher inductive types to be specified with minimal additional syntax.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Transpiling Programming Computable Functions to Answer Set Programs
next chapter Measuring Coverage of Prolog Programs Using Mutation Testing
Footnotes
Literature
1.
2.
Abbott, M., Altenkirch, T., Ghani, N.: Containers: constructing strictly positive types. Theor. Comput. Sci. 342(1), 3–27 (2005)MathSciNetCrossRef
3.
Altenkirch, T.: Containers in homotopy type theory, talk at Mathematical Structures of Computation, January 2014
4.
5.
Angiuli, C., Harper, R., Wilson, T.: Computational higher-dimensional type theory. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL, Paris, France, pp. 680–693, January 2017
6.
Angiuli, C., Morehouse, E., Licata, D.R., Harper, R.: Homotopical patch theory. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP, Gothenburg, Sweden, September 2014
7.
Basold, H., Geuvers, H., van der Weide, N.: Higher inductive types in programming. J. Univ. Comput. Sci. 23(1), 63–88 (2017)MathSciNet
8.
Brunerie, G.: Custom definitional equalities in agda, talk at Univalent Foundations and Proof Assistants session of the 5th International Congress on Mathematical Software, July 2016
9.
10.
Chapman, J., Évariste Dagand, P., McBride, C., Morris, P.: The gentle art of levitation. In: Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP, Baltimore, USA, September 2010
11.
Christiansen, D.: Practical reflection and metaprogramming for dependent types. Ph.D. thesis, IT University of Copenhagen (2016)
12.
Christiansen, D., Brady, E.: Elaborator reflection: extending Idris in Idris. In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP, Nara, Japan, September 2016
13.
Cockx, J., Abel, A.: Sprinkles of extensionality for your vanilla type theory. In: 22nd International Conference on Types for Proofs and Programs, May 2016
14.
Cockx, J., Devriese, D., Piessens, F.: Pattern matching without K. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP, Gothenburg, Sweden, pp. 257–268, September 2014
15.
Cohen, C., Coquand, T., Huber, S., Mörtberg, A.: Cubical type theory: a constructive interpretation of the univalence axiom. In: Proceedings of the 21st International Conference on Types for Proofs and Programs, Tallinn, Estonia, May 2015
16.
17.
Dybjer, P., Moeneclaey, H.: Finitary higher inductive types in the groupoid model. Electro. Notes Theor. Comput. Sci. 336, 119–134 (2018)MathSciNetCrossRef
18.
Ebner, G., Ullrich, S., Roesch, J., Avigad, J., de Moura, L.: A metaprogramming framework for formal verification. In: Proceedings of the 22nd ACM SIGPLAN International Conference on Functional Programming, ICFP, September 2017
19.
Kaposi, A., Kovács, A.: A syntax for higher inductive-inductive types. In: Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, FSCD, Oxford, UK, July 2018
20.
21.
22.
Löh, A., Magalhães, J.P.: Generic programming with indexed functors. In: Proceedings of the 7th ACM SIGPLAN Workshop on Generic Programming, WGP, September 2011
23.
Mimram, S., Giusto, C.D.: A categorical theory of patches. Electron. Notes Theor. Comput. Sci. 298, 283–307 (2013)MathSciNetCrossRef
24.
Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Chalmers University of Technology, Göteborg, Sweden (2007)
25.
26.
Popa, R.A., Redfield, C.M., Zeldovich, N., Balakrishnan, H.: CryptDB: protecting confidentiality with encrypted query processing. In: Proceedings of the 23rd ACM Symposium on Operating Systems Principles, SOSP, Cascais, Portugal (2011)
27.
Roundy, D.: Darcs: distributed version management in haskell. In: Proceedings of the 2005 ACM SIGPLAN Workshop on Haskell, September 2005
28.
Stutterheim, J., Swierstra, W., Swierstra, S.D.: Forty hours of declarative programming: teaching prolog at the junior college utrecht. Electron. Proc. Theor. Comput. Sci. 106, 50–62 (2013)CrossRef
29.
30.
Vivekanandan, P.: HoTT-Crypt: a study in homotopy type theory based on cryptography. In: Short Paper proceedings of the 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR-22, Ethiopia, November 2018. https://​doi.​org/​10.​29007/​tvpp
31.
van der Walt, P.: Reflection in agda. Master’s thesis. Utrecht University, Utrecht, Netherlands (2012)
32.
Metadata
Title
Code Generation for Higher Inductive Types
Author
Paventhan Vivekanandan
Copyright Year
2019
Book
Functional and Constraint Logic Programming

Print ISBN: 978-3-030-16201-6

Electronic ISBN: 978-3-030-16202-3

Copyright Year: 2019

DOI
https://doi.org/10.1007/978-3-030-16202-3_2

Premium Partner

    Image Credits