Commit 53d6057e authored by POTTIER Francois's avatar POTTIER Francois

Bibliography update. No months.

Added links to CompCert's github repository.
parent ceed3a3a
This source diff could not be displayed because it is too large. You can view the blob instead.
@Misc{compcert-github,
author = "Xavier Leroy",
title = "The {CompCert C} verified compiler",
year = "2014",
howpublished = "\url{https://github.com/AbsInt/CompCert}",
}
......@@ -4,6 +4,7 @@
\usepackage{amstext}
\usepackage[T1]{fontenc}
\usepackage[latin1]{inputenc}
\usepackage{moreverb}
\usepackage{tikz}
\usepackage{xspace}
\usepackage{mymacros}
......@@ -2071,8 +2072,9 @@ named \verb+unambiguous+.
% correspond bien à la fin du Stream.
The parsers produced by \menhir's Coq back-end must be linked with a Coq
library, which can be found in the CompCert tree~\cite{compcert}, in the
\verb+cparser/validator+ subdirectory. Additionally, CompCert can be used as
library, which can be found in the CompCert tree~\cite{compcert,compcert-github}, in the
\href{https://github.com/AbsInt/CompCert/tree/master/cparser/validator}
{\texttt{cparser/validator}} subdirectory. Additionally, CompCert can be used as
an example if one wishes to use \menhir to generate a formally verified parser
as part of some other project.
......@@ -2089,6 +2091,7 @@ Extract Constant Int31.compare31 => "Camlcoq.Int31.compare".
Extract Constant Int31.On => "0".
Extract Constant Int31.In => "1".
\end{comment}
% Peut-être en faire aussi un fichier de librairie?
% ---------------------------------------------------------------------------------------------------------------------
......@@ -2291,7 +2294,7 @@ Coq proofs that come with it.
% Bibliography.
\bibliographystyle{plain}
\bibliography{english}
\bibliography{english,local}
\end{document}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment