Skip to main content

Research Repository

Advanced Search

Type theory in type theory using quotient inductive types

Altenkirch, Thorsten; Kaposi, Ambrus

Authors

Ambrus Kaposi auk@Cs.Nott.AC.UK



Abstract

We present an internal formalisation of a type heory with dependent types in Type Theory using a special case of higher inductive types from Homotopy Type Theory which we call quotient inductive types (QITs). Our formalisation of type theory avoids referring to preterms or a typability relation but defines directly well typed objects by an inductive definition. We use the elimination principle to define the set-theoretic and logical predicate interpretation. The work has been formalized using the Agda system extended with QITs using postulates.

Publication Date Jan 22, 2016
Journal Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Peer Reviewed Peer Reviewed
APA6 Citation Altenkirch, T., & Kaposi, A. (2016). Type theory in type theory using quotient inductive types
Keywords Higher Inductive Types, Homotopy Type Theory, Logical
Relations, Metaprogramming, Agda
Publisher URL http://dl.acm.org/citation.cfm?doid=2837614.2837638
Copyright Statement Copyright information regarding this work can be found at the following address: http://eprints.nottingh.../end_user_agreement.pdf
Additional Information Published in: POPL '16 Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York : ACM, c2016, p. 18-29.
ISBN: 9781450335492 doi:10.1145/2837614.2837638

Files

popl16main-mainpopl16-157-p-6ba8421-25791-preprint.pdf (336 Kb)
PDF

Copyright Statement
Copyright information regarding this work can be found at the following address: http://eprints.nottingham.ac.uk/end_user_agreement.pdf





You might also like



Downloadable Citations

;