Name		Name	Last commit message	Last commit date
parent directory ..
Readme.md		Readme.md
SimplificationRules.v		SimplificationRules.v
compare_regex.v		compare_regex.v
derive.v		derive.v
derive_def.v		derive_def.v
main.v		main.v
matches_pred.v		matches_pred.v
matches_pred_proofs.v		matches_pred_proofs.v
nullable.v		nullable.v
regex.v		regex.v
set_of_sequences.v		set_of_sequences.v
setoid.v		setoid.v
simple.v		simple.v
simplified.v		simplified.v
size.v		size.v
smart.v		smart.v
smart_or.v		smart_or.v

Readme.md

Regular-expression derivatives reexamined

Regular-expression derivatives reexamined is a very readable paper by Scott Owens, John Reppy and Aaron Turon.

In this folder we try to reexamine this reexamining using Coq.