% Bibliography downloaded from https://researchr.org/downloadbibtex/bibliography/25a1a247-2393-4332-8436-a6fb68bc4aea-datatype-generics/compact

@article{KaposiKA19,
  title = {Constructing quotient inductive-inductive types},
  author = {Ambrus Kaposi and András Kovács and Thorsten Altenkirch},
  year = {2019},
  url = {https://dl.acm.org/citation.cfm?id=3290315},
  researchr = {https://researchr.org/publication/KaposiKA19},
  cites = {0},
  citedby = {0},
  journal = {PACMPL},
  volume = {3},
}

@book{nordstrom1990programming,
  title = {Programming in Martin-L{\"o}f's type theory},
  author = {Nordström, Bengt and Petersson, Kent and Smith, Jan M},
  year = {1990},
  researchr = {https://researchr.org/publication/nordstrom1990programming},
  cites = {0},
  citedby = {0},
  volume = {200},
  publisher = {Oxford University Press},
}

@inproceedings{HinzeJ03,
  title = {Generic Haskell: Practice and Theory},
  author = {Ralf Hinze and Johan  Jeuring},
  year = {2003},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2793&spage=1},
  tags = {Haskell},
  researchr = {https://researchr.org/publication/HinzeJ03},
  cites = {0},
  citedby = {0},
  pages = {1-56},
  booktitle = {ac},
}

@inproceedings{WeirichC10,
  title = {Arity-generic datatype-generic programming},
  author = {Stephanie Weirich and Chris Casinghino},
  year = {2010},
  doi = {10.1145/1707790.1707799},
  url = {http://doi.acm.org/10.1145/1707790.1707799},
  tags = {programming languages, data-flow language, generic programming, Haskell, data-flow programming, data-flow, programming},
  researchr = {https://researchr.org/publication/WeirichC10},
  cites = {0},
  citedby = {0},
  pages = {15-26},
  booktitle = {plpv},
}

@article{CockxD18,
  title = {Proof-relevant unification: Dependent pattern matching with only the axioms of your type theory},
  author = {Jesper Cockx and Dominique Devriese},
  year = {2018},
  doi = {10.1017/S095679681800014X},
  url = {https://doi.org/10.1017/S095679681800014X},
  researchr = {https://researchr.org/publication/CockxD18},
  cites = {0},
  citedby = {0},
  journal = {JFP},
  volume = {28},
}

@inproceedings{ChapmanDMM10,
  title = {The gentle art of levitation},
  author = {James Chapman and Pierre-Évariste Dagand and Conor McBride and Peter Morris},
  year = {2010},
  doi = {10.1145/1863543.1863547},
  url = {http://doi.acm.org/10.1145/1863543.1863547},
  researchr = {https://researchr.org/publication/ChapmanDMM10},
  cites = {0},
  citedby = {0},
  pages = {3-14},
  booktitle = {ICFP},
}

@book{klabnik2019rust,
  title = {The Rust Programming Language (Covers Rust 2018)},
  author = {Klabnik, Steve and Nichols, Carol},
  year = {2019},
  researchr = {https://researchr.org/publication/klabnik2019rust},
  cites = {0},
  citedby = {0},
  publisher = {No Starch Press},
}

@phdthesis{diehl2017fully,
  title = {Fully Generic Programming over Closed Universes of Inductive-Recursive Types},
  author = {Diehl, Larry},
  year = {2017},
  url = {https://pdxscholar.library.pdx.edu/cgi/viewcontent.cgi?article=4656&context=open_access_etds},
  researchr = {https://researchr.org/publication/diehl2017fully},
  cites = {0},
  citedby = {0},
  school = {Portland State University},
}

@book{leroy2020ocaml-0,
  title = {The OCaml system release 4.11: Documentation and user's manual},
  author = {Leroy, Xavier and Doligez, Damien and Frisch, Alain and Garrigue, Jacques and R{\'e}my, Didier and Vouillon, J{\'e}r{\^o}me},
  year = {2020},
  researchr = {https://researchr.org/publication/leroy2020ocaml-0},
  cites = {0},
  citedby = {0},
}

@mastersthesis{andjelkovic2011family,
  title = {A family of universes for generic programming},
  author = {Andjelkovic, Stevan},
  year = {2011},
  url = {https://publications.lib.chalmers.se/records/fulltext/146810.pdf},
  researchr = {https://researchr.org/publication/andjelkovic2011family},
  cites = {0},
  citedby = {0},
}

@inproceedings{DybjerS99,
  title = {A Finite Axiomatization of Inductive-Recursive Definitions},
  author = {Peter Dybjer and Anton Setzer},
  year = {1999},
  url = {http://link.springer.de/link/service/series/0558/bibs/1581/15810129.htm},
  researchr = {https://researchr.org/publication/DybjerS99},
  cites = {0},
  citedby = {0},
  pages = {129-146},
  booktitle = {tlca},
}

@inproceedings{ChristiansenB16,
  title = {Elaborator reflection: extending Idris in Idris},
  author = {David Christiansen and Edwin Brady},
  year = {2016},
  doi = {10.1145/2951913.2951932},
  url = {http://doi.acm.org/10.1145/2951913.2951932},
  researchr = {https://researchr.org/publication/ChristiansenB16},
  cites = {0},
  citedby = {0},
  pages = {284-297},
  booktitle = {ICFP},
}

@inproceedings{JanssonJ97,
  title = {Polyp - A Polytypic Programming Language},
  author = {Patrik Jansson and Johan  Jeuring},
  year = {1997},
  doi = {10.1145/263699.263763},
  url = {http://doi.acm.org/10.1145/263699.263763},
  tags = {programming languages, polytypic programming, programming, polytypic},
  researchr = {https://researchr.org/publication/JanssonJ97},
  cites = {0},
  citedby = {0},
  pages = {470-482},
  booktitle = {POPL},
}

@inproceedings{VerbruggenVH08,
  title = {Polytypic programming in COQ},
  author = {Wendy Verbruggen and Edsko de Vries and Arthur Hughes},
  year = {2008},
  doi = {10.1145/1411318.1411326},
  url = {http://doi.acm.org/10.1145/1411318.1411326},
  tags = {proof assistant, generic programming, polytypic programming, Haskell, programming, polytypic},
  researchr = {https://researchr.org/publication/VerbruggenVH08},
  cites = {0},
  citedby = {0},
  pages = {49-60},
  booktitle = {ICFP},
}

@phdthesis{ethos-354,
  title = {A cosmology of datatypes : reusability and dependent types},
  author = {Pierre-Évariste Dagand},
  year = {2013},
  url = {http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.605921},
  note = {British Library, EThOS},
  researchr = {https://researchr.org/publication/ethos-354},
  cites = {0},
  citedby = {0},
  school = {University of Strathclyde, Glasgow, UK},
}

@misc{dagand2012elaborating,
  title = {Elaborating Inductive Definitions},
  author = {Pierre-Evariste Dagand and Conor McBride},
  year = {2012},
  researchr = {https://researchr.org/publication/dagand2012elaborating},
  cites = {0},
  citedby = {0},
}

@inproceedings{Brady21-1,
  title = {Idris 2: Quantitative Type Theory in Practice},
  author = {Edwin C. Brady},
  year = {2021},
  doi = {10.4230/LIPIcs.ECOOP.2021.9},
  url = {https://doi.org/10.4230/LIPIcs.ECOOP.2021.9},
  tags = {Intrinsic-Verification},
  researchr = {https://researchr.org/publication/Brady21-1},
  cites = {0},
  citedby = {0},
  booktitle = {ECOOP},
}

@article{BohmB85,
  title = {Automatic Synthesis of Typed Lambda-Programs on Term Algebras},
  author = {Corrado Böhm and Alessandro Berarducci},
  year = {1985},
  tags = { algebra},
  researchr = {https://researchr.org/publication/BohmB85},
  cites = {0},
  citedby = {0},
  journal = {TCS},
  volume = {39},
  pages = {135-154},
}

@phdthesis{ethos-14251,
  title = {Inductive-inductive definitions},
  author = {Fredrik Nordvall Forsberg},
  year = {2013},
  url = {https://cronfa.swan.ac.uk/Record/cronfa43083},
  note = {British Library, EThOS},
  researchr = {https://researchr.org/publication/ethos-14251},
  cites = {0},
  citedby = {0},
  school = {Swansea University, UK},
}

@inproceedings{AltenkirchMM06,
  title = {Generic Programming with Dependent Types},
  author = {Thorsten Altenkirch and Conor McBride and Peter Morris},
  year = {2006},
  doi = {10.1007/978-3-540-76786-2_4},
  url = {http://dx.doi.org/10.1007/978-3-540-76786-2_4},
  researchr = {https://researchr.org/publication/AltenkirchMM06},
  cites = {0},
  citedby = {0},
  pages = {209-257},
  booktitle = {ssdgp},
}

@inproceedings{BernardyJP10,
  title = {Parametricity and dependent types},
  author = {Jean-Philippe Bernardy and Patrik Jansson and Ross Paterson},
  year = {2010},
  doi = {10.1145/1863543.1863592},
  url = {http://doi.acm.org/10.1145/1863543.1863592},
  tags = {translation, constraints, type system, logic, abstraction},
  researchr = {https://researchr.org/publication/BernardyJP10},
  cites = {0},
  citedby = {0},
  pages = {345-356},
  booktitle = {ICFP},
}

@book{0000395,
  title = {Intuitionistic type theory},
  author = {Per Martin-Löf},
  year = {1984},
  researchr = {https://researchr.org/publication/0000395},
  cites = {0},
  citedby = {0},
  volume = {1},
  series = {Studies in proof theory},
  publisher = {Bibliopolis},
  isbn = {978-88-7088-228-5},
}

@book{abrahams2004c-,
  title = {C++ template metaprogramming: concepts, tools, and techniques from Boost and beyond},
  author = {Abrahams, David and Gurtovoy, Aleksey},
  year = {2004},
  researchr = {https://researchr.org/publication/abrahams2004c-},
  cites = {0},
  citedby = {0},
  publisher = {Pearson Education},
}

@book{jones2003haskell,
  title = {Haskell 98 language and libraries: the revised report},
  author = {Jones, Simon Peyton},
  year = {2003},
  researchr = {https://researchr.org/publication/jones2003haskell},
  cites = {0},
  citedby = {0},
  publisher = {Cambridge University Press},
}

@article{McBride2018,
  title = {Everybody's Got To Be Somewhere},
  author = {Conor McBride},
  year = {2018},
  month = {Jul},
  doi = {10.4204/eptcs.275.6},
  url = {http://dx.doi.org/10.4204/EPTCS.275.6},
  researchr = {https://researchr.org/publication/McBride2018},
  cites = {0},
  citedby = {0},
  journal = {Electronic Proceedings in Theoretical Computer Science},
  volume = {275},
  pages = {53-69},
}

@article{MorrisAG09,
  title = {A Universe of Strictly Positive Families},
  author = {Peter Morris and Thorsten Altenkirch and Neil Ghani},
  year = {2009},
  doi = {10.1142/S0129054109006462},
  url = {http://dx.doi.org/10.1142/S0129054109006462},
  researchr = {https://researchr.org/publication/MorrisAG09},
  cites = {0},
  citedby = {0},
  journal = {ijfcs},
  volume = {20},
  number = {1},
  pages = {83-107},
}

@article{SheardJ02,
  title = {Template meta-programming for Haskell},
  author = {Tim  Sheard and Simon L. Peyton Jones},
  year = {2002},
  doi = {10.1145/636517.636528},
  url = {http://doi.acm.org/10.1145/636517.636528},
  tags = {programming languages, optimization, meta programming, data-flow language, meta-model, functional programming, polytypic programming, template meta-programming, language design, Haskell, macros, data-flow programming, data-flow, code generation, compiler, programming, program optimization, Meta-Environment, polytypic, design, meta-objects},
  researchr = {https://researchr.org/publication/SheardJ02},
  cites = {0},
  citedby = {0},
  journal = {SIGPLAN},
  volume = {37},
  number = {12},
  pages = {60-75},
}

@inproceedings{McBrideGM04,
  title = {A Few Constructions on Constructors},
  author = {Conor McBride and Healfdene Goguen and James McKinna},
  year = {2004},
  doi = {10.1007/11617990_12},
  url = {http://dx.doi.org/10.1007/11617990_12},
  researchr = {https://researchr.org/publication/McBrideGM04},
  cites = {0},
  citedby = {0},
  pages = {186-200},
  booktitle = {TYPES},
}

@article{Jay95,
  title = {A Semantics for Shape},
  author = {C. Barry Jay},
  year = {1995},
  tags = {semantics, C++},
  researchr = {https://researchr.org/publication/Jay95},
  cites = {0},
  citedby = {0},
  journal = {SCP},
  volume = {25},
  number = {2-3},
  pages = {251-283},
}

@misc{ppxlib-manual,
  title = {ppxlib's user manual},
  author = {Jane Street Group, LLC},
  year = {2018},
  url = {https://github.com/ocaml-ppx/ppx_deriving},
  researchr = {https://researchr.org/publication/ppxlib-manual},
  cites = {0},
  citedby = {0},
}

@article{BirdMH96,
  title = {Generic Functional Programming with Types and Relations},
  author = {Richard S. Bird and Oege de Moor and Paul F. Hoogendijk},
  year = {1996},
  tags = {generic programming, functional programming, programming},
  researchr = {https://researchr.org/publication/BirdMH96},
  cites = {0},
  citedby = {0},
  journal = {JFP},
  volume = {6},
  number = {1},
  pages = {1-28},
}

@inproceedings{DiehlS13,
  title = {Leveling up dependent types: generic programming over a predicative hierarchy of universes},
  author = {Larry Diehl and Tim Sheard},
  year = {2013},
  doi = {10.1145/2502409.2502414},
  url = {http://doi.acm.org/10.1145/2502409.2502414},
  researchr = {https://researchr.org/publication/DiehlS13},
  cites = {0},
  citedby = {0},
  pages = {49-60},
  booktitle = {ICFP},
}

@inproceedings{ForsbergS10,
  title = {Inductive-Inductive Definitions},
  author = {Fredrik Nordvall Forsberg and Anton Setzer},
  year = {2010},
  doi = {10.1007/978-3-642-15205-4_35},
  url = {http://dx.doi.org/10.1007/978-3-642-15205-4_35},
  researchr = {https://researchr.org/publication/ForsbergS10},
  cites = {0},
  citedby = {0},
  pages = {454-468},
  booktitle = {csl},
}

@article{Dybjer00,
  title = {A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory},
  author = {Peter Dybjer},
  year = {2000},
  tags = {type theory},
  researchr = {https://researchr.org/publication/Dybjer00},
  cites = {0},
  citedby = {0},
  journal = {JSYML},
  volume = {65},
  number = {2},
  pages = {525-549},
}

@inproceedings{DiehlS14,
  title = {Generic constructors and eliminators from descriptions: type theory as a dependently typed internal DSL},
  author = {Larry Diehl and Tim Sheard},
  year = {2014},
  doi = {10.1145/2633628.2633630},
  url = {http://doi.acm.org/10.1145/2633628.2633630},
  researchr = {https://researchr.org/publication/DiehlS14},
  cites = {0},
  citedby = {0},
  pages = {3-14},
  booktitle = {ICFP},
}

@mastersthesis{sijsling2016generic,
  title = {Generic programming with ornaments and dependent types},
  author = {Sijsling, Yorick},
  year = {2016},
  researchr = {https://researchr.org/publication/sijsling2016generic},
  cites = {0},
  citedby = {0},
}

@article{DybjerS03,
  title = {Induction-recursion and initial algebras},
  author = {Peter Dybjer and Anton Setzer},
  year = {2003},
  doi = {10.1016/S0168-0072(02)00096-9},
  url = {http://dx.doi.org/10.1016/S0168-0072(02)00096-9},
  tags = { algebra},
  researchr = {https://researchr.org/publication/DybjerS03},
  cites = {0},
  citedby = {0},
  journal = {APAL},
  volume = {124},
  number = {1-3},
  pages = {1-47},
}

@article{AbbottAG05,
  title = {Containers: Constructing strictly positive types},
  author = {Michael Abbott and Thorsten Altenkirch and Neil Ghani},
  year = {2005},
  doi = {10.1016/j.tcs.2005.06.002},
  url = {http://dx.doi.org/10.1016/j.tcs.2005.06.002},
  researchr = {https://researchr.org/publication/AbbottAG05},
  cites = {0},
  citedby = {0},
  journal = {TCS},
  volume = {342},
  number = {1},
  pages = {3-27},
}

@article{BenkeDJ03,
  title = {Universes for Generic Programs and Proofs in Dependent Type Theory},
  author = {Marcin Benke and Peter Dybjer and Patrik Jansson},
  year = {2003},
  tags = {generic programming, type theory},
  researchr = {https://researchr.org/publication/BenkeDJ03},
  cites = {0},
  citedby = {0},
  journal = {njc},
  volume = {10},
  number = {4},
  pages = {265-289},
}

@phdthesis{ethos-4751,
  title = {Constructing Universes for Generic Programming},
  author = {Peter W. J. Morris},
  year = {2007},
  url = {http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.519405},
  note = {British Library, EThOS},
  researchr = {https://researchr.org/publication/ethos-4751},
  cites = {0},
  citedby = {0},
  school = {University of Nottingham, UK},
}