Towards Formalizing Parametricity For Nested Types In Agda
- ASU Author/Contributor (non-ASU co-authors, if there are any, appear on document)
- Daniel Jeffries (Creator)
- Institution
- Appalachian State University (ASU )
- Web Site: https://library.appstate.edu/
- Advisor
- Patricia Johann
Abstract: Recent work by Johann, Ghiorzi, and Jeffries presents a Hindley-Milner-style calculus whose type system includes a primitive type formation rule for constructing nested types directly as fixpoints. The term calculus for this type system supports primitive pattern matching, functorial map functions, and fold combinators for nested types. A parametric model of the calculus is given in terms of category theory, using fixpoints of higher-order functors to interpret nested types. In this thesis, we formalize the syntax of the calculus and partially formalize its model in the proof assistant and functional programming language Agda. To prove a proposition in Agda, the user first gives a formal definition of the proposition as a type T. Then the user defines a function of type T, and Agda's type-checker checks whether the user-defined function has the correct type. Since the model is defined in terms of category theory, we use the agda-categories library to formalize the categorical constructs used in the model. We introduce the syntax and semantics of the calculus as they are being formalized.
Towards Formalizing Parametricity For Nested Types In Agda
PDF (Portable Document Format)
751 KB
Created on 1/13/2022
Views: 721
Additional Information
- Publication
- Thesis
- Jeffries, D. (2021). Towards Formalizing Parametricity For Nested Types In Agda. Unpublished Master’s Thesis. Appalachian State University, Boone, NC.
- Language: English
- Date: 2021
- Keywords
- Agda,
parametricity,
nested types,
proof assistant,
functional programming