@inProceedings{ACL2,
author = {Gordon, M. J. C. and Reynolds, J. and Hunt, W. A. and Kaufmann, M.},
title = {An Integration of {HOL} and {ACL2}},
booktitle ={FMCAD 2006},
year = {2006},
pages = {153--160},
publisher = {IEEE Computer Society},
}

@article{FosterS15,
  author    = {Foster, S. and
               Struth, G.},
  title     = {On the Fine-Structure of Regular Algebra},
  journal   = {J. Automated Reasoning},
  volume    = {54},
  number    = {2},
  pages     = {165--197},
  year      = {2015},
}


@InProceedings{ArmstrongGomesStruth,
  author =       {Armstrong, A. and Gomes, V. B. F. and Struth, G.},
  title =        {Algebras for Program Correctness in {I}sabelle/{HOL}},
  booktitle = {RAMICS'14},
year = 2014,
  note =      {(In Press)}}



@Article{ArmstrongStruthWeber,
  author =       {Armstrong, A. and Struth, G. and Weber, T.},
  title =        {Programming and Automating Mathematics in the {T}arski-{K}leene Hierarchy},
  journal =      {J. Logic and Algebraic Programming},
  year =         2014,
  ee        = {https://doi.org/10.1016/j.jlap.2014.02.001},
note = {(In Print)}
}

@article{ArmstrongStruthWeberArchive,
  author    = {Armstrong, A. and
               Struth, G. and
               Weber, T.},
  title     = {Kleene Algebra},
  journal   = {Archive of Formal Proofs},
  year      = {2013},
  note      = {\url{http://isa-afp.org/entries/Kleene_Algebra.shtml}, Formal proof development},
}

@InProceedings{Ballarin,
  author =       {Ballarin, C.},
  title =        {Tutorial to Locales and Locale Interpretation},
  booktitle = {Contribuciones Cient{\'\i}ficas en honor de Mirian Andr\'es},
  year =      2010,
  editor =    {Lamb{\'a}n, L. and Romero, A. and Rubio, J.},
  publisher = {Servicio de Publicationes de la Universidad de La Rioja}}

@inproceedings{BenzmuellerSultana,
  author    = {Benzm\"uller, C. and Sultana, N.},
  title     = {LEO-{II} {V}ersion 1.5},
  booktitle = {PxTP 2013},
  editor    = {Blanchette, J. C. and Urban, J.},
  series    = {EPiC Series},
  volume    = {14},
  pages     = {2--10},
  year      = {2013},
  publisher = {EasyChair},
}

@inproceedings{BlanchetteBulwahnNipkow,
  author    = {Blanchette, J. C. and
               Bulwahn, L. and
               Nipkow, T.},
  title     = {Automatic Proof and Disproof in {I}sabelle/{HOL}},
  booktitle = {FroCos 2011},
  year      = {2011},
volume      = {6989},
  pages     = {12--27},
  editor    = {Tinelli, C. and
               Sofronie-Stokkermans, V.},
  publisher = {Springer},
  series    = {LNAI},
}

@Article{BloomEsik,
  author =       {Bloom, S. L. and \'Esik, Z.},
  title =        {Equational Axioms for Regular Sets},
  journal =      {Mathematical Structures in Computer Science},
  year =         1993,
  volume =    3,
  number =    1,
  pages =     {1--24}}

@Article{Boffa1,
  author =       {Boffa, M.},
  title =        {Une remarque sur les syst{\`e}mes complets d'identit{\'e}s rationnelles},
  journal =      {Informatique th{\'e}orique et applications},
  year =         1990,
  volume =    24,
  number =    4,
pages = {419--423},

}

@Article{Boffa2,
  author =       {Boffa, M.},
  title =        {Une condition impliquant toutes les identit{\'e}s rationnelles},
  journal =      {Informatique th{\'e}orique et applications},
  year =         1995,
  volume =    29,
  number =    6,
pages = {515--518},

}

@InProceedings{BraibantPous,
  author =       {Braibant, T. and Pous, D.},
  title =        {An efficient {C}oq tactic for deciding {K}leene algebras},
  booktitle = {ITP 2010},
  pages =     {163--178},
  year =      2010,
  editor =    {Kaufmann, M. and Paulson, L.},
  volume =    {6172},
  series =    {LNCS},
  publisher = {Springer}}

@Book{Conway,
	author		= {Conway, J. H.},
	title		= {Regular Algebra and Finite Machines},
	publisher	= {Chapman and Hall},
	year		= 1971
}

@Book{Eilenberg,
  author =    {Eilenberg, S.},
  title =        {Automata, Languages and Machines},
  publisher =    {Academic Press},
  year =         1976}

@article{Esik,
  author    = {{\'E}sik, Z.},
  title     = {Group Axioms for Iteration},
  journal   = {Information and Computation},
  volume    = {148},
  number    = {2},
  year      = {1999},
  pages     = {131--180},
}

@article{FosterStruthArchive,
  author    = {Foster, S. and
               Struth, G.},
  title     = {Regular Algebras},
  journal   = {Archive of Formal Proofs},
  volume    = {2014},
  year      = {2014},
  ee        = {http://isa-afp.org/entries/Regular_Algebra.shtml},
}

@Book{Ginzburg,
  author =    {Ginzburg, A.},
  title =        {Algebraic Theory of Automata},
  publisher =    {Academic Press},
  year =         1968}

@article{Guttmann,
  author    = {Guttmann, W.},
  title     = {Algebras for iteration and infinite computations},
  journal   = {Acta Informatica},
  volume    = {49},
  number    = {5},
  year      = {2012},
  pages     = {343--359},
}



@InProceedings{GuttmannStruthWeber,
  author =       {Guttmann, W. and Struth, G. and Weber, T.},
  title =        {Automating Algebraic Methods in {I}sabelle},
  booktitle = {ICFEM 2011},
  pages =     {617--632},
  year =      2011,
  editor =    {Qin, S. and Qiu, Z.},
  volume =    6991,
  series =    {LNCS},
  publisher = {Springer}}


@article{HoefnerStruth,
  author    = {H{\"o}fner, P. and
               Struth, G.},
  title     = {Algebraic notions of nontermination: Omega and divergence
               in idempotent semirings},
  journal   = {J. Logic and  Algebraic Programming},
  volume    = {79},
  number    = {8},
  year      = {2010},
  pages     = {794--811},
}


@Unpublished{IsabelleHOL,
  author = 	 {Paulson, L. and Nipkow, T. and Wenzel, M.},
  title = 	 {Isabelle},
  note = 	 {{\tt http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html}},
year = {2011},
}

@Misc{Kasparov,
  author =    {Kasparov Garry},
  title =     {The Chess Master and the Computer},
  howpublished = {The New York Review of Books},
  month =     {11.2.},
  year =      2010,
  note =      {\url{http://www.nybooks.com/articles/archives/2010/feb/11/}}}


@InCollection{Kleene,
  author =       {Kleene, S. C.},
  title =        {Representation of Events in Nerve Nets and Finite Automata},
  booktitle =    {Automata Studies},
  pages =     {3--41},
  publisher = {Princeton University Press},
  year =      1956,
  editor =    {Shannon, C. E. and McCarthy, J.},
  chapter =   1956}

@Article{Kozen,
 author    = {Kozen, D.},
 title     = {A Completeness Theorem for {K}leene Algebras and the
              Algebra of Regular Events},
 journal   = {Information and Computation},
 volume    = {110},
 number    = {2},
 pages     = {366--390},
 year      = {1994}
}

@inproceedings{Kozensemi,
  author    = {Kozen, D.},
  title     = {On {K}leene Algebras and Closed Semirings},
  booktitle = {MFCS'90},
  year      = {1990},
  pages     = {26--47},
  editor    = {Rovan, B.},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {452},
}

@Article{Krob,
  author =       {Krob, D.},
  title =        {Complete Systems of $\mathcal{B}$-Rational Identities},
  journal =      {Theoretical Computer Science},
  year =         1991,
  volume =    89,
  pages =     {207--343}}

@Article{NipkowKrauss,
  author =       {Krauss, A. and Nipkow, T.},
  title =        {Proof Pearl: Regular Expression Equivalence and Relation Algebra},
  journal =      {J. Automated Reasoning},
  year =         2011,
  ee =      {https://doi.org/10.1007/s10817-011-9223-4}}

@Book{NipkowPaulsonWenzel2002,
	author		= {Nipkow, T. and Paulson, L. C. and Wenzel, M.},
	title		= {Isabelle/HOL: A Proof Assistant for Higher-Order Logic},
	publisher	= {Springer},
	series		= {LNCS},
	volume		= {2283},
	year		= 2002,
}


@TechReport{Pratt,
  author =       {Pratt, V.},
  title =        {Action Logic and Pure Induction},
  institution =  {Department of Computer Science, Stanford University},
  year =         1990,
  number =    {STAN-CS-90-1343}}

@Article{Redko,
  author =       {Redko, V. N.},
  title =        {On the determining totality of an algebra of regular events},
  journal =      {Ukrain. Math. Z.},
  year =         1964,
  volume =    16,
  pages =     {120--126},
  note =      {(in Russian)}
}

@article{Salomaa,
  author    = {Salomaa, A.},
  title     = {Two Complete Axiom Systems for the Algebra of Regular Events},
  journal   = {J. ACM},
  volume    = {13},
  number    = {1},
  year      = {1966},
  pages     = {158--169},
}

@inproceedings{WuZhangUrban,
  author    = {Wu, C. and
               Zhang, X. and
               Urban, C.},
  title     = {A Formalisation of the {M}yhill-{N}erode Theorem Based on Regular
               Expressions (Proof Pearl)},
  booktitle = {ITP 2011},
  year      = {2011},
  pages     = {341--356},
  editor    = {van Eekelen, M. C. J. D. and
               Geuvers, H. and
               Schmaltz, J. and
               Wiedijk, F.},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {6898}
}

@book{bertot2004interactive,
  title={Interactive Theorem Proving and and Program Development -- Coq'Art: the calculus of inductive constructions},
  author={Bertot, Y. and Cast{\'e}ran, P.},
  year={2004},
  publisher={Springer}
}

@inproceedings{blanchette10,
year={2010},
isbn={978-3-642-14051-8},
booktitle={Interactive Theorem Proving},
volume={6172},
series={LNCS},
editor={Kaufmann, M. and Paulson, L. C.},
doi={10.1007/978-3-642-14052-5_11},
title={Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder},
publisher={Springer},
author={Blanchette, J. C. and Nipkow, T.},
pages={131-146}
}


@InProceedings{bove09agda,
  author =       {Bove, A. and Dybjer, A. and Norell, U.},
  title =        {A Brief Overview of Agda -- A Functional Language
                  with Dependent Types},
  OPTcrossref =  {},
  OPTkey =       {},
  booktitle =    {Theorem Proving in Higher Order Logics},
  OPTpages =     {},
  year =         {2009},
  OPTeditor =    {},
  volume =       {5674},
  OPTnumber =    {},
  series =       {LNCS},
  OPTaddress =   {},
  OPTmonth =     {},
  OPTorganization = {},
  publisher =    {Springer},
  OPTnote =      {},
  OPTannote =    {}
}

@inproceedings{brady11idris,
  author    = {Brady, E.},
  title     = {IDRIS -- systems programming meets full dependent types},
  booktitle = {Proc. 5th ACM Workshop on Programming Languages
               meets Program Verification},
  year      = {2011},
  pages     = {43--54},
  publisher = {ACM}
}

@inproceedings{bulwahn12,
year={2012},
booktitle={Certified Programs and Proofs},
volume={7679},
series={LNCS},
editor={Hawblitzel, C. and Miller, D.},
title={The New {Q}uickcheck for {I}sabelle},
publisher={Springer},
author={Bulwahn, L.},
pages={92--108}
}

@inProceedings{huffman12lifting,
year=2013,
booktitle={CPP 2013},
volume=8307,
series={LNCS},
editor={Gonthier, G. and Norrish, M.},
title={Lifting and Transfer: A Modular Design for Quotients in {I}sabelle/{HOL}},
publisher={Springer International Publishing},
author={Huffman, B. and Kuncar, O.},
pages={131--146}
}

@article{iancu11,
author = {Iancu, M. and Rabe, F.},
title = {Formalizing foundations of mathematics},
journal = {Mathematical Structures in Computer Science},
volume = {21},
issue = {4},
pages = {883--911},
year = {2011}
}


