--- a/thys/Journal/document/root.bib	Thu Jul 06 16:05:33 2017 +0100
+++ b/thys/Journal/document/root.bib	Tue Jul 18 18:39:20 2017 +0100
@@ -1,5 +1,25 @@
+
+
+
+@Misc{POSIX,
+  title =     {{T}he {O}pen {G}roup {B}ase {S}pecification {I}ssue 6 {IEEE} {S}td 1003.1 2004 {E}dition},
+  year =      {2004},
+  note =    {\url{http://pubs.opengroup.org/onlinepubs/009695399/basedefs/xbd_chap09.html}}
+}
+
+
+@InProceedings{AusafDyckhoffUrban2016,
+  author =   {F.~Ausaf and R.~Dyckhoff and C.~Urban},
+  title = 	 {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions ({P}roof {P}earl)},
+  year = 	 {2016},
+  booktitle = {Proc.~of the 7th International Conference on Interactive Theorem Proving (ITP)},
+  volume = 	 {9807},
+  series = 	 {LNCS},
+  pages =        {69--86}
+}
+
 @article{aduAFP16,
-  author =   {Fahad Ausaf and Roy Dyckhoff and Christian Urban},
+  author =   {F.~Ausaf and R.~Dyckhoff and C.~Urban},
   title =    {{POSIX} {L}exing with {D}erivatives of {R}egular {E}xpressions},
   journal =  {Archive of Formal Proofs},
   year =     2016,
@@ -255,13 +275,6 @@
   series =       {LNCS}
 }
 
-@book{Michaelson,
-  title={An introduction to functional programming through lambda calculus},
-  author={Michaelson, Greg},
-  year={2011},
-  publisher={Courier Corporation}
-}
-
 @article{Owens2008,
   author    = {S.~Owens and K.~Slind},
   title     = {{A}dapting {F}unctional {P}rograms to {H}igher {O}rder {L}ogic},
@@ -273,92 +286,8 @@
 }
 
 
-@book{Velleman,
-  title={How to prove it: a structured approach},
-  author={Velleman, Daniel J},
-  year={2006},
-  publisher={Cambridge University Press}
-}
-
-@book{Jones,
-  title={Implementing functional languages:[a tutorial]},
-  author={Jones, Simon L Peyton and Lester, David R},
-  volume={124},
-  year={1992},
-  publisher={Prentice Hall Reading}
-}
-
-@article{Cardelli,
-  title={Type systems},
-  author={Cardelli, Luca},
-  journal={ACM Computing Surveys},
-  volume={28},
-  number={1},
-  pages={263--264},
-  year={1996}
-}
-
-@article{Morrisett,
-  author    = {J. Gregory Morrisett and
-               Karl Crary and
-               Neal Glew and
-               David Walker},
-  title     = {Stack-based typed assembly language},
-  journal   = {J. Funct. Program.},
-  volume    = {13},
-  number    = {5},
-  pages     = {957--959},
-  year      = {2003},
-  url       = {http://dx.doi.org/10.1017/S0956796802004446},
-  doi       = {10.1017/S0956796802004446},
-  timestamp = {Fri, 19 Mar 2004 13:48:27 +0100},
-  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jfp/MorrisettCGW03},
-  bibsource = {dblp computer science bibliography, http://dblp.org}
-}
-
-@book{Nipkow,
-  title={Concrete Semantics: With Isabelle/HOL},
-  author={Nipkow, Tobias and Klein, Gerwin},
-  year={2014},
-  publisher={Springer}
-}
-
-@article{Dube,
-  author    = {Danny Dub{\'{e}} and
-               Marc Feeley},
-  title     = {Efficiently building a parse tree from a regular expression},
-  journal   = {Acta Inf.},
-  volume    = {37},
-  number    = {2},
-  pages     = {121--144},
-  year      = {2000},
-  url       = {http://link.springer.de/link/service/journals/00236/bibs/0037002/00370121.htm},
-  timestamp = {Tue, 25 Nov 2003 14:51:21 +0100},
-  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/acta/DubeF00},
-  bibsource = {dblp computer science bibliography, http://dblp.org}
-}
-
-@article{Morrisett2,
-  author    = {J. Gregory Morrisett and
-               David Walker and
-               Karl Crary and
-               Neal Glew},
-  title     = {From system {F} to typed assembly language},
-  journal   = {{ACM} Trans. Program. Lang. Syst.},
-  volume    = {21},
-  number    = {3},
-  pages     = {527--568},
-  year      = {1999},
-  url       = {http://doi.acm.org/10.1145/319301.319345},
-  doi       = {10.1145/319301.319345},
-  timestamp = {Wed, 26 Nov 2003 14:26:46 +0100},
-  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/toplas/MorrisettWCG99},
-  bibsource = {dblp computer science bibliography, http://dblp.org}
-}
-
 @article{Owens2,
-  author    = {Scott Owens and
-               Konrad Slind},
+  author    = {S.~Owens and K.~Slind},
   title     = {Adapting functional programs to higher order logic},
   journal   = {Higher-Order and Symbolic Computation},
   volume    = {21},
@@ -379,3 +308,15 @@
 
 
 
+@InProceedings{OkuiSuzuki2013,
+  author =       {S.~Okui and T.~Suzuki},
+  title =        {{D}isambiguation in {R}egular {E}xpression {M}atching via
+                  {P}osition {A}utomata with {A}ugmented {T}ransitions},
+  booktitle = {Proc.~of the 15th International Conference on Implementation
+                  and Application of Automata (CIAA)},
+  year =      {2010},
+  volume =    {6482},
+  series =    {LNCS},
+  pages =     {231--240}
+}
+