paper.bib

@MastersThesis{Aarts,
  author =       {Aarts, C.~J.},
  title =        {Galois Connections Presented Calculationally},
  school =       {Department of Mathematics and Computing Science, Eindhoven University of Technology},
  year =         1992,
}

@article{Aboul-Hosn,
  author    = {Aboul-Hosn, K. and
               Kozen, D.},
  title     = {{KAT-ML}: an interactive theorem prover for {K}leene algebra
               with tests},
  journal   = {Journal of Applied Non-Classical Logics},
  volume    = {16},
  number    = {1--2},
  year      = {2006},
  pages     = {9--34},
}

@techreport{Angus,
  author="Angus, A. and Kozen, D.",
  title="Kleene Algebra with Tests and Program Schematology",
  institution="Computer Science Department, Cornell University",
  number="TR2001-1844",
  month="July",
  year="2001"
}

@article{Archive,
  author    = {Armstrong, A. and
               Struth, G. and
               Weber, T.},
  title     = {Kleene Algebra},
  journal   = {Archive of Formal Proofs},
  year      = {2013},
  ee        = {http://afp.sourceforge.net/entries/Kleene_Algebra.shtml},
}


@article{Arden,
author = {Arden, D. N.},
title = {Delayed-logic and finite-state machines},
journal ={Annual IEEE Symposium on Foundations of Computer Science},
volume = {0},
year = {1961},
pages = {133--151},
publisher = {IEEE Computer Society},
}


@Unpublished{Armstrong,
  author =       {Armstrong, A.},
  title =        {Automated Theorem Prover Evaluation in Regular Algebra},
  note =         {(To be submitted to the RAMiCS-13 doctoral symposium)},
  year =      2012}

@inproceedings{ArmstrongRAMICS,
  author    = {Armstrong, A. and
               Struth, G.},
  title     = {Automated Reasoning in Higher-Order Regular Algebra},
  booktitle = {RAMiCS},
  year      = {2012},
  pages     = {66--81},
  ee        = {http://dx.doi.org/10.1007/978-3-642-33314-9_5},
  crossref  = {DBLP:conf/RelMiCS/2012},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{AspertiRicciotti,
  author    = {Asperti, A. and
               Ricciotti, W. and
               Coen, C.~S. and
               Tassi, E.},
  editor    = {Berghofer, S. and
               Nipkow, T. and
               Urban, C. and
               Wenzel, M.},
  title     = {Hints in Unification},
  booktitle = {TPHOLs 2009},
  publisher = {Springer2},
  series    = {LNCS},
  volume    = {5674},
  year      = {2009},
  pages     = {84--98},
}



@BOOK{Back1998,
  title = {Refinement Calculus: A Systematic Introduction},
  publisher = {Springer},
  year = {1998},
  author = {Back, R-J. and von Wright, J.}
}

@Article{BackhouseCarre,
  author =       {Backhouse, R. C. and Carr{\'e}, B. A.},
  title =        {Regular Algebras Applied to Path-finding Problems},
  journal =      {IMA J. Appl. Math.},
  year =         {1975},
  volume =    {15},
  number =    {2},
  pages =     {161--186},
}

@InCollection{Ballarin,
  author =       {Ballarin, C.},
  title =        {Tutorial to Locales and Locale Interpretation},
  booktitle =    {Contribuciones Cient\'ificas en honor de Mirian Andr\'es},
  publisher = {Servicio de Publicaciones de la Universidad de La Rioja, Spain},
  year =      2010}

@inproceedings{BerghammerStruth,
  author    = {Berghammer, R. and
               Struth, G.},
  title     = {On Automated Program Construction and Verification},
  booktitle = {MPC 2010},
  year      = 2010,
  pages     = {22--41},
  editor    = {Bolduc, C. and
               Desharnais, J. and
               Ktari, B.},
  publisher = {Springer},
  series    = {LNCS},
  volume    = 6120,
}


@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},        
  pages     = {12--27},
  editor    = {Tinelli, C. and
               Sofronie-Stokkermans, V.},
  publisher = {Springer},
  series    = {LNCS},

}

@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},

}

@MastersThesis{Bolduc,
  author =       {Bolduc, C.},
  title =        {Om{\'e}ga-alg{\`e}bre: th{\'e}orie et application en v{\'e}rification de programmes},
  school =       {Facult{\'e} des Sciences et de G{\'e}nie, Universit{\'e} Laval, Canada },
  year =         2006}

@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}}



@article{Brzozowski,
  author    = {Brzozowski, J. A.},
  title     = {Derivatives of Regular Expressions},
  journal   = {J. ACM},
  volume    = {11},
  number    = {4},
  year      = {1964},
  pages     = {481--494},
}

@inproceedings{Cohen,
  author    = {Cohen, E.},
  title     = {Separation and Reduction},
  booktitle = {MPC 2000},
editor    = {Backhouse, R. C. and
               Nuno Oliveira, J.},
publisher = {Springer},
  series    = {LNCS},
  volume    = {1837},
  year      = {2000},
  pages     = {45--59},
}

@InCollection{CollavizzaGordon,
  author =       {Collavizza, H. and Gordon, M.},
  title =        {Forward with {H}oare},
  booktitle =    {Reflections on the Work of C. A. R. Hoare},
  pages =     {101--121},
  publisher = {Springer},
  year =      2010,
  editor =    {Roscoe, A. W. and Jones, C. B. and Wood, K. R.}}

@Book{Conway,
	author		= {Conway, J. H.},
	title		= {Regular Algebra and Finite Machines},
	publisher	= {Chapman and Hall},
	year		= 1971,
	isbn		= {0-412-10620-5},
	note		= {}
}

@proceedings{DBLP:conf/RelMiCS/2003conf,
  editor    = {Berghammer, R. and
               M{\"o}ller, B. and
               Struth, G.},
  title     = {Relational and Kleene-Algebraic Methods in Computer Science:
               7th International Seminar on Relational Methods in Computer
               Science and 2nd International Workshop on Applications of
               Kleene Algebra, Bad Malente, Germany, May 12-17, 2003, Revised
               Selected Papers},
  booktitle = {RelMiCS},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3051},
  year      = {2004},
  isbn      = {3-540-22145-X},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/RelMiCS/2012,
  editor    = {Kahl, W. and
               Griffin, T.~G.},
  title     = {Relational and Algebraic Methods in Computer Science - 13th
               International Conference, RAMiCS 2012, Cambridge, UK, September
               17-20, 2012. Proceedings},
  booktitle = {RAMICS},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {7560},
  year      = {2012},
  isbn      = {978-3-642-33313-2},
  ee        = {http://dx.doi.org/10.1007/978-3-642-33314-9},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/cade/2007,
  editor    = {Pfenning, F.},
  title     = {Automated Deduction - CADE-21, 21st International Conference
               on Automated Deduction, Bremen, Germany, July 17-20, 2007,
               Proceedings},
  booktitle = {CADE},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {4603},
  year      = {2007},
}

@proceedings{DBLP:conf/sac/2011,
  editor    = {Chu, W.~C. and
               Wong, W.~E. and
               Palakal, M.~J. and
               Hung, C.-C.},
  title     = {Proceedings of the 2011 ACM Symposium on Applied Computing
               (SAC), TaiChung, Taiwan, March 21 - 24, 2011},
  booktitle = {SAC},
  publisher = {ACM},
  year      = {2011},
  isbn      = {978-1-4503-0113-8},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{DesharnaisFernandes,
  author    = {Fernandes, T. and
               Desharnais, J.},
  title     = {Describing data flow analysis techniques with {K}leene algebra},
  journal   = {Sci. Comput. Program.},
  volume    = {65},
  number    = {2},
  year      = {2007},
  pages     = {173--194},
}

@article{DesharnaisMoellerStruth11,
  author    = {Desharnais, J. and
               M{\"o}ller, B. and
               Struth, G.},
  title     = {Algebraic Notions of Termination},
  journal   = {Logical Methods in Computer Science},
  volume    = {7},
  number    = {1},
  year      = {2011},
}

@article{DesharnaisMoellerStruthTermination,
	author		= "Desharnais, J. and M{\"o}ller, B. and Struth, G.",
	title		= "Algebraic Notions of Termination",
	journal		= "Logical Methods in Computer Science",
        volume          = "7",
        number          = "1:1",
        pages           = "1--29",
	year		= 2011
}

@article{DesharnaisStruth,
	author		= {Desharnais, J. and Struth, G.},
	title		= {Internal axioms for domain semirings},
	journal		= {Science of Computer Programming},
	volume		= 76,
	number		= 3,
	pages		= {181--203},
	year		= 2011,
}

@article{DoBaWo,
  author    = {Doornbos, H. and
               Backhouse, R. C. and
               van der Woude, J.},
  title     = {A Calculational Approach to Mathematical Induction},
  journal   = {Theor. Comput. Sci.},
  volume    = {179},
  number    = {1--2},
  year      = {1997},
  pages     = {103--135},
}

@inproceedings{EhmMoellerStruth,
  author    = {Ehm, T. and
               M{\"o}ller, B. and
               Struth, G.},
  title     = {Kleene Modules},
  booktitle = {RelMiCS},
  year      = {2003},
  pages     = {112--124},
  editor    = {Berghammer, R. and
               M{\"o}ller, B. and
               Struth, G.},
  series    = {LNCS},
  publisher = {Springer},
  volume    = {3051}
}

@InCollection{FosterStruth,
  author =       {Foster, S. and Struth, G.},
  title =        {Automated analysis of regular algebra},
  booktitle =    {IJCAR 2012},
  year =      2012,
pages     = {271--285},
editor    = {Gramlich, B. and
             Miller, D. and
             Sattler, U.},
publisher = {Springer},
  series    = {LNCS},
  volume    = {7364}}

@InProceedings{FosterStruthWeber,
	author		= {Foster, S. and Struth, G. and Weber, T.},
	title		= {Automated Engineering of Relational and Algebraic Methods in {Isabelle/HOL} -- (Invited Tutorial)},
        year      = {2011},
        pages     = {52--67},
	editor		= {de Swart, H.},
	booktitle	= {RAMiCS 2011},
  series =    {LNCS},
  publisher = {Springer},
volume    = {6663},
}



@article{Gammie,
  author    = {Gammie, P.},
  title     = {The Worker/Wrapper Transformation},
  journal   = {Archive of Formal Proofs},
  volume    = {2009},
  year      = {2009},
  ee        = {http://afp.sourceforge.net/entries/WorkerWrapper.shtml},
}


@inproceedings{GarillotGonthier,
  author    = {Garillot, F. and
               Gonthier, G. and
               Mahboubi, A. and
               Rideau, L.},
  editor    = {Berghofer, S. and
               Nipkow, T. and
               Urban, C. and
               Wenzel, M.},
  title     = {Packaging Mathematical Structures},
  booktitle = {TPHOLs 2009},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {5674},
  year      = {2009},
  pages     = {327--342},}

@inproceedings{Guttmann,
  author    = {Guttmann, W.},
  title     = {Partial, Total and General Correctness},
  editor    = {Bolduc, C. and
               Desharnais, J. and
               Ktari, B.},
  booktitle = {MPC 2010},
  year      = {2010},
  pages     = {157--177},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {6120},
}

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

@inproceedings{GuttmannStruthWeber2,
  author    = {Guttmann, W. and
               Struth, G. and
               Weber, T.},
  title     = {A Repository for {T}arski-{K}leene Algebras},
  booktitle = {ATE 2011},
  year      = 2011,
  pages     = {30--39},
  editor    = {H{\"o}fner, P. and
               McIver, A. and
               Struth, G.},
  publisher = {CEUR-WS.org},
  series    = {CEUR Workshop Proceedings},
  volume    = 760,
  year      = 2011,
}
}

@inproceedings{HaftmannWenzel,
  author    = {Haftmann, F. and
               Wenzel, M.},
  editor    = {Berardi, S. and
               Damiani, F. and
               de'Liguoro, U.},
  title     = {Local Theory Specifications in {I}sabelle/{I}sar},
  booktitle = {TYPES 2008},
  year      = {2008},
  pages     = {153--168},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {5497},
}

@article{HoareCKA,
  author    = {Hoare, T. and
               M{\"o}ller, B. and
               Struth, G. and
               Wehrman, I.},
  title     = {Concurrent {K}leene Algebra and its Foundations},
  journal   = {J. Log. Algebr. Program.},
  volume    = {80},
  number    = {6},
  year      = {2011},
  pages     = {266--296},
  ee        = {http://dx.doi.org/10.1016/j.jlap.2011.04.005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

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

@inproceedings{HoefnerStruthAuto,
  author    = {H{\"o}fner, P. and
               Struth, G.},
  title     = {Automated Reasoning in {K}leene Algebra},
  booktitle = {CADE},
  year      = {2007},
  pages     = {279--294},
  editor    = {Pfenning, F.},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {4603}
}

@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},
}

@Unpublished{IsabelleRepository,
	author		= {Struth, G. and others},
	title		= {Isabelle Algebraic Methods Repository},
	year		= 2011,
	note		= {\url{http://www.dcs.shef.ac.uk/~georg/isa}}
}

@inproceedings{Kaliszyk,
  author    = {Kaliszyk, C. and
               Urban, C.},
  title     = {{Q}uotients revisited for {I}sabelle/{HOL}},
  booktitle = {SAC},
  year      = {2011},
  pages     = {1639--1644},
  editor    = {Chu, W.~C. and
               Wong, W.~E. and
               Palakal, M.~J. and
               Hung, C-C.},
  publisher = {ACM}
}

@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}
}

@article{Kozen00,
  author    = {Kozen, D.},
  title     = {On Hoare logic and Kleene algebra with tests},
  journal   = {ACM Trans. Comput. Log.},
  volume    = {1},
  number    = {1},
  year      = {2000},
  pages     = {60--76},
  ee        = {http://doi.acm.org/10.1145/343369.343378},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{Kozen90,
  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{Kozen97,
  author    = {Kozen, D.},
  title     = {Kleene Algebra with Tests},
  journal   = {ACM Trans. Program. Lang. Syst.},
  volume    = {19},
  number    = {3},
  year      = {1997},
  pages     = {427--443}
}

@inproceedings{KozenComplete,
  author    = {Kozen, D.},
  title     = {On {K}leene Algebras and Closed Semirings},
  year      = {1990},
  pages     = {26--47},
  editor    = {Rovan, B.},
 booktitle     = {Mathematical Foundations of Computer Science 1990},
 publisher = {Springer},
  series    = {LNCS},
  volume    = {452}
}

@inproceedings{KozenPatron,
  author    = {Kozen, D. and
               Patron, M.-C.},
  title     = {Certification of Compiler Optimizations Using {K}leene Algebra
               with Tests},
  booktitle = {Computational Logic},
  year      = {2000},
  pages     = {568--582},
   editor    = {Lloyd, J. D. and
               Dahl, V. and
               Furbach, U. and
               Kerber, M. and
               Lau, K.-K. and
               Palamidessi, C. and
               Moniz Pereira, L. and
               Sagiv, Y. and
               Stuckey, P. J.},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {1861},
}
}



@TechReport{KozenTyped,
  author = 	 {Kozen, D.},
  title = 	 {Typed {K}leene algebra},
  institution =  {Computer Science Department, Cornell University, USA},
  year = 	 1998,
  number = 	 {TR98-1669}}

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

@Unpublished{LaurenceStruth,
  author = 	 {Laurence, M. R. and Struth, G.},
  title = 	 {On Completeness of Omega Modules and Omega Algebras},
 year = 	 2010,
  note = 	 {(Forthcoming)},
}

@article{Leiss,
  author    = {Lei{\ss}, H.},
  title     = {Kleene modules and linear languages},
  journal   = {J. Log. Algebr. Program.},
  volume    = {66},
  number    = {2},
  year      = {2006},
  pages     = {185--194},
  ee        = {http://dx.doi.org/10.1016/j.jlap.2005.04.004},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@book{Manna,
  title={Mathematical theory of computation},
  author={Manna, Z.},
  year={1974},
  publisher={McGraw-Hill}
}

@Article{Milner,
  author =       {Milner, R.},
  title =        {A Complete Inference System for a Class of Regular Behaviours},
  journal =      {J. Computer and System Sciences},
  year =         1982,
  volume =    28,
  pages =     {439--466},
}

@article{MoellerStruth,
  author    = {M{\"o}ller, B. and
               Struth, G.},
  title     = {Algebras of modal operators and partial correctness},
  journal   = {Theor. Comput. Sci.},
  volume    = {351},
  number    = {2},
  year      = {2006},
  pages     = {221--239},
}

@article{Nipkow98,
  author    = {Nipkow, T.},
  title     = {Winskel is (almost) Right: Towards a Mechanized Semantics},
  journal   = {Formal Asp. Comput.},
  volume    = {10},
  number    = {2},
  year      = {1998},
  pages     = {171--186},
  ee        = {http://dx.doi.org/10.1007/s001650050009},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Article{NipkowKrauss,
  author =       {Krauss, A. and Nipkow, T.},
  title =        {Proof Pearl: Regular Expression Equivalence and Relation Algebra},
  journal =      {J. Automated Reasoning},
volume    = {49},
  number    = {1},
  year =         {2012},
pages     = {95--106}
}

@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,
}

@InCollection{Pin,
  author = 	 {Pin, J.-E.},
  title = 	 {Syntactic Semigroups},
  booktitle = 	 {Handbook of Formal Language Theory},
  pages = 	 {679--746},
  publisher = {Springer},
  year = 	 1997,
  editor = 	 {Rozenberg, G. and Salomaa, A.},
  volume = 	 1}



@inproceedings{Pratt,
  author    = {Pratt, V.~R.},
  title     = {Action Logic and Pure Induction},
  booktitle = {JELIA '90},
  year      = {1990},
  editor    = {van Eijck, J.},
  pages     = {97--120},
  publisher = {Springer},
  series    = {LNCS},
  volume    = {478},
}

@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},
}

@phdthesis{Schirmer,
  author    = {Schirmer, N.},
  title     = {Verification of sequential imperative programs in Isabelle-HOL},
  year      = {2006},
  pages     = {1--249},
  ee        = {http://mediatum.ub.tum.de/mediatum/servlets/TUMDistributionServlet?id=mediaTUM_derivate_000000000002972},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{Struth,
title = "Abstract abstract reduction",
journal = "J. Logic and Algebraic Programming",
volume = 66,
number = 2,
pages = "239--270",
year = 2006,
author = "Struth, G.",
}

@Article{Struth08,
  author = 	 {Struth, G.},
  title = 	 {Modal Tools for Separation and Refinement},
  journal = 	 {Electronic Notes in Theoretical Computer Science},
  year = 	 2008,
  volume = 	 214,
  pages = 	 {81--101}}


@Article{StruthJLAP,
  author =       {Struth, G.},
  title =        {Left omega algebras and regular equations},
  journal =      {J. Logic and Algebraic Programming},
  year =         2012,
  note =      {(In press)}}

@inproceedings{Urban,
  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},
  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},
}

@article{Wagner,
  author    = {Wagner, K. W.},
  title     = {Eine {A}xiomatisierung der {T}heorie der regul{\"a}ren {F}olgenmengen},
  journal   = {Elektronische Informationsverarbeitung und Kybernetik},
  volume    = 12,
  number    = 7,
  year      = 1976,
  pages     = {337--354},
}


@inproceedings{Wilke,
  author    = {Wilke, T.},
  title     = {An {E}ilenberg Theorem for Infinity-Languages},
  editor    = {Leach Albert, J. and
               Monien, B. and
               Rodr\'{\i}guez-Artalejo, M.},
 booktitle = {ICALP91},
  year      = 1991,
  pages     = {588--599},
 publisher = {Springer},
  series    = {LNCS},
  volume    = 510,
}

@article{vonWright,
  author    = {von Wright, J.},
  title     = {Towards a refinement algebra},
  journal   = {Science of Computer Programming},
  volume    = {51},
  number    = {1-2},
  year      = {2004},
  pages     = {23--45},
}

@inproceedings{Nanevski,
  author    = {Nanevski, A. and
               Morrisett, G. and
               Shinnar, A. and
               Govereau, P. and
               Birkedal, L.},
  title     = {Ynot: Dependent types for imperative programs},
  booktitle = {ICFP},
  year      = {2008},
  pages     = {229-240},
  editor    = {Hook, J. and Thiemann, P.}
  publisher = {ACM}
}