--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/Response/apa.bst Wed Dec 12 11:45:04 2012 +0000
@@ -0,0 +1,1130 @@
+%%% ====================================================================
+%%% @BibTeX-style-file{
+%%% author = "Alan Rogers",
+%%% version = "1.1",
+%%% date = "June 27, 1992",
+%%% filename = "apa.bst",
+%%% address = "Dept of Anthropology, University of Utah,
+%%% Salt Lake City, UT 84112",
+%%% checksum = "21129 1130 3156 23582",
+%%% email = "rogers@anthro.utah.edu",
+%%% supported = "no",
+%%% docstring = "Adapted from apalike.bst.
+%%% Usage: \documentstyle[astron]{...}
+%%% ...
+%%% \bibliographystyle{apa}
+%%% ...
+%%% This file incorporates features of Sake J.
+%%% Hogeveen's `astron.bst' into`apalike.bst'.
+%%% The \documentstyle command above invokes
+%%% Hogeveen's `astron.sty', which must be in
+%%% TeX's search path.
+%%%
+%%% The modifications implement `\cite*{}', which
+%%% generates references in short form. For
+%%% example, `Rogers \cite*{...}' would produce
+%%% `Rogers (1992)'."
+%%% }
+%%% ====================================================================
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% BibTeX `apalike' bibliography style (24-Jan-88 version)
+% Adapted from the `alpha' style, version 0.99a; for BibTeX version 0.99a.
+% Copyright (C) 1988, all rights reserved.
+% Copying of this file is allowed, provided that if you make any changes at all
+% you name it something other than `apalike.bst'.
+% This restriction helps ensure that all copies are identical.
+% Differences between this style and `alpha' are generally heralded by a `%'.
+% The file btxbst.doc has the documentation for alpha.bst.
+%
+% This style should be used with the `apalike' LaTeX style (apalike.sty).
+% \cite's come out like "(Jones, 1986)" in the text but there are no labels
+% in the bibliography, and something like "(1986)" comes out immediately
+% after the author. Author (and editor) names appear as last name, comma,
+% initials. A `year' field is required for every entry, and so is either
+% an author (or in some cases, an editor) field or a key field.
+%
+% Editorial note:
+% Many journals require a style like `apalike', but I strongly, strongly,
+% strongly recommend that you not use it if you have a choice---use something
+% like `plain' instead. Mary-Claire van Leunen (A Handbook for Scholars,
+% Knopf, 1979) argues convincingly that a style like `plain' encourages better
+% writing than one like `apalike'. Furthermore the strongest arguments for
+% using an author-date style like `apalike'---that it's "the most practical"
+% (The Chicago Manual of Style, University of Chicago Press, thirteenth
+% edition, 1982, pages 400--401)---fall flat on their face with the new
+% computer-typesetting technology. For instance page 401 anachronistically
+% states "The chief disadvantage of [a style like `plain'] is that additions
+% or deletions cannot be made after the manuscript is typed without changing
+% numbers in both text references and list." LaTeX sidesteps the disadvantage.
+%
+% History:
+% 15-sep-86 (SK,OP) Original version, by Susan King and Oren Patashnik.
+% 10-nov-86 (OP) Truncated the sort.key$ string to the correct length
+% in bib.sort.order to eliminate error message.
+% 24-jan-88 (OP) Updated for BibTeX version 0.99a, from alpha.bst 0.99a;
+% apalike now sorts by author, then year, then title;
+% THIS `apalike' VERSION DOES NOT WORK WITH BIBTEX 0.98i.
+
+ENTRY
+ { address
+ author
+ booktitle
+ chapter
+ edition
+ editor
+ howpublished
+ institution
+ journal
+ key
+% month not used in apalike
+ note
+ number
+ organization
+ pages
+ publisher
+ school
+ series
+ title
+ type
+ volume
+ year
+ }
+ {}
+ { label extra.label sort.label }
+
+INTEGERS { output.state before.all mid.sentence after.sentence after.block }
+
+FUNCTION {init.state.consts}
+{ #0 'before.all :=
+ #1 'mid.sentence :=
+ #2 'after.sentence :=
+ #3 'after.block :=
+}
+
+STRINGS { s t }
+
+FUNCTION {output.nonnull}
+{ 's :=
+ output.state mid.sentence =
+ { ", " * write$ }
+ { output.state after.block =
+ { add.period$ write$
+ newline$
+ "\newblock " write$
+ }
+ { output.state before.all =
+ 'write$
+ { add.period$ " " * write$ }
+ if$
+ }
+ if$
+ mid.sentence 'output.state :=
+ }
+ if$
+ s
+}
+
+FUNCTION {output}
+{ duplicate$ empty$
+ 'pop$
+ 'output.nonnull
+ if$
+}
+
+FUNCTION {output.check}
+{ 't :=
+ duplicate$ empty$
+ { pop$ "empty " t * " in " * cite$ * warning$ }
+ 'output.nonnull
+ if$
+}
+
+% apalike needs this function because
+% the year has special punctuation;
+% apalike ignores the month
+FUNCTION {output.year.check}
+{ year empty$
+ { "empty year in " cite$ * warning$ }
+ { write$
+ " [" year * extra.label * "]" *
+ mid.sentence 'output.state :=
+ }
+ if$
+}
+
+FUNCTION {output.bibitem}
+{ newline$
+ "\bibitem[" write$
+ label write$
+ "]{" write$
+ cite$ write$
+ "}" write$
+ newline$
+ ""
+ before.all 'output.state :=
+}
+
+FUNCTION {fin.entry}
+{ add.period$
+ write$
+ newline$
+}
+
+FUNCTION {new.block}
+{ output.state before.all =
+ 'skip$
+ { after.block 'output.state := }
+ if$
+}
+
+FUNCTION {new.sentence}
+{ output.state after.block =
+ 'skip$
+ { output.state before.all =
+ 'skip$
+ { after.sentence 'output.state := }
+ if$
+ }
+ if$
+}
+
+FUNCTION {not}
+{ { #0 }
+ { #1 }
+ if$
+}
+
+FUNCTION {and}
+{ 'skip$
+ { pop$ #0 }
+ if$
+}
+
+FUNCTION {or}
+{ { pop$ #1 }
+ 'skip$
+ if$
+}
+
+FUNCTION {new.block.checkb}
+{ empty$
+ swap$ empty$
+ and
+ 'skip$
+ 'new.block
+ if$
+}
+
+FUNCTION {field.or.null}
+{ duplicate$ empty$
+ { pop$ "" }
+ 'skip$
+ if$
+}
+
+FUNCTION {emphasize}
+{ duplicate$ empty$
+ { pop$ "" }
+ { "{\em " swap$ * "}" * }
+ if$
+}
+
+INTEGERS { nameptr namesleft numnames }
+
+FUNCTION {format.names}
+{ 's :=
+ #1 'nameptr :=
+ s num.names$ 'numnames :=
+ numnames 'namesleft :=
+ { namesleft #0 > }
+ { s nameptr "{vv~}{ll}{, jj}{, f.}" format.name$ 't := % last name first
+ nameptr #1 >
+ { namesleft #1 >
+ { ", " * t * }
+ { numnames #2 >
+ { "," * }
+ 'skip$
+ if$
+ t "others" =
+ { " et~al." * }
+ { " and " * t * }
+ if$
+ }
+ if$
+ }
+ 't
+ if$
+ nameptr #1 + 'nameptr :=
+ namesleft #1 - 'namesleft :=
+ }
+ while$
+}
+
+FUNCTION {format.authors}
+{ author empty$
+ { "" }
+ { author format.names }
+ if$
+}
+
+FUNCTION {format.key} % this function is just for apalike
+{ empty$
+ { key field.or.null }
+ { "" }
+ if$
+}
+
+FUNCTION {format.editors}
+{ editor empty$
+ { "" }
+ { editor format.names
+ editor num.names$ #1 >
+ { ", editors" * }
+ { ", editor" * }
+ if$
+ }
+ if$
+}
+
+FUNCTION {format.title}
+{ title empty$
+ { "" }
+ { title "t" change.case$ }
+ if$
+}
+
+FUNCTION {n.dashify}
+{ 't :=
+ ""
+ { t empty$ not }
+ { t #1 #1 substring$ "-" =
+ { t #1 #2 substring$ "--" = not
+ { "--" *
+ t #2 global.max$ substring$ 't :=
+ }
+ { { t #1 #1 substring$ "-" = }
+ { "-" *
+ t #2 global.max$ substring$ 't :=
+ }
+ while$
+ }
+ if$
+ }
+ { t #1 #1 substring$ *
+ t #2 global.max$ substring$ 't :=
+ }
+ if$
+ }
+ while$
+}
+
+FUNCTION {format.btitle}
+{ title emphasize
+}
+
+FUNCTION {tie.or.space.connect}
+{ duplicate$ text.length$ #3 <
+ { "~" }
+ { " " }
+ if$
+ swap$ * *
+}
+
+FUNCTION {either.or.check}
+{ empty$
+ 'pop$
+ { "can't use both " swap$ * " fields in " * cite$ * warning$ }
+ if$
+}
+
+FUNCTION {format.bvolume}
+{ volume empty$
+ { "" }
+ { "volume" volume tie.or.space.connect
+ series empty$
+ 'skip$
+ { " of " * series emphasize * }
+ if$
+ "volume and number" number either.or.check
+ }
+ if$
+}
+
+FUNCTION {format.number.series}
+{ volume empty$
+ { number empty$
+ { series field.or.null }
+ { output.state mid.sentence =
+ { "number" }
+ { "Number" }
+ if$
+ number tie.or.space.connect
+ series empty$
+ { "there's a number but no series in " cite$ * warning$ }
+ { " in " * series * }
+ if$
+ }
+ if$
+ }
+ { "" }
+ if$
+}
+
+FUNCTION {format.edition}
+{ edition empty$
+ { "" }
+ { output.state mid.sentence =
+ { edition "l" change.case$ " edition" * }
+ { edition "t" change.case$ " edition" * }
+ if$
+ }
+ if$
+}
+
+INTEGERS { multiresult }
+
+FUNCTION {multi.page.check}
+{ 't :=
+ #0 'multiresult :=
+ { multiresult not
+ t empty$ not
+ and
+ }
+ { t #1 #1 substring$
+ duplicate$ "-" =
+ swap$ duplicate$ "," =
+ swap$ "+" =
+ or or
+ { #1 'multiresult := }
+ { t #2 global.max$ substring$ 't := }
+ if$
+ }
+ while$
+ multiresult
+}
+
+FUNCTION {format.pages}
+{ pages empty$
+ { "" }
+ { pages multi.page.check
+ { "pages" pages n.dashify tie.or.space.connect }
+ { "page" pages tie.or.space.connect }
+ if$
+ }
+ if$
+}
+
+FUNCTION {format.vol.num.pages}
+{ volume field.or.null
+ number empty$
+ 'skip$
+ { "(" number * ")" * *
+ volume empty$
+ { "there's a number but no volume in " cite$ * warning$ }
+ 'skip$
+ if$
+ }
+ if$
+ pages empty$
+ 'skip$
+ { duplicate$ empty$
+ { pop$ format.pages }
+ { ":" * pages n.dashify * }
+ if$
+ }
+ if$
+}
+
+FUNCTION {format.chapter.pages}
+{ chapter empty$
+ 'format.pages
+ { type empty$
+ { "chapter" }
+ { type "l" change.case$ }
+ if$
+ chapter tie.or.space.connect
+ pages empty$
+ 'skip$
+ { ", " * format.pages * }
+ if$
+ }
+ if$
+}
+
+FUNCTION {format.in.ed.booktitle}
+{ booktitle empty$
+ { "" }
+ { editor empty$
+ { "In " booktitle emphasize * }
+ { "In " format.editors * ", " * booktitle emphasize * }
+ if$
+ }
+ if$
+}
+
+FUNCTION {format.thesis.type}
+{ type empty$
+ 'skip$
+ { pop$
+ type "t" change.case$
+ }
+ if$
+}
+
+FUNCTION {format.tr.number}
+{ type empty$
+ { "Technical Report" }
+ 'type
+ if$
+ number empty$
+ { "t" change.case$ }
+ { number tie.or.space.connect }
+ if$
+}
+
+FUNCTION {format.article.crossref}
+{ "In" % this is for apalike
+ " \cite{" * crossref * "}" *
+}
+
+FUNCTION {format.book.crossref}
+{ volume empty$
+ { "empty volume in " cite$ * "'s crossref of " * crossref * warning$
+ "In "
+ }
+ { "Volume" volume tie.or.space.connect
+ " of " *
+ }
+ if$
+ "\cite{" * crossref * "}" * % this is for apalike
+}
+
+FUNCTION {format.incoll.inproc.crossref}
+{ "In" % this is for apalike
+ " \cite{" * crossref * "}" *
+}
+
+FUNCTION {article}
+{ output.bibitem
+ format.authors "author" output.check
+ author format.key output % special for
+ output.year.check % apalike
+ new.block
+ format.title "title" output.check
+ new.block
+ crossref missing$
+ { journal emphasize "journal" output.check
+ format.vol.num.pages output
+ }
+ { format.article.crossref output.nonnull
+ format.pages output
+ }
+ if$
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {book}
+{ output.bibitem
+ author empty$
+ { format.editors "author and editor" output.check
+ editor format.key output
+ }
+ { format.authors output.nonnull
+ crossref missing$
+ { "author and editor" editor either.or.check }
+ 'skip$
+ if$
+ }
+ if$
+ output.year.check % special for apalike
+ new.block
+ format.btitle "title" output.check
+ crossref missing$
+ { format.bvolume output
+ new.block
+ format.number.series output
+ new.sentence
+ publisher "publisher" output.check
+ address output
+ }
+ { new.block
+ format.book.crossref output.nonnull
+ }
+ if$
+ format.edition output
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {booklet}
+{ output.bibitem
+ format.authors output
+ author format.key output % special for
+ output.year.check % apalike
+ new.block
+ format.title "title" output.check
+ new.block
+ howpublished output
+ address output
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {inbook}
+{ output.bibitem
+ author empty$
+ { format.editors "author and editor" output.check
+ editor format.key output
+ }
+ { format.authors output.nonnull
+ crossref missing$
+ { "author and editor" editor either.or.check }
+ 'skip$
+ if$
+ }
+ if$
+ output.year.check % special for apalike
+ new.block
+ format.btitle "title" output.check
+ crossref missing$
+ { format.bvolume output
+ format.chapter.pages "chapter and pages" output.check
+ new.block
+ format.number.series output
+ new.sentence
+ publisher "publisher" output.check
+ address output
+ }
+ { format.chapter.pages "chapter and pages" output.check
+ new.block
+ format.book.crossref output.nonnull
+ }
+ if$
+ format.edition output
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {incollection}
+{ output.bibitem
+ format.authors "author" output.check
+ author format.key output % special for
+ output.year.check % apalike
+ new.block
+ format.title "title" output.check
+ new.block
+ crossref missing$
+ { format.in.ed.booktitle "booktitle" output.check
+ format.bvolume output
+ format.number.series output
+ format.chapter.pages output
+ new.sentence
+ publisher "publisher" output.check
+ address output
+ format.edition output
+ }
+ { format.incoll.inproc.crossref output.nonnull
+ format.chapter.pages output
+ }
+ if$
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {inproceedings}
+{ output.bibitem
+ format.authors "author" output.check
+ author format.key output % special for
+ output.year.check % apalike
+ new.block
+ format.title "title" output.check
+ new.block
+ crossref missing$
+ { format.in.ed.booktitle "booktitle" output.check
+ format.bvolume output
+ format.number.series output
+ format.pages output
+ address output % for apalike
+ new.sentence % there's no year
+ organization output % here so things
+ publisher output % are simpler
+ }
+ { format.incoll.inproc.crossref output.nonnull
+ format.pages output
+ }
+ if$
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {conference} { inproceedings }
+
+FUNCTION {manual}
+{ output.bibitem
+ format.authors output
+ author format.key output % special for
+ output.year.check % apalike
+ new.block
+ format.btitle "title" output.check
+ organization address new.block.checkb
+ organization output
+ address output
+ format.edition output
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {mastersthesis}
+{ output.bibitem
+ format.authors "author" output.check
+ author format.key output % special for
+ output.year.check % apalike
+ new.block
+ format.title "title" output.check
+ new.block
+ "Master's thesis" format.thesis.type output.nonnull
+ school "school" output.check
+ address output
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {misc}
+{ output.bibitem
+ format.authors output
+ author format.key output % special for
+ output.year.check % apalike
+ new.block
+ format.title output
+ new.block
+ howpublished output
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {phdthesis}
+{ output.bibitem
+ format.authors "author" output.check
+ author format.key output % special for
+ output.year.check % apalike
+ new.block
+ format.btitle "title" output.check
+ new.block
+ "PhD thesis" format.thesis.type output.nonnull
+ school "school" output.check
+ address output
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {proceedings}
+{ output.bibitem
+ format.editors output
+ editor format.key output % special for
+ output.year.check % apalike
+ new.block
+ format.btitle "title" output.check
+ format.bvolume output
+ format.number.series output
+ address output % for apalike
+ new.sentence % we always output
+ organization output % a nonempty organization
+ publisher output % here
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {techreport}
+{ output.bibitem
+ format.authors "author" output.check
+ author format.key output % special for
+ output.year.check % apalike
+ new.block
+ format.title "title" output.check
+ new.block
+ format.tr.number output.nonnull
+ institution "institution" output.check
+ address output
+ new.block
+ note output
+ fin.entry
+}
+
+FUNCTION {unpublished}
+{ output.bibitem
+ format.authors "author" output.check
+ author format.key output % special for
+ output.year.check % apalike
+ new.block
+ format.title "title" output.check
+ new.block
+ note "note" output.check
+ fin.entry
+}
+
+FUNCTION {default.type} { misc }
+
+MACRO {jan} {"January"}
+
+MACRO {feb} {"February"}
+
+MACRO {mar} {"March"}
+
+MACRO {apr} {"April"}
+
+MACRO {may} {"May"}
+
+MACRO {jun} {"June"}
+
+MACRO {jul} {"July"}
+
+MACRO {aug} {"August"}
+
+MACRO {sep} {"September"}
+
+MACRO {oct} {"October"}
+
+MACRO {nov} {"November"}
+
+MACRO {dec} {"December"}
+
+MACRO {acmcs} {"ACM Computing Surveys"}
+
+MACRO {acta} {"Acta Informatica"}
+
+MACRO {cacm} {"Communications of the ACM"}
+
+MACRO {ibmjrd} {"IBM Journal of Research and Development"}
+
+MACRO {ibmsj} {"IBM Systems Journal"}
+
+MACRO {ieeese} {"IEEE Transactions on Software Engineering"}
+
+MACRO {ieeetc} {"IEEE Transactions on Computers"}
+
+MACRO {ieeetcad}
+ {"IEEE Transactions on Computer-Aided Design of Integrated Circuits"}
+
+MACRO {ipl} {"Information Processing Letters"}
+
+MACRO {jacm} {"Journal of the ACM"}
+
+MACRO {jcss} {"Journal of Computer and System Sciences"}
+
+MACRO {scp} {"Science of Computer Programming"}
+
+MACRO {sicomp} {"SIAM Journal on Computing"}
+
+MACRO {tocs} {"ACM Transactions on Computer Systems"}
+
+MACRO {tods} {"ACM Transactions on Database Systems"}
+
+MACRO {tog} {"ACM Transactions on Graphics"}
+
+MACRO {toms} {"ACM Transactions on Mathematical Software"}
+
+MACRO {toois} {"ACM Transactions on Office Information Systems"}
+
+MACRO {toplas} {"ACM Transactions on Programming Languages and Systems"}
+
+MACRO {tcs} {"Theoretical Computer Science"}
+
+READ
+
+FUNCTION {sortify}
+{ purify$
+ "l" change.case$
+}
+
+INTEGERS { len }
+
+FUNCTION {chop.word}
+{ 's :=
+ 'len :=
+ s #1 len substring$ =
+ { s len #1 + global.max$ substring$ }
+ 's
+ if$
+}
+
+% There are three apalike cases: one person (Jones),
+% two (Jones and de~Bruijn), and more (Jones et~al.).
+% This function is much like format.crossref.editors.
+%
+FUNCTION {format.lab.names}
+{ 's :=
+ s #1 "{vv~}{ll}" format.name$
+ s num.names$ duplicate$
+ #2 >
+ { pop$ " et~al." * }
+ { #2 <
+ 'skip$
+ { s #2 "{ff }{vv }{ll}{ jj}" format.name$ "others" =
+ { " et~al." * }
+ { " and " * s #2 "{vv~}{ll}" format.name$ * }
+ if$
+ }
+ if$
+ }
+ if$
+}
+
+FUNCTION {author.key.label}
+{ author empty$
+ { key empty$
+ { cite$ #1 #3 substring$ }
+ 'key % apalike uses the whole key
+ if$
+ }
+ { author format.lab.names }
+ if$
+}
+
+FUNCTION {author.editor.key.label}
+{ author empty$
+ { editor empty$
+ { key empty$
+ { cite$ #1 #3 substring$ }
+ 'key % apalike uses the whole key
+ if$
+ }
+ { editor format.lab.names }
+ if$
+ }
+ { author format.lab.names }
+ if$
+}
+
+FUNCTION {editor.key.label}
+{ editor empty$
+ { key empty$
+ { cite$ #1 #3 substring$ }
+ 'key % apalike uses the whole key, no organization
+ if$
+ }
+ { editor format.lab.names }
+ if$
+}
+
+FUNCTION {calc.label} % this function came from ASTRON.BST (ARR)
+{ type$ "book" =
+ type$ "inbook" =
+ or
+ 'author.editor.key.label
+ { type$ "proceedings" =
+ 'editor.key.label % apalike ignores organization
+ 'author.key.label % for labeling and sorting
+ if$
+ }
+ if$
+ "\protect\astroncite{" swap$ * "}{" % these three lines are
+ * % for apalike, which
+ year field.or.null purify$ #-1 #4 substring$ % uses all four digits
+ * % the mathing closing "}" comes in at the reverse.pass
+ 'label :=
+}
+
+FUNCTION {sort.format.names}
+{ 's :=
+ #1 'nameptr :=
+ ""
+ s num.names$ 'numnames :=
+ numnames 'namesleft :=
+ { namesleft #0 > }
+ { nameptr #1 >
+ { " " * }
+ 'skip$
+ if$ % apalike uses initials
+ s nameptr "{vv{ } }{ll{ }}{ f{ }}{ jj{ }}" format.name$ 't := % <= here
+ nameptr numnames = t "others" = and
+ { "et al" * }
+ { t sortify * }
+ if$
+ nameptr #1 + 'nameptr :=
+ namesleft #1 - 'namesleft :=
+ }
+ while$
+}
+
+FUNCTION {sort.format.title}
+{ 't :=
+ "A " #2
+ "An " #3
+ "The " #4 t chop.word
+ chop.word
+ chop.word
+ sortify
+ #1 global.max$ substring$
+}
+
+FUNCTION {author.sort}
+{ author empty$
+ { key empty$
+ { "to sort, need author or key in " cite$ * warning$
+ ""
+ }
+ { key sortify }
+ if$
+ }
+ { author sort.format.names }
+ if$
+}
+
+FUNCTION {author.editor.sort}
+{ author empty$
+ { editor empty$
+ { key empty$
+ { "to sort, need author, editor, or key in " cite$ * warning$
+ ""
+ }
+ { key sortify }
+ if$
+ }
+ { editor sort.format.names }
+ if$
+ }
+ { author sort.format.names }
+ if$
+}
+
+FUNCTION {editor.sort}
+{ editor empty$
+ { key empty$
+ { "to sort, need editor or key in " cite$ * warning$
+ ""
+ }
+ { key sortify }
+ if$
+ }
+ { editor sort.format.names }
+ if$
+}
+
+% apalike uses two sorting passes; the first one sets the
+% labels so that the `a's, `b's, etc. can be computed;
+% the second pass puts the references in "correct" order.
+% The presort function is for the first pass. It computes
+% label, sort.label, and title, and then concatenates.
+FUNCTION {presort}
+{ calc.label
+ label sortify
+ " "
+ *
+ type$ "book" =
+ type$ "inbook" =
+ or
+ 'author.editor.sort
+ { type$ "proceedings" =
+ 'editor.sort
+ 'author.sort
+ if$
+ }
+ if$
+ #1 entry.max$ substring$ % for
+ 'sort.label := % apalike
+ sort.label % style
+ *
+ " "
+ *
+ title field.or.null
+ sort.format.title
+ *
+ #1 entry.max$ substring$
+ 'sort.key$ :=
+}
+
+ITERATE {presort}
+
+SORT % by label, sort.label, title---for final label calculation
+
+STRINGS { last.label next.extra } % apalike labels are only for the text;
+
+INTEGERS { last.extra.num } % there are none in the bibliography
+
+FUNCTION {initialize.extra.label.stuff} % and hence there is no `longest.label'
+{ #0 int.to.chr$ 'last.label :=
+ "" 'next.extra :=
+ #0 'last.extra.num :=
+}
+
+FUNCTION {forward.pass}
+{ last.label label =
+ { last.extra.num #1 + 'last.extra.num :=
+ last.extra.num int.to.chr$ 'extra.label :=
+ }
+ { "a" chr.to.int$ 'last.extra.num :=
+ "" 'extra.label :=
+ label 'last.label :=
+ }
+ if$
+}
+
+FUNCTION {reverse.pass} % this function came from ASTRON.BST (ARR)
+{ next.extra "b" =
+ { "a" 'extra.label := }
+ 'skip$
+ if$
+ label extra.label * "}" * 'label :=
+ extra.label 'next.extra :=
+}
+
+EXECUTE {initialize.extra.label.stuff}
+
+ITERATE {forward.pass}
+
+REVERSE {reverse.pass}
+
+% Now that the label is right we sort for real,
+% on sort.label then year then title. This is
+% for the second sorting pass.
+FUNCTION {bib.sort.order}
+{ sort.label
+ " "
+ *
+ year field.or.null sortify
+ *
+ " "
+ *
+ title field.or.null
+ sort.format.title
+ *
+ #1 entry.max$ substring$
+ 'sort.key$ :=
+}
+
+ITERATE {bib.sort.order}
+
+SORT % by sort.label, year, title---giving final bibliography order
+
+FUNCTION {begin.bib}
+{ preamble$ empty$ % no \etalchar in apalike
+ 'skip$
+ { preamble$ write$ newline$ }
+ if$
+ "\begin{thebibliography}{}" write$ newline$ % no labels in apalike
+}
+
+EXECUTE {begin.bib}
+
+EXECUTE {init.state.consts}
+
+ITERATE {call.type$}
+
+FUNCTION {end.bib}
+{ newline$
+ "\end{thebibliography}" write$ newline$
+}
+
+EXECUTE {end.bib}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/Response/response.tex Wed Dec 12 11:45:04 2012 +0000
@@ -0,0 +1,255 @@
+\documentclass[12pt]{article}
+\usepackage{times}
+\usepackage{a4}
+\usepackage{hyperref}
+\usepackage[comma,square]{natbib}
+\usepackage{tikz}
+\usetikzlibrary{automata}
+
+\begin{document}
+
+\noindent
+{\bf Dear Dale, dear Reviewers,}\bigskip
+
+\noindent
+Thank you very much for your time and effort in reviewing this paper. We really appreciate
+this. However we passionately believe that the most important aspect of the paper has \underline{\bf no}t been taken into account
+when reaching your decision, and that Referee No 3, who we assume has extensive expertise in
+regular languages, has proved our point in his review. He brilliantly writes:
+
+\begin{quote}\it
+``the Myhill-Nerode theorem admits a 15-20 lines fairly detailed proof
+ (e.g., see the one given on wikipedia) ; being able to formalise it
+ is not a real challenge from my point of view.''
+\end{quote}
+
+\noindent
+The problem is it \underline{\bf is} a challenge in theorem provers! And the
+real value of the paper and its novelty is that this is a surprising fact, even for experts
+in regular languages, as the report of Referee No 3 shows. Because it is
+surprising, we really think the paper should appear in a more general journal than one
+specialised on theorem provers (after all, many theorem prover people already
+appreciate the difficulties; they
+just did not know of a way how to overcome them elegantly).
+We hope you share with us the belief that theorem prover proofs might not actually
+be used in all subjects, but they are
+the gold standard of proofs and all researchers should be aware of them.\medskip
+
+We therefore kindly ask you to reconsider the decision from this
+point of view and also ask you to consider the supporting
+numbers, which we provided in the paper in order to prove that formalising automata theory \underline{\bf is} a challenge.
+We list them below again for quick reference.
+We are also happy to implement every improvement you suggest that make our general point
+and proofs clearer.\medskip
+
+We can also give one \underline{\bf new} datapoint: \citet{LammichTuerk12} took up the challenge and have formalised a library for NFAs and DFAs
+in approximately 7000 of lines of Isabelle code---this just sets up the framework. For proving the correctness of
+Hopcroft's algorithm they need an additional 7000 lines of Isabelle code. In contrast, our
+paper describes a formalised proof of the most central property in regular language
+theory taking only 1500(!) lines in Isabelle including all definitions and supporting
+lemmas. However, the difficulties with formalising automata theory are \underline{\bf not} restricted
+to Isabelle, as the Reviewers assert, and that you do not have to take
+our word for it, we list below numbers and comments
+made by researchers from \underline{\bf Coq}, \underline{\bf Isabelle} and \underline{\bf Nuprl}. We think similar comments would apply to
+\underline{\bf Matita}, for example, and therefore our paper is written to be as much as possible
+agnostic with respect to a single theorem prover. \medskip
+
+We answer below the specific points the Reviewers raised. We also hope to surprise again
+ Referee No 3
+in that automata complementation is more tricky than it first might appear and
+most textbooks would suggest.\bigskip
+
+
+\newpage
+\noindent
+\underline{\bf Reviewer 1}\medskip
+
+\begin{itemize}
+\item additions with respect to ITP: section 4 gives now a more detailed proof; section 5 and 6 are
+new; the introduction and conclusion are extended with more numbers and comments, which should prove
+beyond doubt our general point that automata are difficult to reason about and regular expressions are
+a better substitute
+\item we did {\bf not} cite \citet{OwensReppyTuron09} for the comment that derivatives ``went lost in the sands of time''
+but that they proved with numbers and an actual implementation that in the context of lexing, derivatives are
+good enough in practice; we believe that this statement is still accurate and it is the only paper that we could
+cite for this
+\item we would be grateful to receive a concrete pointer to the literature: ``{\it The technique is folklore, and can be found in traditional textbooks (possibly passing through left linear
+grammars)}''
+\end{itemize}\bigskip
+
+\noindent
+\underline{\bf Reviewer 2}\medskip
+
+\begin{itemize}
+\item we hope the Reviewer agrees with us that an actual deep analysis of the technical
+details and a comparison with Coq/Sreflect would be a major distraction from the main
+point that the paper wants to convey;
+such an analysis would also be in violation with the editor's guidelines for ToCL
+\end{itemize}\bigskip
+
+\noindent
+\underline{\bf Reviewer 3}\medskip
+
+\noindent
+We honestly enjoyed the comments by Reviewer 3 very much, since they pretty much
+agreed with our view we helt before we started this work---automata theory is
+more than 50 years old, surely nothing can be challenging there. We hope, however, the
+following comments by independent Coq/Nuprl/Isabelle-researchers destroy this view:
+
+\begin{itemize}
+\item[] {\bf Numbers and comments from the literature that reasoning about automata is challenging in theorem provers
+(our formalisation is 1500 loc):}\medskip
+
+\item[{\bf Coq:}] \citet{Braibant12} formalises automata theory including
+ Myhill-Nerode: he writes that our formalisation based on
+ regular expressions ``{\it is more concise}'' than his; he also writes
+ there are no problems with standard textbook proofs,
+ except for the ``{\it {\bf intrinsic} difficulties of working with
+ rectangular matrices}'' in Coq ($>$10k loc)
+
+
+\item [{\bf Coq:}] \citet{Filliatre97} formalised automata theory using matrices
+ leading only to Kleene's theorem, but not
+ Myhill-Nerode nor closure under complementation: he
+ writes his formalisation based on matrices is
+ ``{\it rather big}'' ($>$4.5k loc)
+
+\item[{\bf Coq:}] \citet{Almeidaetal10} verify Mirkin's partial derivatives
+ automata ($>$10k lines of code using matrices)
+
+\item [{\bf Nuprl:}] \citet{Constable00} estimate their 4-member team needs
+ 11 months with Nuprl for chapters 1 - 11 from Hopcroft
+ \& Ullman, which includes Myhill-Nerode ($>$100k lines
+ of code)
+
+\item[{\bf Isabelle:}] \citet{LammichTuerk12} have in Isabelle formalised an automata
+ library (7k loc) and verified Hopcroft's algorithm
+ (additional 7k loc)
+
+\item[{\bf Isabelle:}]
+ \citet{Nipkow98} formalises automata with functions but writes
+ ``{\it proofs require a painful amount of detail}''
+\end{itemize}
+
+\noindent
+These numbers and comments should
+convincingly negate the premises of the following comments from the judgement
+by Reviewer No 3:
+
+\begin{itemize}
+\item ``{\it all formalised mathematical results are well known and established
+ since more than fifty years''} ({\bf we do not contest this nor claim otherwise; we talk about
+ theorem prover proofs - there issues are interesting and we have not seen
+ any previous work that took our view of starting with a definition for regular expressions only})
+\item ``{\it the Myhill-Nerode theorem admits a 15-20 lines fairly detailed proof
+ (e.g., see the one given on wikipedia) ; being able to formalise it
+ is not a real challenge from my point of view.}'' {(\bf not true)}
+\item ``{\it the followed approach is highly specific to Isabelle/HOL: it is
+ driven by the postulate that it's hard to manipulate automata or
+ matrices.}'' ({\bf not true})
+\item ``{\it despite what the authors claim, I'm certain that a mechanised proof
+ of this Theorem could be straightforward in other theorem provers,
+ using automata for the right-to-left direction and partial
+ derivatives for the left-to-right direction''} {\bf (not true)}
+\end{itemize}
+
+\noindent
+Reviewer 3 also raised the following criticisms in his judgement:
+
+\begin{itemize}
+\item ``{\it Moreover, the authors insist on the fact that they don't want to use
+automata, while they actually just rephrase automata-based proofs,
+without using the word `automaton'}''
+
+We did not deliberately avoid the word ``automaton'', but the {\bf definition} of what an automaton
+is. As soon as we start with such a definition, be it in terms of functions, matrices or graphs, we would be in trouble
+with formalised proofs as the loc-numbers above show in comparison to ours.
+
+\item ``{\it All in all, the paper should be presented as `here is a way of doing
+automata in HOL'. I'm sure this would make it much clearer and more
+interesting, notably since doing automata is supposed to be difficult
+in HOL.}''
+
+The fundamental difference is that it is easier in {\bf every} theorem prover to
+reason about inductive datatypes in comparison with non-inductively defined structures
+(graphs, functions, matrices). The specific problem the paper addresses is that
+all textbook proofs of Myhill-Nerode start with a definition of automata leading
+to cumbersome theorem prover proofs in {\bf all} theorem provers we are aware of.
+\end{itemize}\bigskip
+
+\subsection*{Complementation of Automata}
+
+Finally, we like to comment on the difficulty about complementation of automata, which
+on {\bf paper} looks trivial and which highlights the differences between pencil-and-paper textbook
+reasoning and formal proofs in a theorem prover:
+
+\begin{quote}\it
+``if we take the definition `a language is regular if recognised by
+ a finite deterministic automaton (DFA)' then closure under
+ complementation is **trivial** (revert the accepting status of
+ states, that's it)''
+\end{quote}
+
+\noindent
+Given a representation of automata as graphs or
+matrices, then the following
+
+\begin{center}
+\begin{tikzpicture}[scale=3, line width=0.7mm]
+ \node[state, initial] (q0) at ( 0,1) {$q_0$};
+ \node[state, accepting] (q1) at ( 1,1) {$q_1$};
+ \path[->] (q0) edge node[above] {$a$} (q1)
+ (q1) edge [loop right] node {$b$} ()
+ ;
+\end{tikzpicture}
+\end{center}
+
+\noindent
+fits the definition as a graph or matrix of nodes. However interchanging the terminal and
+non-terminal states gives the {\bf incorrect} result. What is needed is the
+notion of a {\bf completed} automaton, such as
+
+\begin{center}
+\begin{tikzpicture}[scale=3, line width=0.7mm]
+ \node[state, initial] (q0) at ( 0,1) {$q_0$};
+ \node[state, accepting] (q1) at ( 1,1) {$q_1$};
+ \node[state] (q3) at (0.5, 1.5) {$q_{sink}$};
+
+ \path[->] (q0) edge node[above] {$a$} (q1)
+ (q1) edge [loop right] node {$b$} ()
+ (q0) edge node[above] {$b$} (q3)
+ (q1) edge node[above] {$a$} (q3)
+ (q3) edge [loop above] node {$a, b$} ()
+ ;
+\end{tikzpicture}
+\end{center}
+
+\noindent
+This additional restriction unfortunately percolates through formalised proofs. In the work by
+\citet{LammichTuerk12}, for example, this completeness constrain is mentioned in 160 places
+out of almost 600 lemmas. Since, their representation is based on graphs (sets of nodes and edges), the restriction
+about finitely many nodes is mentioned in another 108 places. Similarly, badly fare the definitions
+based on matrices in Coq: they need to formalise the shape of matrices and carry around
+this baggage in their proofs and operations (which {\bf all} authors of formalised automata theory in
+Coq point out as clunky). Also, attempting to imitate the textbook definition of a finite
+function of type state $\times$ letter $\rightarrow$ state, which by the way has not been
+used by anybody who formalised automata theory in Coq, does not solve the difficulties: since
+no theorem prover has a finite-function type built in, the additional constraint about finite
+domains need to be carried around, again making proofs clunky.
+
+Regular expressions really solve all the problems mentioned above: they are inductive
+datatypes in all theorem provers, they come with simple structural induction principles
+for free and operations can be easily defined without any restrictions. The concrete question
+the paper answers is whether regular expressions are enough to obtain the central result in
+regular language theory side-stepping the definition of automata which, according to
+all previous work, leads to cumbersome reasoning in all theorem provers. The answer we give is yes:
+If you are in the business of verifying Hopcroft's algorithm there is no way around automata.
+But for Myhill-Nerode there is, and the work involved is reduced by roughly a {\bf factor of 5}.
+We have not found this answer in any of the textbooks or papers available to us. We are happy to
+be proved otherwise.
+
+
+\bibliographystyle{apa}
+\bibliography{root}
+
+\end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/Response/root.bib Wed Dec 12 11:45:04 2012 +0000
@@ -0,0 +1,406 @@
+@InProceedings{CoquandSiles12,
+ author = {T.~Coquand and V.~Siles},
+ title = {{A} {D}ecision {P}rocedure for {R}egular {E}xpression {E}quivalence in {T}ype {T}heory},
+ booktitle = {Proc.~of the 1st Conference on Certified Programs and Proofs},
+ pages = {119--134},
+ year = {2011},
+ volume = {7086},
+ series = {LNCS}
+}
+
+@InProceedings{Asperti12,
+ author = {A.~Asperti},
+ title = {{A} {C}ompact {P}roof of {D}ecidability for {R}egular {E}xpression {E}quivalence},
+ booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving},
+ pages = {283--298},
+ year = {2012},
+ volume = {7406},
+ series = {LNCS}
+}
+
+@InProceedings{LammichTuerk12,
+ author = {P.~Lammich and T.~Tuerk},
+ title = {{A}pplying {D}ata {R}efinement for {M}onadic {P}rograms to {H}opcroft's {A}lgorithm},
+ booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving},
+ year = {2012},
+ volume = {7406},
+ series = {LNCS},
+ pages = {166--182}
+}
+
+@PhdThesis{Braibant12,
+ author = {T.~Braibant},
+ title = {{K}leene {A}lgebras, {R}ewriting {M}odulo {AC}, and {C}ircuits in {C}oq},
+ school = {University of Grenoble},
+ year = {2012}
+}
+
+@incollection{Nipkow11,
+ author = {T.~Nipkow},
+ title = {{G}auss-{J}ordan {E}limination for {M}atrices {R}epresented as {F}unctions},
+ booktitle = {The Archive of Formal Proofs},
+ editor = {G.~Klein and T.~Nipkow and L.~Paulson},
+ publisher = {\url{http://afp.sourceforge.net/entries/Gauss-Jordan-Elim-Fun.shtml}},
+ year = 2011,
+ note = {Formal proof development},
+ ISSN = {2150-914x}
+}
+
+@Article{Haines69,
+ author = {L.~H.~Haines},
+ title = {{O}n {F}ree {M}onoids {P}artially {O}rdered by {E}mbedding},
+ journal = {Journal of Combinatorial Theory},
+ year = {1969},
+ volume = {6},
+ pages = {94--98}
+}
+
+@inproceedings{Berghofer03,
+ author = {S.~Berghofer},
+ title = {{A} {C}onstructive {P}roof of {H}igman's {L}emma in {I}sabelle},
+ booktitle = {In Proc. of the Workshop on Types},
+ year = {2003},
+ pages = {66--82},
+ series = {LNCS},
+ volume = {3085}
+}
+
+@article{Gasarch09,
+ author = {S.~A.~Fenner and W.~I.~Gasarch and B.~Postow},
+ title = {{T}he {C}omplexity of {F}inding {SUBSEQ(A)}},
+ journal = {Theory of Computing Systems},
+ volume = {45},
+ number = {3},
+ year = {2009},
+ pages = {577-612}
+}
+
+@Book{Shallit08,
+ author = {J.~Shallit},
+ title = {{A} {S}econd {C}ourse in {F}ormal {L}anguages and {A}utomata {T}heory},
+ publisher = {Cambridge University Press},
+ year = {2008}
+}
+
+@Unpublished{Rosenberg06,
+ author = {A.~L.~Rosenberg},
+ title = {{A} {B}ig {I}deas {A}pproach to the {T}heory of {C}omputation},
+ note = {Course notes for CMPSCI 401 at the University of Massachusetts},
+ year = {2006}
+}
+
+@incollection{myhillnerodeafp11,
+ author = {C.~Wu and X.~Zhang and C.~Urban},
+ title = {{T}he {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions},
+ booktitle = {The Archive of Formal Proofs},
+ editor = {G.~Klein and T.~Nipkow and L.~Paulson},
+ publisher = {\url{http://afp.sourceforge.net/entries/Myhill-Nerode.shtml}},
+ month = Aug,
+ year = 2011,
+ note = {Formal proof development},
+ ISSN = {2150-914x}
+}
+
+@PhdThesis{Haftmann09,
+ author = {F.~Haftmann},
+ title = {{C}ode {G}eneration from {S}pecifications in {H}igher-{O}rder {L}ogic},
+ school = {Technical University of Munich},
+ year = {2009}
+}
+
+@article{Harper99,
+ author = {R.~Harper},
+ title = {{P}roof-{D}irected {D}ebugging},
+ journal = {Journal of Functional Programming},
+ volume = {9},
+ number = {4},
+ year = {1999},
+ pages = {463-469}
+}
+
+@article{Yi06,
+ author = {K.~Yi},
+ title = {{E}ducational {P}earl: `{P}roof-{D}irected {D}ebugging' {R}evisited
+ for a {F}irst-{O}rder {V}ersion},
+ journal = {Journal of Functional Programming},
+ volume = {16},
+ number = {6},
+ year = {2006},
+ pages = {663-670}
+}
+
+
+@Manual{PittsHOL4,
+ title = {{S}yntax and {S}emantics},
+ author = {A.~M.~Pitts},
+ note = {Part of the documentation for the HOL4 system.}
+}
+
+@article{OwensReppyTuron09,
+ author = {S.~Owens and J.~Reppy and A.~Turon},
+ title = {{R}egular-{E}xpression {D}erivatives {R}e-{E}xamined},
+ journal = {Journal of Functional Programming},
+ volume = 19,
+ number = {2},
+ year = 2009,
+ pages = {173--190}
+}
+
+
+
+@article{KraussNipkow11,
+ author = {A.~Krauss and T.~Nipkow},
+ title = {{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra},
+ journal = {Journal of Automated Reasoning},
+ volume = 49,
+ number = {1},
+ year = {2012},
+ pages = {95--106}
+}
+
+@Book{Kozen97,
+ author = {D.~Kozen},
+ title = {{A}utomata and {C}omputability},
+ publisher = {Springer Verlag},
+ year = {1997}
+}
+
+
+
+@InProceedings{Almeidaetal10,
+ author = {J.~B.~Almeida and N.~Moriera and D.~Pereira and S.~M.~de Sousa},
+ title = {{P}artial {D}erivative {A}utomata {F}ormalized in {C}oq},
+ booktitle = {Proc.~of the 15th International Conference on Implementation
+ and Application of Automata},
+ pages = {59-68},
+ year = {2010},
+ volume = {6482},
+ series = {LNCS}
+}
+
+@incollection{Constable00,
+ author = {R.~L.~Constable and
+ P.~B.~Jackson and
+ P.~Naumov and
+ J.~C.~Uribe},
+ title = {{C}onstructively {F}ormalizing {A}utomata {T}heory},
+ booktitle = {Proof, Language, and Interaction},
+ year = {2000},
+ publisher = {MIT Press},
+ pages = {213-238}
+}
+
+
+@techreport{Filliatre97,
+ author = {J.-C. Filli\^atre},
+ institution = {LIP - ENS Lyon},
+ number = {97--04},
+ title = {{F}inite {A}utomata {T}heory in {C}oq:
+ {A} {C}onstructive {P}roof of {K}leene's {T}heorem},
+ type = {Research Report},
+ year = {1997}
+}
+
+@article{OwensSlind08,
+ author = {S.~Owens and K.~Slind},
+ title = {{A}dapting {F}unctional {P}rograms to {H}igher {O}rder {L}ogic},
+ journal = {Higher-Order and Symbolic Computation},
+ volume = {21},
+ number = {4},
+ year = {2008},
+ pages = {377--409}
+}
+
+@article{Brzozowski64,
+ author = {J.~A.~Brzozowski},
+ title = {{D}erivatives of {R}egular {E}xpressions},
+ journal = {Journal of the ACM},
+ volume = {11},
+ number = {4},
+ year = {1964},
+ pages = {481--494},
+ publisher = {ACM}
+}
+
+@inproceedings{Nipkow98,
+ author={T.~Nipkow},
+ title={{V}erified {L}exical {A}nalysis},
+ booktitle={Proc.~of the 11th International Conference on Theorem Proving in Higher Order Logics},
+ series={LNCS},
+ volume=1479,
+ pages={1--15},
+ year=1998
+}
+
+@inproceedings{BerghoferNipkow00,
+ author={S.~Berghofer and T.~Nipkow},
+ title={{E}xecuting {H}igher {O}rder {L}ogic},
+ booktitle={Proc.~of the International Workshop on Types for Proofs and Programs},
+ year=2002,
+ series={LNCS},
+ volume=2277,
+ pages="24--40"
+}
+
+@book{HopcroftUllman69,
+ author = {J.~E.~Hopcroft and
+ J.~D.~Ullman},
+ title = {{F}ormal {L}anguages and {T}heir {R}elation to {A}utomata},
+ publisher = {Addison-Wesley},
+ year = {1969}
+}
+
+
+@inproceedings{BerghoferReiter09,
+ author = {S.~Berghofer and
+ M.~Reiter},
+ title = {{F}ormalizing the {L}ogic-{A}utomaton {C}onnection},
+ booktitle = {Proc.~of the 22nd International
+ Conference on Theorem Proving in Higher Order Logics},
+ year = {2009},
+ pages = {147-163},
+ series = {LNCS},
+ volume = {5674}
+}
+
+@Article{Church40,
+ author = {A.~Church},
+ title = {{A} {F}ormulation of the {S}imple {T}heory of {T}ypes},
+ journal = {Journal of Symbolic Logic},
+ year = {1940},
+ volume = {5},
+ number = {2},
+ pages = {56--68}
+}
+
+@ARTICLE{Antimirov95,
+ author = {V.~Antimirov},
+ title = {{P}artial {D}erivatives of {R}egular {E}xpressions and
+ {F}inite {A}utomata {C}onstructions},
+ journal = {Theoretical Computer Science},
+ year = {1995},
+ volume = {155},
+ pages = {291--319}
+}
+
+@ARTICLE{Brzozowski10,
+ author = {J.~A.~Brzozowski},
+ title = {{Q}uotient {C}omplexity of {R}egular {L}anguages},
+ journal = {Journal of Automata, Languages and Combinatorics},
+ volume = {15},
+ number = {1/2},
+ pages = {71--89},
+ year = 2010
+}
+
+@book{Sakarovitch09,
+ author = {J.~Sakarovitch},
+ title = {{E}lements of {A}utomata {T}heory},
+ publisher = {Cambridge University Press},
+ year = {2009}
+}
+
+@inproceedings{WuZhangUrban11,
+ author = {C.~Wu and X.~Zhang and C.~Urban},
+ title = {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions
+ ({P}roof {P}earl)},
+ booktitle = {Proc.~of the 2nd International Conference on Interactive Theorem Proving},
+ year = {2011},
+ pages = {341--356},
+ series = {LNCS},
+ volume = {6898}
+}
+
+
+
+
+
+@Article{Okhotin04,
+ author = "A.~Okhotin",
+ title = "{B}oolean {G}rammars",
+ journal = "Information and Computation",
+ pages = "19--48",
+ year = "2004",
+ number = "1",
+ volume = "194"
+}
+
+@Article{KountouriotisNR09,
+ title = "{W}ell-founded {S}emantics for {B}oolean {G}rammars",
+ author = "V.~Kountouriotis and C.~Nomikos and P.~Rondogiannis",
+ journal = "Information and Computation",
+ year = "2009",
+ number = "9",
+ volume = "207",
+ pages = "945--967"
+}
+
+
+@article{Leroy09,
+ author = {X.~Leroy},
+ title = {{F}ormal {V}erification of a {R}ealistic {C}ompiler},
+ journal = {Communications of the ACM},
+ year = {2009},
+ volume = {52},
+ number = {7},
+ pages = {107--115}
+}
+
+
+@Unpublished{Might11,
+ title = "{Y}acc is {D}ead",
+ author = "M.~Might and D.~Darais",
+ note = "To appear in {\it Proc.~of the 16th ACM International Conference on
+ Functional Programming (ICFP)}",
+ year = "2011"
+}
+
+@InProceedings{Ford04,
+ author = "B.~Ford",
+ title = "{P}arsing {E}xpression {G}rammars: {A} {R}ecognition-{B}ased
+ {S}yntactic {F}oundation",
+ booktitle = "Proc.~of the 31st ACM Symposium on Principles of Programming Languages (POPL)",
+ year = "2004",
+ pages = "111--122"
+}
+
+@InProceedings{Ford02,
+ author = "B.~Ford",
+ title = "{P}ackrat {P}arsing: : {S}imple, {P}owerful, {L}azy, {L}inear {T}ime,
+ ({F}unctional {P}earl)",
+ booktitle = "Proc.~of the 7th ACM International Conference on Functional Programming (ICFP)",
+ year = "2002",
+ pages = "36--47"
+
+}
+
+@InProceedings{WarthDM08,
+ title = "{P}ackrat {P}arsers {C}an {S}upport {L}eft {R}ecursion",
+ author = "A.~Warth and J.~R.~Douglass and T.~D.~Millstein",
+ booktitle = "Proc. of the {ACM} Symposium on
+ Partial Evaluation and Semantics-based Program
+ Manipulation (PEPM)",
+ year = "2008",
+ pages = "103--110"
+}
+
+@Article{Earley70,
+ author = "J.~Earley",
+ title = "{A}n {E}fficient {C}ontext-{F}ree {P}arsing {A}lgorithm",
+ journal = "Communications of the ACM",
+ volume = "13",
+ number = "2",
+ pages = "94--102",
+ year = "1970"
+}
+
+@Article{AycHor02,
+ author = "J.~Aycock and R.~N.~Horspool",
+ title = "{P}ractical {E}arley {P}arsing",
+ journal = "The Computer Journal",
+ volume = "45",
+ number = "6",
+ pages = "620--630",
+ year = "2002",
+}
+