1. A. Ahmed, D. Dreyer & A. Rossberg (2009): State-dependent representation independence. In: Principles of Programming Languages, pp. 340–353, doi:10.1145/1594834.1480925.
  2. R. Atkey (2012): Relational parametricity for higher kinds. In: Computer Science Logic, pp. 46–61.
  3. 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.
  4. R. Bird & L. Meertens (1998): Nested datatypes. In: Mathematics of Program Construction, pp. 52–67, doi:10.1007/BFb0054285.
  5. 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.
  6. 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.
  7. freeCodeCamp (2020): The Iron Triangle, or ``Pick Two".
  8. 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.
  9. J.-Y. Girard (1972): Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. University of Paris.
  10. G. Gonzalez (2021): The visitor pattern is essentially the same thing as Church encoding.
  11. 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.
  12. 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.
  13. 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.
  14. P. Johann (2003): Short cut fusion is correct. Journal of Functional Programming 13, pp. 797–814, doi:10.1017/S0956796802004409.
  15. 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.
  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.
  17. P. Johann & E. Ghiorzi (2022): (Deep) induction for GADTs. In: To appear, Certified Proofs and Programs.
  18. 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.
  19. 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.
  20. 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.
  21. 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.
  22. S. MacLane (1971): Categories for the Working Mathematician. Springer-Verlag.
  23. Y. Mandelbaum & A. Stump (2009): GADTs for the OCaml masses. In: Workshop on ML.
  24. Y. Minsky (2015): Why GADTs matter for performance.
  25. P. Morris & T. Altenkirch (2009): Indexed containers. In: Logic in Computer Science, pp. 277–285, doi:10.1017/S095679681500009X.
  26. 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.
  27. 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.
  28. C. Penner (2020): Simpler and safer API design using GADTs.
  29. A. Pitts (1998): Parametric polymorphism, recursive types, and operational equivalence. Unpublished manuscript.
  30. A. Pitts (2000): Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science 10, pp. 1–39, doi:10.1017/S0960129500003066.
  31. 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.
  32. J. C. Reynolds (1983): Types, abstraction, and parametric polymorphism. Information Processing 83(1), pp. 513–523.
  33. E. Riehl (2016): Category Theory in Context. Dover.
  34. TFCA (2019): Transfinite Construction of Free Algebras.
  35. D. Vytiniotis & S. Weirich (2006): Parametricity and GADTs.
  36. 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.
  37. P. Wadler (1989): Theorems for free!. In: Functional Programming Languages and Computer Architecture, pp. 347–359, doi:10.1145/99370.99404.

Comments and questions to:
For website issues: