This repository holds the Agda development of my internship in the MSP group with Conor McBride. Report
References:
- Neil Ghani, Conor McBride, Fredrik Nordvall Forsberg, and Stephan Spahn. Variation on Inductive-Recursive Definitions. MFCS '17, 63:1–13, 2017.
- Peter Dybjer, and Anton Setzer. Indexed induction-recursion. Journal of Logic and Algebraic Programming, 66(1):1–49, 2006.
- Conor McBride. Ornamental Algebras, Algebraic Ornaments. Preprint, 2011.
- Robert Atkey, Patricia Johann, and Neil Ghani. When is a Type Refinement an Inductive Type? FOSSACS '11, 6604:72–87, 2011.
- Pierre-Évariste Dagand, and Conor McBride. Transporting functions across Ornaments. Journal of Functional Programming, 24(2–3):316–383.
- Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, and Peter Morris. Indexed Containers. Journal of Functional Programming, 25:e5, 2015.
- Edwin Brady, Conor McBride, and James McKinna. Inductive Families Need Not Store Their Indices. TYPES '03, 3085:115–129, 2003.
- Peter Hancock, Conor McBride, Neil Ghani, Lorenzo Malatesta, and Thorsten Altenkirch. Small Induction-Recursion. TCLA '13, 156–172, 2013.
- Guillaume Allais, Robert Atkey, James Chapman, Conor McBride, and James McKinna. A Type and Scope Safe Universe of Syntaxes with Bindings, Their Semantics and Proofs. ICFP '18, 2018.