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