@article {birkhoff:1942,
    AUTHOR = {Birkhoff, Garrett},
     TITLE = {Lattice, ordered groups},
   JOURNAL = {Ann. of Math. (2)},
  FJOURNAL = {Annals of Mathematics. Second Series},
    VOLUME = {43},
      YEAR = {1942},
     PAGES = {298--331},
      ISSN = {0003-486X},
   MRCLASS = {20.0X},
  MRNUMBER = {0006550 (4,3f)},
MRREVIEWER = {H. Wallman},
}

@article {bergmann:1929,
   author = {Bergmann, Gustav},
   affiliation = {Wien Wien},
   title = {Zur Axiomatik der Elementargeometrie},
   journal = {Monatshefte f\"ur Mathematik},
   publisher = {Springer Wien},
   issn = {0026-9255},
   keyword = {Mathematics and Statistics},
   pages = {269-284},
   volume = {36},
   issue = {1},
   url = {https://doi.org/10.1007/BF02307616},
   note = {10.1007/BF02307616},
   year = {1929}
}

@book {birkhoff:1967,
    AUTHOR = {Birkhoff, Garrett},
     TITLE = {Lattice theory},
    SERIES = {Third edition. American Mathematical Society Colloquium
              Publications, Vol. XXV},
 PUBLISHER = {American Mathematical Society},
   ADDRESS = {Providence, R.I.},
      YEAR = {1967},
     PAGES = {vi+418},
   MRCLASS = {06.30},
  MRNUMBER = {0227053 (37 \#2638)},
MRREVIEWER = {P. A. Fillmore},
}

@book {burris:sankappanavar:1981,
    AUTHOR = {Burris, Stanley and Sankappanavar, H. P.},
     TITLE = {A course in universal algebra},
    SERIES = {Graduate Texts in Mathematics},
    VOLUME = {78},
 PUBLISHER = {Springer-Verlag},
   ADDRESS = {New York},
      YEAR = {1981},
     PAGES = {xvi+276},
      ISBN = {0-387-90578-2},
   MRCLASS = {08-01},
  MRNUMBER = {648287 (83k:08001)},
MRREVIEWER = {R. S. Pierce},
}


@article{georgescu:leustean:preoteasa:2005,
  title = "Pseudo-hoops",
  journal = "Journal of Multiple-Valued Logic and Soft Computing",
  volume = "11",
  number = "1-2",
  pages = "153 - 184",
  year = "2005",
  author = "Georgescu, George and Leu\c s tean, Lauren\c tiu and Viorel Preoteasa",
}


@article{preoteasa:back:2009,
title = "Data Refinement of Invariant Based Programs",
journal = "Electronic Notes in Theoretical Computer Science",
volume = "259",
number = "",
pages = "143 - 163",
year = "2009",
note = "Proceedings of the 14th BCS-FACS Refinement Workshop (REFINE 2009)",
issn = "1571-0661",
doi = "DOI: 10.1016/j.entcs.2009.12.022",
url = "http://www.sciencedirect.com/science/article/B75H1-4XYHXFB-B/2/27ba4be3ad580ef9b5a8b4a20a42d8ca",
author = "Viorel Preoteasa and Ralph-Johan Back",
keywords = "Invariant based programming",
keywords = "Data refinement",
keywords = "Mechanical verification"
}

@inproceedings{nipkow:2002,
 author = {Tobias Nipkow},
 title = {Hoare Logics for Recursive Procedures and Unbounded Nondeterminism},
 booktitle = {CSL '02: Proceedings of the 16th International Workshop and 11th Annual Conference of the EACSL on Computer Science Logic},
 year = {2002},
 isbn = {3-540-44240-5},
 pages = {103--119},
 publisher = {Springer-Verlag},
 address = {London, UK},
 }


@article{schorr:waite:1967,
 author = {H. Schorr and W. M. Waite},
 title = {An efficient machine-independent procedure for garbage collection in various list structures},
 journal = {Commun. ACM},
 volume = {10},
 number = {8},
 year = {1967},
 issn = {0001-0782},
 pages = {501--506},
 doi = {http://doi.acm.org/10.1145/363534.363554},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@book{knuth:1997,
 author = {Donald E. Knuth},
 title = {The art of computer programming, volume 1 (3rd ed.): fundamental algorithms},
 year = {1997},
 isbn = {0-201-89683-4},
 publisher = {Addison Wesley Longman Publishing Co., Inc.},
 address = {Redwood City, CA, USA},
 }

@techreport{back:preoteasa:2008,
author="Ralph-Johan Back and Viorel Preoteasa",
title="Semantics and Proof Rules of Invariant Based Programs",
language="none",
number="903",
year="2008",
month="Jul",
address="",
note="",
keywords="Invariant based programming. Semantics. Hoare proof rules. Completeness",
series="",
organisation="",
ISBN="978-952-12-2111-8",
institution="{TUCS}"
}

@article{aBack08,
	Author = {Ralph-Johan Back},
	Date-Added = {2008-07-05 14:58:33 +0300},
	Date-Modified = {2008-08-05 17:58:06 +0300},
	Journal = {Formal Aspects of Computing},
	Title = {Invariant Based Programming: Basic approach and Teaching Experience},
	Year = {2008}
}

@INPROCEEDINGS{Back83:invariants,
  author = {Ralph-Johan Back},
  title = {Invariant Based Programs and Their Correctness},
  booktitle = {Automatic Program Construction Techniques },
  year = {1983},
  editor = {Biermann, W. and Guiho, G and Kodratoff, Y},
  pages = {223--242},
  publisher = {MacMillan Publishing Company},
  pdf = {http://crest.abo.fi/publications/public/1983/InvariantBasedProgramsAndTheirCorrectnessP.pdf},
  project = {methods verification},
}

@INPROCEEDINGS{Back80:invariants,
  author = {Ralph-Johan Back},
  title = {Semantic Correctness of Invariant Based Programs},
  booktitle = {International Workshop on Program Construction},
  year = {1980},
  address = {Chateau de Bonas, France},
  pdf = {http://crest.abo.fi/publications/public/1980/SemanticCorrectnessOfInvariantBasedProgramsP.pdf},
  project = {methods verification},
}
