%--------------------------

@INPROCEEDINGS{sortMorp,
    author = {Lex Augusteijn},
    title = {Sorting Morphisms},
    booktitle = {3rd International Summer School on Advanced Functional Programming, volume 1608 of LNCS},
    year = {1998},
    pages = {1--27},
    publisher = {Springer-Verlag}
}

%--------------------------


@article{meritt, 
 author = {Merritt, Susan M.},
 title = {An inverted taxonomy of sorting algorithms},
 journal = {Commun. ACM},
 issue_date = {Jan. 1985},
 volume = {28},
 number = {1},
 month = jan,
 year = {1985},
 issn = {0001-0782},
 pages = {96--99},
 numpages = {4},
 url = {http://doi.acm.org/10.1145/2465.214925},
 doi = {10.1145/2465.214925},
 acmid = {214925},
 publisher = {ACM},
 address = {New York, NY, USA},
} 

%--------------------------

@article{dps,
 author = {Nguyen, Dung ``Zung'' and Wong, Stephen B.},
 title = {Design patterns for sorting},
 journal = {SIGCSE Bull.},
 issue_date = {March 2001},
 volume = {33},
 number = {1},
 month = feb,
 year = {2001},
 issn = {0097-8418},
 pages = {263--267},
 numpages = {5},
 url = {http://doi.acm.org/10.1145/366413.364597},
 doi = {10.1145/366413.364597},
 acmid = {364597},
 publisher = {ACM},
 address = {New York, NY, USA},
} 

%--------------------------

@inproceedings{arrays,
 author = {Bradley, Aaron R. and Manna, Zohar and Sipma, Henny B.},
 title = {What's decidable about arrays?},
 booktitle = {Proceedings of the 7th international conference on Verification, Model Checking, and Abstract Interpretation},
 series = {VMCAI'06},
 year = {2006},
 isbn = {3-540-31139-4, 978-3-540-31139-3},
 location = {Charleston, SC},
 pages = {427--442},
 numpages = {16},
 url = {https://doi.org/10.1007/11609773_28},
 doi = {10.1007/11609773_28},
 acmid = {2146256},
 publisher = {Springer-Verlag},
 address = {Berlin, Heidelberg},
} 

%--------------------------

@MISC{codegeneration,
    author = {Florian Haftmann and Lukas Bulwahn},
    title = {Code generation from Isabelle/HOL theories},
    year = {2007}
}

%--------------------------

@INPROCEEDINGS{socos,
    author = {Ralph-johan Back and Johannes Eriksson and Magnus Myreen},
    title = {Verifying invariant based programs in the SOCOS environment},
    booktitle = {In Teaching Formal Methods: Practice and Experience (BCS Electronic Workshops in Computing). BCS-FACS},
    year = {2006}
}

%--------------------------

@techreport{spsa,
inhal = {no},
domainehal = {INFO:INFO_SE, INFO:INFO_MO},
equipe = {vesontio},
classement = {*},
author = {Tushkanova, Elena and Giorgetti, Alain and Kouchnarenko, Olga},
institution = {LIFC - Laboratoire d'Informatique de l'Universit\'{e} de Franche-Comt\'{e}},
title = {{S}pecifying and {P}roving a {S}orting {A}lgorithm},
note = {35 pages},
number = {RR2009-03},
type = {Research Report},
pdf = {/~publis/papers/pub/2009/RR2009-03.pdf},
month = oct,
year = 2009,
}

%--------------------------

@INPROCEEDINGS{krakatoa,
    author = {Jean-christophe Filliâtre and Claude Marché},
    title = {The Why/Krakatoa/Caduceus platform for deductive program verification},
    booktitle = {In CAV ’07},
    year = {2007},
    pages = {173--177}
}

%--------------------------

@inproceedings{LSDtrip,
  title={Teaching semantics with a proof assistant: No more LSD trip proofs},
  author={Nipkow, Tobias},
  booktitle={Verification, Model Checking, and Abstract Interpretation},
  pages={24--38},
  year={2012},
  organization={Springer}
}

%--------------------------

@article{back2011correct,
  title={Correct-by-construction programming in the Socos environment},
  author={Back, Ralph-Johan and Eriksson, Johannes},
  journal={CTP Components for Educational Software},
  pages={16},
  year={2011}
}






