From fca241c91ba0f27d145bf083a283491844da1da1 Mon Sep 17 00:00:00 2001
From: "Richard L. Ford" <richford@microsoft.com>
Date: Wed, 27 Jan 2016 21:35:30 -0800
Subject: Add Dafny reference manual

This version is still a draft, but is mostly complete and
about half reviewed. The manual is written using
Madoko. The sources are in the Docs/DafnyRef directory.
The processed sources are available in the
Docs/DafnyRef/out directory in the form of a single
HTML page or as a PDF.
---
 Docs/DafnyRef/DafnyRef.bib | 48 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 48 insertions(+)
 create mode 100644 Docs/DafnyRef/DafnyRef.bib

(limited to 'Docs/DafnyRef/DafnyRef.bib')

diff --git a/Docs/DafnyRef/DafnyRef.bib b/Docs/DafnyRef/DafnyRef.bib
new file mode 100644
index 00000000..9a2a5a5b
--- /dev/null
+++ b/Docs/DafnyRef/DafnyRef.bib
@@ -0,0 +1,48 @@
+@Misc{Rise4fun:dafny,
+  author = {K. Rustan  M. Leino},
+  title = {Try Dafny In Your Browser},
+  note = "Available at \url{http://rise4fun.com/Dafny}"
+}
+@Misc{MSR:dafny:main,
+  author = {K. Rustan  M. Leino},
+  title = {Main Microsoft Research Dafny Web page},
+  note = "Available at \url{http://research.microsoft.com/en-us/projects/dafny}"
+}
+@Misc{MSR:dafny:source,
+  author = {K. Rustan  M. Leino et al},
+  title = {Dafny Source Code},
+  note = "Available at \url{http://dafny.codeplex.com}"
+}
+@Misc{MSR:dafny:quickref,
+  author = {K. Rustan  M. Leino},
+  title = {Dafny Quick Reference},
+  note = "Available at \url{http://research.microsoft.com/en-us/projects/dafny/reference.aspx}"
+}
+@Misc{Linz:Coco,
+  author = {Hanspeter M{\"{o}}ssenb{\"{o}}ck and Markus L{\"{o}}berbauer and Albrecht W{\"{o}}{\ss}},
+  title = {The Compiler Generator Coco/R},
+  howpublished = {Open source from University of Linz},
+  year = 2013,
+  note = "Available at \url{http://www.ssw.uni-linz.ac.at/Research/Projects/Coco/}"
+}
+@Misc{LEINO:Dafny:Calc,
+  author = {K. Rustan M. Leino and Nadia Polikarpova},
+  title = {Verified Calculations},
+  howpublished = {Manuscript KRML 231},
+  year = 2013,
+  note = "Available at \url{http://research.microsoft.com/en-us/um/people/leino/papers/krml231.pdf}"
+}
+@Misc{LEINO:Dafny:Coinduction,
+  author = {K. Rustan M. Leino and Michal Moskal},
+  title = {Co-induction Simply: Automatic Co-inductive Proofs in a Program Verifier},
+  howpublished = {Manuscript KRML 230},
+  year = 2014,
+  note = "Available at \url{http://research.microsoft.com/en-us/um/people/leino/papers/krml230.pdf}" 
+}
+@Misc{LEINO:Dafny:DynamicFrames,
+  author = {K. Rustan M. Leino},
+  title = {Dynamic-frame specifications in Dafny},
+  howpublished = {JML seminar, Dagstuhl, Germany},
+  year = 2009,
+  note = "Available at \url{http://research.microsoft.com/en-us/um/people/leino/papers/dafny-jml-dagstuhl-2009.pptx}"
+}
-- 
cgit v1.2.3