All Media Types
Constructing quotient inductive-inductive types
Kaposi A., Kovács A., Altenkirch T. Proceedings of the ACM on Programming Languages 3(POPL): 1-24, 2019. Type: Article
At the core of Martin-Löf type theory (also known as “intuitionistic type theory”) are dependent types, that is, types whose definitions depend on values; these may be used to encode logical quantification. In general, a type may ...
Jul 9 2021
Reproduction in whole or in part without permission is prohibited. Copyright © 2000-2021 ThinkLoud, Inc.