@inproceedings(adr09,
 author       = {A. Ahmed and D. Dreyer and A. Rossberg},
 year         = {2009},
 title        = {State-dependent representation independence},
 booktitle    = {Principles of Programming Languages},
 pages        = {340--353},
 doi          = {10.1145/1594834.1480925},
)
@inproceedings(atk12,
 author       = {R. Atkey},
 year         = {2012},
 title        = {Relational parametricity for higher kinds},
 booktitle    = {Computer Science Logic},
 pages        = {46--61},
)
@inproceedings(agj14,
 author       = {R. Atkey and N. Ghani and P. Johann},
 year         = {2014},
 title        = {A Relationally Parametric Model of Dependent Type Theory},
 booktitle    = {Principles of Programming Languages},
 pages        = {503--516},
 doi          = {10.1145/2535838.2535852},
)
@inproceedings(bm98,
 author       = {R. Bird and L. Meertens},
 year         = {1998},
 title        = {Nested datatypes},
 booktitle    = {Mathematics of Program Construction},
 pages        = {52--67},
 doi          = {10.1007/BFb0054285},
)
@article(blw03,
 author       = {M. R. Bush and M. Leeming and R. F. C. Walters},
 year         = {2003},
 title        = {Computing left {K}an extensions},
 journal      = {Journal of Symbolic Computation},
 volume       = {35},
 pages        = {107--126},
 doi          = {10.1016/S0747-7171(02)00102-5},
)
@article(dnb12,
 author       = {D. Dreyer and G. Neis and L. Birkedal},
 year         = {2012},
 title        = {The impact of higher-order state and control effects on local relational reasoning},
 journal      = {Journal of Functional Programming},
 volume       = {22},
 pages        = {477--528},
 doi          = {10.1145/1863543.1863566},
)
@misc(iron-triangle,
 author       = {freeCodeCamp},
 year         = {2020},
 title        = {The Iron Triangle, or ``Pick Two"},
 howpublished = {\url{https://www.freecodecamp.org/news/the-iron-triangle-or-pick-two/}},
)
@inproceedings(gh03,
 author       = {N. Gambino and M. Hyland},
 year         = {2003},
 title        = {Well-founded trees and dependent polynomial functors},
 booktitle    = {TYPES},
 pages        = {210--225},
 doi          = {10.1007/978-3-540-24849-1\_14},
)
@phdthesis(gir72,
 author       = {J.-Y. Girard},
 year         = {1972},
 title        = {Interpr\'etation fonctionnelle et \'elimination des coupures de l'arithm\IeC{\'e}tique d'ordre sup\'erieur},
 school       = {University of Paris},
)
@misc(gon21,
 author       = {G. Gonzalez},
 year         = {2021},
 title        = {The visitor pattern is essentially the same thing as Church encoding},
 howpublished = {\url{https://www.haskellforall.com/2021/01/the-visitor-pattern-is-essentially-same.html}},
)
@inproceedings(hf11,
 author       = {M. Hamama and M. Fiore},
 year         = {2011},
 title        = {A foundation for GADTs and inductive families: Dependent polynomial functor approach},
 booktitle    = {Workshop on Generic Programming},
 pages        = {59--70},
 doi          = {10.1145/2036918.2036927},
)
@inproceedings(hd11,
 author       = {C.-K. Hur and D. Dreyer},
 year         = {2011},
 title        = {A Kriple logical relation between ML and assembly},
 booktitle    = {Principles of Programming Languages},
 pages        = {133--146},
 doi          = {10.1145/1926385.1926402},
)
@article(joh02,
 author       = {P.\ Johann},
 year         = {2002},
 title        = {A generalization of short-cut fusion and its correctness proof},
 journal      = {Higher-Order and Symbolic Computation},
 volume       = {15},
 pages        = {273--300},
 doi          = {10.1023/A:1022982420888},
)
@article(joh03,
 author       = {P.\ Johann},
 year         = {2003},
 title        = {Short cut fusion is correct},
 journal      = {Journal of Functional Programming},
 volume       = {13},
 pages        = {797--814},
 doi          = {10.1017/S0956796802004409},
)
@inproceedings(jg07,
 author       = {P. Johann and N. Ghani},
 year         = {2007},
 title        = {Initial algebra semantics is enough!},
 booktitle    = {Typed Lambda Calculus and Applications},
 pages        = {207--222},
 doi          = {10.1007/978-3-540-73228-0\_16},
)
@inproceedings(jg08,
 author       = {P. Johann and N. Ghani},
 year         = {2008},
 title        = {Foundations for structured programming with GADTs},
 booktitle    = {Principles of Programming Languages},
 pages        = {297--308},
 doi          = {10.1145/1328438.1328475},
)
@inproceedings(jg22,
 author       = {P. Johann and E. Ghiorzi},
 year         = {2022},
 title        = {(Deep) induction for GADTs},
 booktitle    = {To appear, Certified Proofs and Programs},
)
@inproceedings(jgj21,
 author       = {P. Johann and E. Ghiorzi and D. Jeffries},
 year         = {2021},
 title        = {Parametricity for primitive nested types},
 booktitle    = {Foundations of Software Science and Computation Structures},
 pages        = {234--343},
 doi          = {10.1007/978-3-030-71995-1\_17},
)
@inproceedings(jp19,
 author       = {P. Johann and A. Polonsky},
 year         = {2019},
 title        = {Higher-kinded data types: Syntax and semantics},
 booktitle    = {Logic in Computer Science},
 pages        = {1--13},
 doi          = {10.1109/LICS.2019.8785657},
)
@inproceedings(jp20,
 author       = {P. Johann and A. Polonsky},
 year         = {2020},
 title        = {Deep Induction: Induction rules for (truly) nested types},
 booktitle    = {Foundations of Software Science and Computation Structures},
 pages        = {339--358},
 doi          = {10.1007/978-3-030-45231-5\_18},
)
@inproceedings(pvww06,
 author       = {{P}eyton {J}ones, S. L. and D. Vytiniotis and G. Washburn and S. Weirich},
 year         = {2006},
 title        = {Simple unification-based type inference for GADTs},
 booktitle    = {International Conference on Functional Programming},
 pages        = {50--61},
 doi          = {10.1145/1160074.1159811},
)
@book(mac71,
 author       = {S. MacLane},
 year         = {1971},
 title        = {Categories for the Working Mathematician},
 publisher    = {Springer-Verlag},
)
@inproceedings(ms09,
 author       = {Y. Mandelbaum and A. Stump},
 year         = {2009},
 title        = {GADTs for the OCaml masses},
 booktitle    = {Workshop on ML},
)
@misc(min15,
 author       = {Y. Minsky},
 year         = {2015},
 title        = {Why {GADT}s matter for performance},
 howpublished = {\url{https://blog.janestreet.com/why-gadts-matter-for-performance/}},
)
@inproceedings(ma09,
 author       = {P. Morris and T. Altenkirch},
 year         = {2009},
 title        = {Indexed containers},
 booktitle    = {Logic in Computer Science},
 pages        = {277--285},
 doi          = {10.1017/S095679681500009X},
)
@inproceedings(owg08,
 author       = {B. {C. d. S.} Oliveira and M. Wang and J. Gibbons},
 year         = {2008},
 title        = {The visitor pattern as a reusable, generic, type-safe component},
 booktitle    = {Object-Oriented Programming: Systems, Languages, Applications},
 pages        = {439--456},
 doi          = {10.1145/1449764.1449799},
)
@inproceedings(pl04,
 author       = {E. Pasalic and N. Linger},
 year         = {2004},
 title        = {Meta-programming with typed object-language representations},
 booktitle    = {Generic Programming and Component Engineering},
 pages        = {136--167},
 doi          = {10.1007/978-3-540-30175-2\_8},
)
@misc(pen20,
 author       = {C. Penner},
 year         = {2020},
 title        = {Simpler and safer {API} design using {GADT}s},
 howpublished = {\url{https://chrispenner.ca/posts/gadt-design}},
)
@unpublished(pit98,
 author       = {A. Pitts},
 year         = {1998},
 title        = {Parametric polymorphism, recursive types, and operational equivalence},
 note         = {Unpublished manuscript},
)
@article(pit00,
 author       = {A. Pitts},
 year         = {2000},
 title        = {Parametric polymorphism and operational equivalence},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {10},
 pages        = {1--39},
 doi          = {10.1017/S0960129500003066},
)
@inproceedings(pr06,
 author       = {F. Pottier and R{\'e}gis-Gianas, Y.},
 year         = {2006},
 title        = {Stratified type inference for generalized algebraic data types},
 booktitle    = {Principles of Programming Languages},
 pages        = {232--244},
 doi          = {10.1145/1111320.1111058},
)
@article(rey83,
 author       = {J. C. Reynolds},
 year         = {1983},
 title        = {Types, abstraction, and parametric polymorphism},
 journal      = {Information Processing},
 volume       = {83(1)},
 pages        = {513--523},
)
@book(rie16,
 author       = {E. Riehl},
 year         = {2016},
 title        = {Category Theory in Context},
 publisher    = {Dover},
)
@misc(tfca,
 author       = {TFCA},
 year         = {2019},
 title        = {Transfinite Construction of Free Algebras},
 howpublished = {\url{http://ncatlab.org/nlab/show/transfinite+construction+of+free+algebras}},
)
@misc(vw06,
 author       = {D. Vytiniotis and S. Weirich},
 year         = {2006},
 title        = {Parametricity and GADTs},
 howpublished = {\url{https://www.cis.upenn.edu/~sweirich//talks/param-gadt.pdf}},
)
@article(vw10,
 author       = {D. Vytiniotis and S. Weirich},
 year         = {2010},
 title        = {Parametricity, type equality, and higher-order polymorphism},
 journal      = {Journal of Functional Programming},
 volume       = {20\tmspace+\thinmuskip{.1667em}(2)},
 pages        = {175--210},
 doi          = {10.1017/S0956796810000079},
)
@inproceedings(wad89,
 author       = {P.\ Wadler},
 year         = {1989},
 title        = {Theorems for free!},
 booktitle    = {Functional Programming Languages and Computer Architecture},
 pages        = {347--359},
 doi          = {10.1145/99370.99404},
)