@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},
)