aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx/biblio.bib
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx/biblio.bib')
-rw-r--r--doc/sphinx/biblio.bib32
1 files changed, 22 insertions, 10 deletions
diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib
index 3e988709c..3574bf675 100644
--- a/doc/sphinx/biblio.bib
+++ b/doc/sphinx/biblio.bib
@@ -3,6 +3,21 @@
@String{lnai = "Lecture Notes in Artificial Intelligence"}
@String{SV = "{Sprin-ger-Verlag}"}
+@InCollection{Asp00,
+ Title = {Proof General: A Generic Tool for Proof Development},
+ Author = {Aspinall, David},
+ Booktitle = {Tools and Algorithms for the Construction and
+ Analysis of Systems, {TACAS} 2000},
+ Publisher = {Springer Berlin Heidelberg},
+ Year = {2000},
+ Editor = {Graf, Susanne and Schwartzbach, Michael},
+ Pages = {38--43},
+ Series = {Lecture Notes in Computer Science},
+ Volume = {1785},
+ Doi = {10.1007/3-540-46419-0_3},
+ ISBN = {978-3-540-67282-1},
+}
+
@Book{Bar81,
author = {H.P. Barendregt},
publisher = {North-Holland},
@@ -290,16 +305,13 @@ the Calculus of Inductive Constructions}},
year = {1995}
}
-@Misc{Pcoq,
- author = {Lemme Team},
- title = {Pcoq a graphical user-interface for {Coq}},
- note = {\url{http://www-sop.inria.fr/lemme/pcoq/}}
-}
-
-@Misc{ProofGeneral,
- author = {David Aspinall},
- title = {Proof General},
- note = {\url{https://proofgeneral.github.io/}}
+@InProceedings{Pit16,
+ Title = {Company-Coq: Taking Proof General one step closer to a real IDE},
+ Author = {Pit-Claudel, Clément and Courtieu, Pierre},
+ Booktitle = {CoqPL'16: The Second International Workshop on Coq for PL},
+ Year = {2016},
+ Month = jan,
+ Doi = {10.5281/zenodo.44331},
}
@Book{RC95,