src/HOL/Data_Structures/document/root.bib

Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context

@techreport{Adams-TR92,author="Stephen Adams",
title="Implementing Sets Efficiently in a Functional Language",
institution="University of Southampton, Department of Electronics and Computer Science",number="CSTR 92-10",year=1992}

@article{Adams-JFP93,
  author    = {Stephen Adams},
  title     = {Efficient Sets - {A} Balancing Act},
  journal   = {J. Funct. Program.},
  volume    = {3},
  number    = {4},
  pages     = {553--561},
  year      = {1993}
}

@inproceedings{Andersson-WADS93,author={Arne Andersson},
title={Balanced search trees made simple},pages={60--71},year=1993,
booktitle={Algorithms and Data Structures (WADS '93)},
series={LNCS},volume={709},publisher={Springer}}

@inproceedings{BlellochFS-SPAA16,
  author    = {Guy E. Blelloch and
               Daniel Ferizovic and
               Yihan Sun},
  title     = {Just Join for Parallel Ordered Sets},
  booktitle = {{SPAA}},
  pages     = {253--264},
  publisher = {{ACM}},
  year      = {2016}
}

@unpublished{BraunRem,author={W. Braun and Martin Rem},
title="A logarithmic implementation of flexible arrays",
note="Memorandum MR83/4. Eindhoven University of Techology",year=1983}

@phdthesis{Crane72,author={Clark A. Crane},
title={Linear Lists and Prorty Queues as Balanced Binary Trees},
school={Computer Science Department, Stanford University},year=1972}

@article{Hinze-bro12,author={Ralf Hinze},
title={Purely Functional 1-2 Brother Trees},
journal={J. Functional Programming},
volume=19,number={6},pages={633--644},year=2009}

@article{HoffmannOD-TOPLAS82,
author={Christoph M. Hoffmann and Michael J. O'Donnell},
title={Programming with Equations},journal={{ACM} Trans. Program. Lang. Syst.},
volume=4,number=1,pages={83--112},year=1982}}

@inproceedings{Hoogerwoord,author={Rob R. Hoogerwoord},
title="A logarithmic implementation of flexible arrays",
editor={R. Bird and C. Morgan and J. Woodcock},
booktitle={Mathematics of Program Construction, Second International Conference},
publisher={Springer},series={LNCS},volume=669,year=1992,
pages={191-207}}

@article{Kahrs-JFP01,author={Stefan Kahrs},title={Red-Black Trees with Types},
journal={J. Functional Programming},volume=11,number=4,pages={425-432},year=2001}

@misc{Kahrs-html,author={Stefan Kahrs},title={Red Black Trees},
note={\url{http://www.cs.ukc.ac.uk/people/staff/smk/redblack/rb.html}}}

@unpublished{Nipkow16,author={Tobias Nipkow},
title={Automatic Functional Correctness Proofs for Functional Search Trees},
year=2016,month=feb,note={\url{http://www.in.tum.de/~nipkow/pubs/trees.html}}}

@inproceedings{NunezPP95,
  author    = {Manuel N{\'{u}}{\~{n}}ez and
               Pedro Palao and
               Ricardo Pena},
  title     = {A Second Year Course on Data Structures Based on Functional Programming},
  booktitle = {Functional Programming Languages in Education},
  pages     = {65--84},
  year      = {1995},
  editor    = {Pieter H. Hartel and
               Marinus J. Plasmeijer},
  series    = {LNCS},
  volume    = {1022},
  publisher = {Springer},
  year      = {1995},
}


@book{Okasaki,author={Chris Okasaki},title="Purely Functional Data Structures",
publisher="Cambridge University Press",year=1998}

@article{OttmannS76,author={Thomas Ottmann and Hans-Werner Six},
title={Eine neue {K}lasse von ausgeglichenen {B}in\"arb\"aumen},
journal={Angewandte Informatik},volume=18,number=9,pages={395--400},year=1976}

@article{OttmannW-CJ80,author={Thomas Ottmann and Derick Wood},
title={1-2 Brother Trees or {AVL} Trees Revisited},journal={Comput. J.},
volume=23,number=3,pages={248--255},year=1980}

@inproceedings{Ragde14,author={Prabhakar Ragde},
title={Simple Balanced Binary Search Trees},pages={78--87},year=2014,
booktitle={Trends in Functional Programming in Education},
series={EPTCS},volume=170,editor={Caldwell and H\"olzenspies and Achten}}

@article{Reade-SCP92,author={Chris Reade},
title={Balanced Trees with Removals: An Exercise in Rewriting and Proof},
journal={Sci. Comput. Program.},volume=18,number=2,pages={181--204},year=1992}

@article{Schoenmakers-IPL93,author="Berry Schoenmakers",
title="A Systematic Analysis of Splaying",journal={Information Processing Letters},volume=45,pages={41-50},year=1993}

@article{SleatorT-JACM85,author={Daniel D. Sleator and Robert E. Tarjan},
title={Self-adjusting Binary Search Trees},journal={J. ACM},
volume=32,number=3,pages={652-686},year=1985}

@misc{Turbak230,author={Franklyn Turbak},
title={{CS230 Handouts --- Spring 2007}},year=2007,
note={\url{http://cs.wellesley.edu/~cs230/spring07/handouts.html}}}