src/HOL/Data_Structures/document/root.bib
author nipkow
Thu, 06 Aug 2020 17:39:57 +0200
changeset 72100 9fa6dde8d959
parent 69133 22fe10b4c0c6
permissions -rw-r--r--
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
67966
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
     1
@techreport{Adams-TR92,author="Stephen Adams",
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
     2
title="Implementing Sets Efficiently in a Functional Language",
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
     3
institution="University of Southampton, Department of Electronics and Computer Science",number="CSTR 92-10",year=1992}
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
     4
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
     5
@article{Adams-JFP93,
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
     6
  author    = {Stephen Adams},
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
     7
  title     = {Efficient Sets - {A} Balancing Act},
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
     8
  journal   = {J. Funct. Program.},
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
     9
  volume    = {3},
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
    10
  number    = {4},
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
    11
  pages     = {553--561},
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
    12
  year      = {1993}
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
    13
}
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
    14
62496
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
    15
@inproceedings{Andersson-WADS93,author={Arne Andersson},
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
    16
title={Balanced search trees made simple},pages={60--71},year=1993,
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
    17
booktitle={Algorithms and Data Structures (WADS '93)},
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
    18
series={LNCS},volume={709},publisher={Springer}}
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
    19
67966
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
    20
@inproceedings{BlellochFS-SPAA16,
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
    21
  author    = {Guy E. Blelloch and
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
    22
               Daniel Ferizovic and
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
    23
               Yihan Sun},
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
    24
  title     = {Just Join for Parallel Ordered Sets},
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
    25
  booktitle = {{SPAA}},
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
    26
  pages     = {253--264},
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
    27
  publisher = {{ACM}},
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
    28
  year      = {2016}
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
    29
}
f13796496e82 Added binary set operations with join-based implementation
nipkow
parents: 62706
diff changeset
    30
69133
22fe10b4c0c6 added Braun_Tree.thy
nipkow
parents: 67966
diff changeset
    31
@unpublished{BraunRem,author={W. Braun and Martin Rem},
22fe10b4c0c6 added Braun_Tree.thy
nipkow
parents: 67966
diff changeset
    32
title="A logarithmic implementation of flexible arrays",
22fe10b4c0c6 added Braun_Tree.thy
nipkow
parents: 67966
diff changeset
    33
note="Memorandum MR83/4. Eindhoven University of Techology",year=1983}
22fe10b4c0c6 added Braun_Tree.thy
nipkow
parents: 67966
diff changeset
    34
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    35
@phdthesis{Crane72,author={Clark A. Crane},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    36
title={Linear Lists and Prorty Queues as Balanced Binary Trees},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    37
school={Computer Science Department, Stanford University},year=1972}
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    38
61784
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
    39
@article{Hinze-bro12,author={Ralf Hinze},
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
    40
title={Purely Functional 1-2 Brother Trees},
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
    41
journal={J. Functional Programming},
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
    42
volume=19,number={6},pages={633--644},year=2009}
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
    43
72100
nipkow
parents: 69133
diff changeset
    44
@article{jfp/Hinze18,
nipkow
parents: 69133
diff changeset
    45
  author    = {Ralf Hinze},
nipkow
parents: 69133
diff changeset
    46
  title     = {On constructing 2-3 trees},
nipkow
parents: 69133
diff changeset
    47
  journal   = {J. Funct. Program.},
nipkow
parents: 69133
diff changeset
    48
  volume    = {28},
nipkow
parents: 69133
diff changeset
    49
  pages     = {e19},
nipkow
parents: 69133
diff changeset
    50
  year      = {2018},
nipkow
parents: 69133
diff changeset
    51
  url       = {https://doi.org/10.1017/S0956796818000187},
nipkow
parents: 69133
diff changeset
    52
}
nipkow
parents: 69133
diff changeset
    53
61791
nipkow
parents: 61784
diff changeset
    54
@article{HoffmannOD-TOPLAS82,
nipkow
parents: 61784
diff changeset
    55
author={Christoph M. Hoffmann and Michael J. O'Donnell},
nipkow
parents: 61784
diff changeset
    56
title={Programming with Equations},journal={{ACM} Trans. Program. Lang. Syst.},
nipkow
parents: 61784
diff changeset
    57
volume=4,number=1,pages={83--112},year=1982}}
nipkow
parents: 61784
diff changeset
    58
69133
22fe10b4c0c6 added Braun_Tree.thy
nipkow
parents: 67966
diff changeset
    59
@inproceedings{Hoogerwoord,author={Rob R. Hoogerwoord},
22fe10b4c0c6 added Braun_Tree.thy
nipkow
parents: 67966
diff changeset
    60
title="A logarithmic implementation of flexible arrays",
22fe10b4c0c6 added Braun_Tree.thy
nipkow
parents: 67966
diff changeset
    61
editor={R. Bird and C. Morgan and J. Woodcock},
22fe10b4c0c6 added Braun_Tree.thy
nipkow
parents: 67966
diff changeset
    62
booktitle={Mathematics of Program Construction, Second International Conference},
22fe10b4c0c6 added Braun_Tree.thy
nipkow
parents: 67966
diff changeset
    63
publisher={Springer},series={LNCS},volume=669,year=1992,
22fe10b4c0c6 added Braun_Tree.thy
nipkow
parents: 67966
diff changeset
    64
pages={191-207}}
22fe10b4c0c6 added Braun_Tree.thy
nipkow
parents: 67966
diff changeset
    65
61224
759b5299a9f2 added red black trees
nipkow
parents: 61203
diff changeset
    66
@article{Kahrs-JFP01,author={Stefan Kahrs},title={Red-Black Trees with Types},
759b5299a9f2 added red black trees
nipkow
parents: 61203
diff changeset
    67
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
    68
61224
759b5299a9f2 added red black trees
nipkow
parents: 61203
diff changeset
    69
@misc{Kahrs-html,author={Stefan Kahrs},title={Red Black Trees},
759b5299a9f2 added red black trees
nipkow
parents: 61203
diff changeset
    70
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
    71
62496
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
    72
@unpublished{Nipkow16,author={Tobias Nipkow},
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
    73
title={Automatic Functional Correctness Proofs for Functional Search Trees},
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
    74
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
    75
62706
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    76
@inproceedings{NunezPP95,
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    77
  author    = {Manuel N{\'{u}}{\~{n}}ez and
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    78
               Pedro Palao and
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    79
               Ricardo Pena},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    80
  title     = {A Second Year Course on Data Structures Based on Functional Programming},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    81
  booktitle = {Functional Programming Languages in Education},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    82
  pages     = {65--84},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    83
  year      = {1995},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    84
  editor    = {Pieter H. Hartel and
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    85
               Marinus J. Plasmeijer},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    86
  series    = {LNCS},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    87
  volume    = {1022},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    88
  publisher = {Springer},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    89
  year      = {1995},
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    90
}
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    91
49c6a54ceab6 added Leftist_Heap
nipkow
parents: 62496
diff changeset
    92
61224
759b5299a9f2 added red black trees
nipkow
parents: 61203
diff changeset
    93
@book{Okasaki,author={Chris Okasaki},title="Purely Functional Data Structures",
759b5299a9f2 added red black trees
nipkow
parents: 61203
diff changeset
    94
publisher="Cambridge University Press",year=1998}
61525
87244a9cfe40 added splay trees
nipkow
parents: 61225
diff changeset
    95
61784
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
    96
@article{OttmannS76,author={Thomas Ottmann and Hans-Werner Six},
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
    97
title={Eine neue {K}lasse von ausgeglichenen {B}in\"arb\"aumen},
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
    98
journal={Angewandte Informatik},volume=18,number=9,pages={395--400},year=1976}
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
    99
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
   100
@article{OttmannW-CJ80,author={Thomas Ottmann and Derick Wood},
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
   101
title={1-2 Brother Trees or {AVL} Trees Revisited},journal={Comput. J.},
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
   102
volume=23,number=3,pages={248--255},year=1980}
21b34a2269e5 added 1-2 brother trees
nipkow
parents: 61697
diff changeset
   103
62496
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
   104
@inproceedings{Ragde14,author={Prabhakar Ragde},
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
   105
title={Simple Balanced Binary Search Trees},pages={78--87},year=2014,
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
   106
booktitle={Trends in Functional Programming in Education},
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
   107
series={EPTCS},volume=170,editor={Caldwell and H\"olzenspies and Achten}}
f187aaf602c4 added invariant proofs to AA trees
nipkow
parents: 61791
diff changeset
   108
61791
nipkow
parents: 61784
diff changeset
   109
@article{Reade-SCP92,author={Chris Reade},
nipkow
parents: 61784
diff changeset
   110
title={Balanced Trees with Removals: An Exercise in Rewriting and Proof},
nipkow
parents: 61784
diff changeset
   111
journal={Sci. Comput. Program.},volume=18,number=2,pages={181--204},year=1992}
nipkow
parents: 61784
diff changeset
   112
61525
87244a9cfe40 added splay trees
nipkow
parents: 61225
diff changeset
   113
@article{Schoenmakers-IPL93,author="Berry Schoenmakers",
87244a9cfe40 added splay trees
nipkow
parents: 61225
diff changeset
   114
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
   115
87244a9cfe40 added splay trees
nipkow
parents: 61225
diff changeset
   116
@article{SleatorT-JACM85,author={Daniel D. Sleator and Robert E. Tarjan},
87244a9cfe40 added splay trees
nipkow
parents: 61225
diff changeset
   117
title={Self-adjusting Binary Search Trees},journal={J. ACM},
87244a9cfe40 added splay trees
nipkow
parents: 61225
diff changeset
   118
volume=32,number=3,pages={652-686},year=1985}
61697
0753dd4c9144 converted to cmp
nipkow
parents: 61525
diff changeset
   119
0753dd4c9144 converted to cmp
nipkow
parents: 61525
diff changeset
   120
@misc{Turbak230,author={Franklyn Turbak},
0753dd4c9144 converted to cmp
nipkow
parents: 61525
diff changeset
   121
title={{CS230 Handouts --- Spring 2007}},year=2007,
0753dd4c9144 converted to cmp
nipkow
parents: 61525
diff changeset
   122
note={\url{http://cs.wellesley.edu/~cs230/spring07/handouts.html}}}