src/HOL/Data_Structures/document/root.bib
author wenzelm
Wed, 04 Oct 2017 12:00:53 +0200
changeset 66787 64b47495676d
parent 62706 49c6a54ceab6
child 67966 f13796496e82
permissions -rw-r--r--
obsolete;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62496
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
     1
@inproceedings{Andersson-WADS93,author={Arne Andersson},
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
     2
title={Balanced search trees made simple},pages={60--71},year=1993,
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
     3
booktitle={Algorithms and Data Structures (WADS '93)},
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
     4
series={LNCS},volume={709},publisher={Springer}}
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
     5
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
     6
@phdthesis{Crane72,author={Clark A. Crane},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
     7
title={Linear Lists and Prorty Queues as Balanced Binary Trees},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
     8
school={Computer Science Department, Stanford University},year=1972}
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
     9
61784
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
    10
@article{Hinze-bro12,author={Ralf Hinze},
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
    11
title={Purely Functional 1-2 Brother Trees},
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
    12
journal={J. Functional Programming},
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
    13
volume=19,number={6},pages={633--644},year=2009}
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
    14
61791
nipkow
parents: 61784
diff changeset
    15
@article{HoffmannOD-TOPLAS82,
nipkow
parents: 61784
diff changeset
    16
author={Christoph M. Hoffmann and Michael J. O'Donnell},
nipkow
parents: 61784
diff changeset
    17
title={Programming with Equations},journal={{ACM} Trans. Program. Lang. Syst.},
nipkow
parents: 61784
diff changeset
    18
volume=4,number=1,pages={83--112},year=1982}}
nipkow
parents: 61784
diff changeset
    19
61224
759b5299a9f2 added red black trees
nipkow
parents: 61203
diff changeset
    20
@article{Kahrs-JFP01,author={Stefan Kahrs},title={Red-Black Trees with Types},
759b5299a9f2 added red black trees
nipkow
parents: 61203
diff changeset
    21
journal={J. Functional Programming},volume=11,number=4,pages={425-432},year=2001}
61203
a8a8eca85801 New subdirectory for functional data structures
nipkow
parents:
diff changeset
    22
61224
759b5299a9f2 added red black trees
nipkow
parents: 61203
diff changeset
    23
@misc{Kahrs-html,author={Stefan Kahrs},title={Red Black Trees},
759b5299a9f2 added red black trees
nipkow
parents: 61203
diff changeset
    24
note={\url{http://www.cs.ukc.ac.uk/people/staff/smk/redblack/rb.html}}}
61203
a8a8eca85801 New subdirectory for functional data structures
nipkow
parents:
diff changeset
    25
62496
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
    26
@unpublished{Nipkow16,author={Tobias Nipkow},
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
    27
title={Automatic Functional Correctness Proofs for Functional Search Trees},
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
    28
year=2016,month=feb,note={\url{http://www.in.tum.de/~nipkow/pubs/trees.html}}}
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
    29
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    30
@inproceedings{NunezPP95,
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    31
  author    = {Manuel N{\'{u}}{\~{n}}ez and
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    32
               Pedro Palao and
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    33
               Ricardo Pena},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    34
  title     = {A Second Year Course on Data Structures Based on Functional Programming},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    35
  booktitle = {Functional Programming Languages in Education},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    36
  pages     = {65--84},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    37
  year      = {1995},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    38
  editor    = {Pieter H. Hartel and
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    39
               Marinus J. Plasmeijer},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    40
  series    = {LNCS},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    41
  volume    = {1022},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    42
  publisher = {Springer},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    43
  year      = {1995},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    44
}
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    45
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    46
61224
759b5299a9f2 added red black trees
nipkow
parents: 61203
diff changeset
    47
@book{Okasaki,author={Chris Okasaki},title="Purely Functional Data Structures",
759b5299a9f2 added red black trees
nipkow
parents: 61203
diff changeset
    48
publisher="Cambridge University Press",year=1998}
61525
87244a9cfe40 added splay trees
nipkow
parents: 61225
diff changeset
    49
61784
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
    50
@article{OttmannS76,author={Thomas Ottmann and Hans-Werner Six},
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
    51
title={Eine neue {K}lasse von ausgeglichenen {B}in\"arb\"aumen},
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
    52
journal={Angewandte Informatik},volume=18,number=9,pages={395--400},year=1976}
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
    53
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
    54
@article{OttmannW-CJ80,author={Thomas Ottmann and Derick Wood},
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
    55
title={1-2 Brother Trees or {AVL} Trees Revisited},journal={Comput. J.},
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
    56
volume=23,number=3,pages={248--255},year=1980}
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
    57
62496
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
    58
@inproceedings{Ragde14,author={Prabhakar Ragde},
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
    59
title={Simple Balanced Binary Search Trees},pages={78--87},year=2014,
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
    60
booktitle={Trends in Functional Programming in Education},
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
    61
series={EPTCS},volume=170,editor={Caldwell and H\"olzenspies and Achten}}
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
    62
61791
nipkow
parents: 61784
diff changeset
    63
@article{Reade-SCP92,author={Chris Reade},
nipkow
parents: 61784
diff changeset
    64
title={Balanced Trees with Removals: An Exercise in Rewriting and Proof},
nipkow
parents: 61784
diff changeset
    65
journal={Sci. Comput. Program.},volume=18,number=2,pages={181--204},year=1992}
nipkow
parents: 61784
diff changeset
    66
61525
87244a9cfe40 added splay trees
nipkow
parents: 61225
diff changeset
    67
@article{Schoenmakers-IPL93,author="Berry Schoenmakers",
87244a9cfe40 added splay trees
nipkow
parents: 61225
diff changeset
    68
title="A Systematic Analysis of Splaying",journal={Information Processing Letters},volume=45,pages={41-50},year=1993}
87244a9cfe40 added splay trees
nipkow
parents: 61225
diff changeset
    69
87244a9cfe40 added splay trees
nipkow
parents: 61225
diff changeset
    70
@article{SleatorT-JACM85,author={Daniel D. Sleator and Robert E. Tarjan},
87244a9cfe40 added splay trees
nipkow
parents: 61225
diff changeset
    71
title={Self-adjusting Binary Search Trees},journal={J. ACM},
87244a9cfe40 added splay trees
nipkow
parents: 61225
diff changeset
    72
volume=32,number=3,pages={652-686},year=1985}
61697
0753dd4c9144 converted to cmp
nipkow
parents: 61525
diff changeset
    73
0753dd4c9144 converted to cmp
nipkow
parents: 61525
diff changeset
    74
@misc{Turbak230,author={Franklyn Turbak},
0753dd4c9144 converted to cmp
nipkow
parents: 61525
diff changeset
    75
title={{CS230 Handouts --- Spring 2007}},year=2007,
0753dd4c9144 converted to cmp
nipkow
parents: 61525
diff changeset
    76
note={\url{http://cs.wellesley.edu/~cs230/spring07/handouts.html}}}