@(BackboneJSURL,
 title        = {Backbone.js: a JavaScript library with a RESTful JSON interface},
 url          = {http://backbonejs.org/},
)
@(PlayFrameworkURL,
 title        = {Play: an open source MVC web application framework},
 url          = {http://www.playframework.com/},
)
@(TypescriptURL,
 title        = {TypeScript: a language for application-scale JavaScript development, http://www.typescriptlang.org/},
 url          = {http://www.typescriptlang.org/},
)
@inproceedings(alur-fmcad13,
 author       = {Rajeev Alur and Rastislav Bodik and Garvit Juniwal and Milo M. K. Martin and Mukund Raghothaman and Sanjit A. Seshia and Rishabh Singh and Solar-Lezama, Armando and Emina Torlak and Abhishek Udupa},
 year         = {2013},
 title        = {Syntax-Guided Synthesis},
 booktitle    = {Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD)},
 doi          = {10.1109/FMCAD.2013.6679385},
)
@article(back1997structured,
 author       = {Ralph Back and Jim Grundy and Von Wright, Joakim},
 year         = {1997},
 title        = {Structured Calculational Proof},
 journal      = {Formal Aspects of Computing},
 volume       = {9},
 number       = {5-6},
 pages        = {469--483},
 doi          = {10.1007/BF01211456},
)
@inproceedings(backhouse2006exercises,
 author       = {Roland Backhouse and Diethard Michaelis},
 year         = {2006},
 title        = {Exercises in quantifier manipulation},
 booktitle    = {Mathematics of program construction},
 organization = {Springer},
 pages        = {69--81},
 doi          = {10.1007/11783596\_7},
)
@techreport(bertot1997implementing,
 author       = {Yves Bertot and Kleymann-Schreiber, Thomas and Dilip Sequeira},
 year         = {1997},
 title        = {Implementing Proof by Pointing without a Structure Editor},
 type         = {Technical Report},
 number       = {ECS-LFCS-97-368},
 institution  = {University of Edinburgh},
 url          = {http://www.inria.fr/RRRT/RR-3286.html},
)
@incollection(bornat1997jape,
 author       = {Richard Bornat and Bernard Sufrin},
 year         = {1997},
 title        = {Jape: A calculator for animating proof-on-paper},
 booktitle    = {Automated Deduction—CADE-14},
 publisher    = {Springer},
 pages        = {412--415},
 doi          = {10.1007/3-540-63104-6\_41},
)
@inproceedings(butlerProgram1996,
 author       = {Michael Butler and L{\r a}ngbacka, Thomas},
 year         = {1996},
 title        = {Program Derivation Using the Refinement Calculator},
 booktitle    = {Theorem Proving in Higher Order Logics: 9th International Conference, volume 1125 of LNCS},
 publisher    = {Springer Verlag},
 pages        = {93--108},
 doi          = {10.1007/BFb0105399},
)
@techreport(carringtonTool1996,
 author       = {David Carrington and Ian Hayes and Ray Nickson and G. N. Watson and Jim Welsh},
 year         = {1996},
 title        = {A Tool for Developing Correct Programs by Refinement},
 type         = {Technical Report},
 url          = {http://espace.library.uq.edu.au/view/UQ:10768},
)
@incollection(ChaudhariDamaniIFM14,
 author       = {Dipak L. Chaudhari and Om Damani},
 year         = {2014},
 title        = {Automated Theorem Prover Assisted Program Calculations},
 editor       = {Elvira Albert and Emil Sekerinski},
 booktitle    = {Integrated Formal Methods},
 series       = {Lecture Notes in Computer Science},
 publisher    = {Springer International Publishing},
 pages        = {205--220},
 doi          = {10.1007/978-3-319-10181-1\_13},
)
@incollection(ChaudhariDamaniITICSE15,
 author       = {Dipak L. Chaudhari and Om Damani},
 year         = {2015},
 title        = {Introducing Formal Methods via Program Derivation},
 booktitle    = {Innovation and Technology in Computer Science Education, ITiCSE 15},
)
@incollection(cohen2009vcc,
 author       = {Ernie Cohen and Markus Dahlweid and Mark Hillebrand and Dirk Leinenbach and Micha{\l} Moskal and Thomas Santen and Wolfram Schulte and Stephan Tobies},
 year         = {2009},
 title        = {VCC: A Practical System for Verifying Concurrent C},
 booktitle    = {Theorem Proving in Higher Order Logics},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-03359-9\_2},
)
@article(dijkstraGuarded1975,
 author       = {Edsger W. Dijkstra},
 year         = {1975},
 title        = {Guarded Commands, Nondeterminacy and Formal Derivation of Programs},
 journal      = {Commun. {ACM}},
 volume       = {18},
 number       = {8},
 pages        = {453--457},
 doi          = {10.1145/360933.360975},
)
@book(dijMethod1988,
 author       = {Edsger W. Dijkstra and W. H. Feijen},
 year         = {1988},
 title        = {A Method of Programming},
 publisher    = {Addison-Wesley Longman Publishing Co., Inc.},
 address      = {Boston, {MA}, {USA}},
)
@inproceedings(filliatre:hal-00789533,
 author       = {Jean-Christophe Filli{\^a}tre and Andrei Paskevich},
 year         = {2013},
 title        = {{Why3 -- Where Programs Meet Provers}},
 booktitle    = {{ESOP'13 22nd European Symposium on Programming}},
 series       = {LNCS},
 volume       = {7792},
 publisher    = {Springer},
 address      = {Rome, Italie},
 doi          = {10.1007/978-3-642-37036-6\_8},
)
@inproceedings(franssen1999cocktail,
 author       = {Michael Franssen},
 year         = {1999},
 title        = {Cocktail: A tool for deriving correct programs},
 booktitle    = {Workshop on Automated Reasoning},
)
@techreport(VerifastJacobsPiessens08,
 author       = {Bart Jacobs and Frank Piessens},
 year         = {2008},
 title        = {The {VeriFast} Program Verifier},
 type         = {Technical Report},
 number       = {CW-520},
 institution  = {Dept. of Computer Science, Katholieke Universiteit Leuven},
 url          = {http://www.cs.kuleuven.be/~bartj/verifast/verifast.pdf},
)
@book(kalProg1990,
 author       = {Anne Kaldewaij},
 year         = {1990},
 title        = {Programming: The Derivation of Algorithms},
 publisher    = {Prentice-Hall, Inc.},
 address      = {{NJ}, {USA}},
)
@inproceedings(leino2010dafny,
 author       = {K. Rustan M. Leino},
 year         = {2010},
 title        = {Dafny: An Automatic Program Verifier for Functional Correctness},
 booktitle    = {Logic for Programming, Artificial Intelligence, and Reasoning},
 organization = {Springer},
 doi          = {10.1007/978-3-642-17511-4\_20},
)
@incollection(LeinoDirection,
 author       = {K. Rustan M. Leino},
 year         = {2011},
 title        = {Tools and Behavioral Abstraction: A Direction for Software Engineering},
 editor       = {Sebastian Nanz},
 booktitle    = {The Future of Software Engineering},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {115--124},
 doi          = {10.1007/978-3-642-15187-3\_7},
)
@inproceedings(oliveira2004refine,
 author       = {Marcel Oliveira and Manuela Xavier and Ana Cavalcanti},
 year         = {2004},
 title        = {Refine and Gabriel: support for refinement and tactics},
 booktitle    = {Software Engineering and Formal Methods, 2004. SEFM 2004. Proceedings of the Second International Conference on},
 organization = {IEEE},
 pages        = {310--319},
 doi          = {10.1109/SEFM.2004.1347535},
)
@incollection(kiama,
 author       = {Anthony M. Sloane},
 year         = {2011},
 title        = {Lightweight Language Processing in Kiama},
 editor       = {JoãoM. Fernandes and Ralf Lämmel and Joost Visser and João Saraiva},
 booktitle    = {Generative and Transformational Techniques in Software Engineering III},
 series       = {Lecture Notes in Computer Science},
 volume       = {6491},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {408--425},
 doi          = {10.1007/978-3-642-18023-1\_12},
)
@incollection(SmithGenProg,
 author       = {Douglas R. Smith},
 year         = {2008},
 title        = {Generating Programs Plus Proofs by Refinement},
 editor       = {Bertrand Meyer and Jim Woodcock},
 booktitle    = {Verified Software: Theories, Tools, Experiments},
 series       = {Lecture Notes in Computer Science},
 volume       = {4171},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {182--188},
 doi          = {10.1007/978-3-540-69149-5\_20},
)