regexp: Graph

added slides for talk at Imperial
2012-08-29, by urbanc
(none)
2012-08-13, by wu
add comments by christian
2012-08-13, by wu
Slightly modifications.
2012-08-13, by wu
Slides modified
2012-08-10, by zhang
IsaMakefile modified
2012-08-10, by zhang
added some slides for an informal talk about PIP
2012-06-28, by urbanc
corrected reference to Rostedt article
2012-06-21, by urbanc
small typo in the itp-12 paper
2012-05-24, by urbanc
typo
2012-05-11, by urbanc
updated
2012-05-09, by urbanc
comments by Xingyuan
2012-05-09, by urbanc
some small editing
2012-05-03, by urbanc
tuned paragraph on multiprocesors
2012-05-03, by urbanc
added section about PINTOS and rewritten multi-processor section
2012-05-02, by urbanc
slightly changed the definition of holdends and detached
2012-04-30, by urbanc
made changes for another journal submission of the MN-paper
2012-04-23, by urbanc
changes to get the files through for CU
2012-04-20, by urbanc
made changes for another journal submission of the MH-paper
2012-04-20, by urbanc
Intuitive definition of "detached" is added to PrioG.thy.
2012-04-20, by zhang
added an acknowledgement
2012-04-17, by urbanc
some small tuning
2012-04-17, by urbanc
some small improvements
2012-04-17, by urbanc
???-marks
2012-04-16, by urbanc
changes requested by the reviewers
2012-04-16, by urbanc
polished
2012-04-16, by urbanc
The result for "Set" operation gets strengthened.
2012-04-16, by zhang
added some of the comments of the reviewers and made it compile with current Isabelle
2012-04-15, by urbanc
made the changes thes 2nd referee suggested and made it to compile again
2012-04-13, by urbanc
typo
2012-03-06, by urbanc
fixed typo
2012-02-28, by urbanc
typo
2012-02-27, by urbanc
partially updated conference paper; slightly tuned journal paper
2012-02-22, by urbanc
some polishing of the repository
2012-02-20, by urbanc
one typo
2012-02-16, by urbanc
changes by Xingyuan
2012-02-14, by urbanc
changed
2012-02-14, by urbanc
live
2012-02-14, by urbanc
live
2012-02-14, by urbanc
draft
2012-02-14, by urbanc
draft
2012-02-14, by urbanc
key lemma
2012-02-14, by urbanc
fixed 1st paragraph
2012-02-14, by urbanc
1st paragraph
2012-02-14, by urbanc
1st paragraph
2012-02-13, by urbanc
polished implementation
2012-02-13, by urbanc
Line numbers added.
2012-02-13, by zhang
conclusion done
2012-02-13, by urbanc
more conclusion
2012-02-13, by urbanc
more conclusion
2012-02-13, by urbanc
more conclusion
2012-02-13, by urbanc
more conclusion
2012-02-13, by urbanc
some parts of the conclusion
2012-02-13, by urbanc
proof idea
2012-02-13, by urbanc
added implementation section
2012-02-13, by urbanc
merged Xingyuan's changes
2012-02-13, by urbanc
polished
2012-02-13, by urbanc
more on the paper
2012-02-13, by urbanc
more on the paper
2012-02-13, by urbanc
assumptions
2012-02-13, by urbanc
some polishing
2012-02-13, by urbanc
some polishing
2012-02-12, by urbanc
contribution section
2012-02-12, by urbanc
Correct a mistake.
2012-02-12, by zhang
runing_inversion_3 added.
2012-02-12, by zhang
lates
2012-02-12, by urbanc
correct RAG
2012-02-12, by urbanc
small polishing
2012-02-12, by urbanc
completed model section; vt has only state as argument
2012-02-12, by urbanc
added picture
2012-02-11, by urbanc
spell check; release
2012-02-11, by urbanc
fixed problem with back
2012-02-11, by urbanc
renamed waiting_queue -> wq_fun; cur_preced -> cprec_fun
2012-02-11, by urbanc
some polishing
2012-02-11, by urbanc
fixed problem with Latexsugar
2012-02-11, by urbanc
more on paper; modified schs functions; it is still compatible with the old definition
2012-02-10, by urbanc
more on paper
2012-02-10, by urbanc
attempt to fix problem by Xingyuan
2012-02-09, by urbanc
changes by Xingyuan
2012-02-09, by urbanc
more on the specification section
2012-02-09, by urbanc
corrections by Xingyuan
2012-02-08, by urbanc
more on paper
2012-02-07, by urbanc
more on paper
2012-02-07, by urbanc
paper updatated
2012-02-06, by urbanc
moved unused theories to Attic
2012-02-05, by urbanc
README added.
2012-02-05, by zhang
updated
2012-02-04, by urbanc
slight polishing
2012-02-04, by urbanc
a bit more on the introduction
2012-02-03, by urbanc
slight tuning
2012-02-02, by urbanc
more on intro
2012-02-01, by urbanc
more on intro
2012-02-01, by urbanc
more on intro
2012-02-01, by urbanc
slightly more on text
2012-02-01, by urbanc
All comments added.
2012-02-01, by zhang
spell check
2012-01-30, by urbanc
slight polishing
2012-01-30, by urbanc
more text
2012-01-30, by urbanc
more text
2012-01-30, by urbanc
added two paragraphs to the introduction
2012-01-30, by urbanc
More explanations added by XY.
2012-01-29, by zhang
changed abstract, intro and IsaMakefile
2012-01-27, by urbanc
Newer version.
2012-01-27, by zhang
minor edit
2012-01-24, by urbanc
initial version of the PIP formalisation
2012-01-24, by urbanc
changed to 11 months
2011-12-26, by urbanc
added a draft of the letter for Chunhan
2011-12-22, by urbanc
updated urls to AFP
2011-12-17, by urbanc
added slides for a talk in St Andrews
2011-11-20, by urbanc
small change
2011-11-11, by urbanc
set -> language
2011-09-15, by urbanc
added a paper about applications
2011-09-14, by urbanc
added paper that recently appeared about rexps and pegs
2011-09-14, by urbanc
polished the non-regularity proof
2011-09-14, by urbanc
clarified proof about non-regularity
2011-09-14, by urbanc
corrected typo found by Xingyuan
2011-09-14, by urbanc
small typo
2011-09-13, by urbanc
a final polishing before submitting later this week
2011-09-12, by urbanc
one more itteration on the paper
2011-09-08, by urbanc
some more polishing and a link to Haines
2011-09-07, by urbanc
typos
2011-09-07, by urbanc
polished a bit the journal paper
2011-09-07, by urbanc
typo
2011-09-06, by urbanc
more tuning on the proposal
2011-09-06, by urbanc
polished proposal
2011-09-06, by urbanc
tuning on the derivatives and closures theories
2011-09-05, by urbanc
added section about non-regularity
2011-09-05, by urbanc
polished SUBSEQ
2011-09-05, by urbanc
slight polishing to SUBSEQ
2011-09-05, by urbanc
slight polishing to SUBSEQ
2011-09-05, by urbanc
shortened
2011-09-05, by urbanc
some changes
2011-09-05, by urbanc
some changes
2011-09-05, by urbanc
added section about SUBSEQ and SUPSEQ
2011-09-05, by urbanc
Proposal paragraphs by Xingyuan completed (with references added).
2011-09-04, by zhang
removed the last two sorry's
2011-09-04, by urbanc
More modification by Xingyuan.
2011-09-02, by zhang
One passage added.
2011-09-02, by zhang
latest changes
2011-09-02, by urbanc
small change
2011-09-02, by urbanc
small improvement
2011-09-02, by urbanc
added a start for a proposal
2011-09-02, by urbanc
added example about non-regularity
2011-09-02, by urbanc
cleaned up proofs
2011-09-02, by urbanc
included Higman's lemma from the Isabelle repository
2011-09-01, by urbanc
solved the SUBSEQ/SUPSEQ problem
2011-09-01, by urbanc
added a further test
2011-08-30, by urbanc
corrected typo
2011-08-26, by urbanc
added a few points
2011-08-26, by urbanc
a few bits on the journal paper
2011-08-25, by urbanc
shown slides
2011-08-25, by urbanc
final polishing
2011-08-25, by urbanc
added pdf of slides
2011-08-24, by urbanc
final slides
2011-08-24, by urbanc
more slides
2011-08-24, by urbanc
more on slides
2011-08-24, by urbanc
just test
2011-08-24, by urbanc
added test for Higman's lemma
2011-08-23, by urbanc
more on slides
2011-08-23, by urbanc
more on the slides
2011-08-23, by urbanc
more on the slides
2011-08-23, by urbanc
forgotten file
2011-08-23, by urbanc
beginnig of the slides (not yet finished)
2011-08-23, by urbanc
changes according to afp-submission
2011-08-22, by urbanc
two more literature
2011-08-19, by urbanc
added comments by Xingyuan
2011-08-19, by urbanc
added an example for non-regularity and continuation lemma (the example does not yet work)
2011-08-17, by urbanc
a little tuning
2011-08-17, by urbanc
final(?) version of the paper
2011-08-16, by urbanc
a bit more polishing
2011-08-15, by urbanc
polishing of the closure section and conclusion
2011-08-15, by urbanc
small typo
2011-08-12, by urbanc
some typos
2011-08-11, by urbanc
finished section about derivatives and closure properties
2011-08-11, by urbanc
two interesting papers
2011-08-11, by urbanc
slight polishing
2011-08-11, by urbanc
more on paper
2011-08-09, by urbanc
more on paper and literature
2011-08-09, by urbanc
added paper on partial derivatives
2011-08-05, by urbanc
more on the derivatives section
2011-08-05, by urbanc
added more to the derivatives section
2011-08-03, by urbanc
completed the taging-function section
2011-08-03, by urbanc
more on the paper
2011-08-03, by urbanc
cleaned up the proofs in Myhill_2
2011-08-03, by urbanc
a version of the proof which dispenses with the notion of string-subtraction
2011-08-02, by urbanc
some experiments with the proofs in Myhill_2
2011-07-31, by urbanc
added a picture
2011-07-28, by urbanc
small improvements
2011-07-28, by urbanc
added more examles
2011-07-28, by urbanc
more one the paper
2011-07-28, by urbanc
latest version of the journal paper
2011-07-27, by urbanc
polished the introduction
2011-07-27, by urbanc
more on the section about derivatives
2011-07-26, by urbanc
more on the introduction of the journal paper
2011-07-26, by urbanc
more on the journal paper
2011-07-25, by urbanc
added a paper about PEG-parsing and left recursion
2011-07-25, by urbanc
made the theories compatible with the existing developments in the AFP; old theories are in the directory Attic
2011-07-25, by urbanc
added boolean grammar
2011-06-03, by zhang
added
2011-06-03, by zhang
added a journal version
2011-06-02, by urbanc
updated theories and itp-paper
2011-06-02, by urbanc
added missing file
2011-05-31, by urbanc
added old paper
2011-05-29, by urbanc
a few more literature places
2011-05-26, by urbanc
added directory for journal version; took uptodate version of the theory files
2011-05-18, by urbanc
preparation for final paper version
2011-05-12, by urbanc
added comments from Chunhan
2011-05-09, by urbanc
edits; sqeezed to 16 pages
2011-05-04, by urbanc
paper about formalising parsing; seems to have done what we would like to do....probably also appears at ITP'11
2011-04-28, by urbanc
a small change
2011-04-21, by urbanc
a few more changes
2011-04-21, by urbanc
removed experimental code from Matcher
2011-04-19, by urbanc
implemented most suggestions from the reviewers
2011-04-19, by urbanc
added literature about parsing
2011-04-06, by urbanc
MN via partial derivatives
2011-03-25, by urbanc
moved paper to correct place
2011-03-23, by urbanc
added paper by Antimirov
2011-03-23, by urbanc
added the most current versions of the theories.
2011-03-23, by urbanc
correct version
2011-03-15, by urbanc
deleted wrong version
2011-03-15, by urbanc
added chapter about regular expressions by Sakarovitch (interesting pages are 139 - 142)
2011-03-15, by urbanc
corrected small typo
2011-03-15, by urbanc
slight polishing of the bibliography
2011-03-05, by urbanc
formalisation of first direction is now only 780 loc
2011-03-05, by urbanc
changed one occurence of tagging function into tagging relation
2011-02-26, by urbanc
added yacc is dead paper
2011-02-25, by urbanc
added a paper about derivatives
2011-02-24, by urbanc
added hocroft and ullman book
2011-02-24, by urbanc
three typos
2011-02-22, by urbanc
one further polishing
2011-02-21, by urbanc
final final polishing
2011-02-21, by urbanc
final polished
2011-02-21, by urbanc
chunhan's comments
2011-02-21, by urbanc
minor change
2011-02-20, by urbanc
comments by Xingyuan
2011-02-20, by urbanc
chunhan's comments
2011-02-20, by urbanc
pre-final version
2011-02-20, by urbanc
minor
2011-02-20, by urbanc
finished picture
2011-02-20, by urbanc
seq case finished
2011-02-20, by urbanc
latest update
2011-02-20, by urbanc
added pictures for seq-case
2011-02-20, by urbanc
added definition of string prefix and string subtraction
2011-02-20, by urbanc
polished everywhere...two cases still missing
2011-02-20, by urbanc
my latest version (SEQ and STAR still missing)
2011-02-19, by urbanc
added directory with the small files and numbers of lines
2011-02-19, by urbanc
ALT case done
2011-02-19, by urbanc
first two proofs in 2 direction
2011-02-19, by urbanc
first proof
2011-02-19, by urbanc
updated second direction
2011-02-19, by urbanc
included comments by Chunhan
2011-02-19, by urbanc
added comment from Larry
2011-02-18, by urbanc
updated bib
2011-02-18, by urbanc
polished everything
2011-02-18, by urbanc
more on the conclusion
2011-02-17, by urbanc
first ideas about conclusion
2011-02-17, by urbanc
completed first direction
2011-02-17, by urbanc
minor updated
2011-02-16, by urbanc
filled details in one place
2011-02-16, by urbanc
updated paper
2011-02-15, by urbanc
updated paper
2011-02-15, by urbanc
updated paper
2011-02-15, by urbanc
updated paper
2011-02-15, by urbanc
updated
2011-02-14, by urbanc
added definition of DERIV and delta
2011-02-14, by urbanc
updated paper
2011-02-14, by urbanc
updated
2011-02-14, by urbanc
More into the second direction
2011-02-13, by zhang
included comments by Xingyuan
2011-02-11, by urbanc
slightly streamlined the proof
2011-02-11, by urbanc
simplified a bit the proof
2011-02-10, by urbanc
more things
2011-02-10, by urbanc
latest on the paper
2011-02-10, by urbanc
more on the paper
2011-02-10, by urbanc
more on paper
2011-02-10, by urbanc
added Xingyuan's changes with the while combinator
2011-02-09, by urbanc
added an example
2011-02-09, by urbanc
a bit more on the paper
2011-02-09, by urbanc
added something about Setalt and folds
2011-02-09, by urbanc
deleted the non_empty invariant
2011-02-09, by urbanc
tuned comments and names in Myhill_1
2011-02-09, by urbanc
separated the definition of folds into a separate file
2011-02-09, by urbanc
saved a copy of the current Myhill for reference
2011-02-09, by urbanc
a bit more on the paper
2011-02-08, by urbanc
added coments about functions
2011-02-08, by urbanc
more direct definitions
2011-02-08, by urbanc
deleted lam_of
2011-02-08, by urbanc
started to define things more directly
2011-02-08, by urbanc
More explaination on equational system
2011-02-08, by zhang
small additions
2011-02-08, by urbanc
added an abbreviation for folds ALT NULL
2011-02-08, by urbanc
parts of the 3 section
2011-02-07, by urbanc
added bib-file
2011-02-07, by urbanc
More into first direction
2011-02-07, by zhang
added an option fullpaper to IsaMakefile
2011-02-07, by urbanc
more on the paper
2011-02-07, by urbanc
slightly more on the paper
2011-02-06, by urbanc
A formal presentation of automaton and Myhill-Nerrode theorem added to serve as a basis for further discussion
2011-02-06, by zhang
Check in Myhill.thy before trying another way to explain DFA
2011-02-05, by zhang
more intro
2011-02-05, by urbanc
more on the introduction
2011-02-04, by urbanc
exercise about arden from TU Munich
2011-02-04, by urbanc
Added something to Myhill.thy, trying to explain the relationship between finite automata and language partition.
2011-02-04, by zhang
Myhill_2.thy added
2011-02-03, by zhang
Copy Myhill.thy into Myhill_2.thyand put Myhill_2.thy into logic ListP. Myhill.thy is now almost empty ready to be extended by new manuscripts.
2011-02-03, by zhang
more to the intro
2011-02-03, by urbanc
a bit more tuning on the introduction
2011-02-03, by urbanc
more on the intro
2011-02-02, by urbanc
a little bit in the introduction
2011-02-02, by urbanc
Myhill.pdf modified
2011-02-02, by zhang
removed the inductive definition of Star and replaced it by a definition in terms of pow
2011-02-02, by urbanc
Myhill.thy IsabelleMakefile modified
2011-01-31, by zhang
a bit more on the paper
2011-01-31, by urbanc
small typo
2011-01-30, by urbanc
tuning of the syntax; needs the stmaryrd latex package
2011-01-30, by urbanc
some tuning of the paper
2011-01-30, by urbanc
revised proof of Ardens lemma
2011-01-30, by urbanc
Illustration added together with renewed explainations for case STAR.
2011-01-30, by zhang
Myhill.thy and Myhill_1.thy changed.
2011-01-29, by zhang
slightly tuned the main lemma and the finiteness proofs
2011-01-28, by urbanc
test
2011-01-28, by wu
More improvement
2011-01-28, by zhang
added a recent paper about reg exps and automata
2011-01-27, by wu
added my changes again
2011-01-27, by urbanc
Trying to solve the confict
2011-01-27, by zhang
a newer version
2011-01-27, by zhang
tuned a bit more the last STAR-proof
2011-01-27, by wu
tuned a little bit the section about finite partitions
2011-01-27, by urbanc
Delete generated
2011-01-26, by zhang
ITP-Paper loads Myhill.thy
2011-01-26, by wu
added an itp entry to IsaMakefile; fixed problem with eqref; have not used heap file ListP
2011-01-26, by wu
made the theory work under both Isabelle 2009 and 2011
2011-01-26, by urbanc
Just checkin
2011-01-26, by zhang
Small modification
2011-01-26, by zhang
ok
2011-01-26, by zhang
1. Myhill.thy is proved to correct some typos. 2. Some sections are added to the first direction. 3. The small theory of list difference is now separated into Prefix_subtract.thy and the ROOT.ML
2011-01-25, by zhang
Directory [tphols-2011] is added to host the commented version of [Myhill.thy]. Directory [pres] is created to host a build session for logical image [ListP] which is essentially [Main] extended with [List_prefix.thy].
2011-01-24, by zhang
Beautifying of the Other Direction is finished.
2011-01-07, by wu
Rewritten of hard direction once more. To make it looking better.
2010-12-31, by wu
Add new file for the new definition of the hard direction's simplification.
2010-12-14, by wu
added a recent paper by Tobias Nipkow on regular expressions
2010-11-26, by urbanc
added interesting paper by rutten
2010-11-26, by urbanc
added paper
2010-11-25, by urbanc
All cases of the Other direction finished
2010-11-18, by wu
added a test file
2010-11-10, by urbanc
my slides from the talk in Cambridge
2010-11-10, by urbanc
added my slides
2010-11-10, by urbanc
slight tuning of proof by Chunhan
2010-11-08, by urbanc
the ALT case is done;
2010-11-06, by wu
added more experiments
2010-11-03, by urbanc
added initial slides for informal talk in Cambridge
2010-11-03, by urbanc
added slides of chunhan
2010-10-26, by urbanc
more experiments
2010-10-26, by urbanc
a few more experiments, but no proof for the ALT-case
2010-10-24, by urbanc
add some proofs about the other direction
2010-10-23, by wu
deleted two unnecessary lemmas
2010-10-22, by urbanc
added a paper by Constable about the Myhill-Nerode in Nuprl using DFA and a paper by tobias about RegExp->DFA translation
2010-10-22, by urbanc
deleted the test
2010-10-21, by urbanc
tried at the end to prove the other direction (failed at the moment)
2010-10-21, by urbanc
deleted the matcher ate the beginning; made it to work with stable Isabelle and the development version
2010-10-21, by urbanc
former version has a ugly usage of "overloaded";
2010-10-20, by wu
added a file about the easy closure properties of regular sets (the difficult parts, like complement, are missing)
2010-10-19, by urbanc
Add a test file, after testing, this file can be deleted.
2010-10-07, by wu
added simple regexp matcher from Slind et al
2010-10-03, by urbanc
test
2010-10-03, by urbanc
added literature
2010-10-03, by urbanc
added initial version by Chunhan
2010-10-03, by urbanc