Commit 6b059d9c authored by POTTIER Francois's avatar POTTIER Francois

Added a citation of CompCert.

parent 4b46e509
......@@ -2919,6 +2919,17 @@
URL = "http://www.ccs.neu.edu/scheme/pubs/esop2003-cf.ps.gz",
}
@InProceedings{clochard-marche-paskevich-14,
author = "Martin Clochard and Claude March{\'{e}} and Andrei
Paskevich",
title = "Verified programs with binders",
booktitle = plpv,
pages = "29--40",
month = jan,
year = "2014",
URL = "https://hal.inria.fr/hal-00913431",
}
@Article{cohen-search-06,
author = "Albert Cohen and Sébastien Donadio and Maria-Jesus
Garzaran and Christoph Herrmann and Oleg Kiselyov and
......@@ -7567,6 +7578,15 @@
URL = "http://gallium.inria.fr/~xleroy/publi/compiler-certif.pdf",
}
@Misc{compcert,
author = "Xavier Leroy",
title = "The {CompCert} verified compiler, software and
commented proof",
month = sep,
year = "2014",
howpublished = "\url{http://compcert.inria.fr/}",
}
@TechReport{leroy-phd-92,
author = "Xavier Leroy",
title = "Polymorphic typing of an algorithmic language",
......
......@@ -1914,13 +1914,18 @@ in the near future.
\section{Coq back-end}
\label{sec:coq}
Using the Coq proof assistant, \menhir is able to generate formally
verified parsers~\cite{jourdan-leroy-pottier-12}: when used with the
\ocoq option, menhir shall be given a \texttt{.vy}, and will generate
a \texttt{.v} file. This file contains both a description of the
grammar and semantic actions in the Coq language. \texttt{.vy} files
use the same syntax as \texttt{.mly} files. There are however, several
additional restrictions:
Using the Coq proof assistant, \menhir is able to generate formally verified
parsers~\cite{jourdan-leroy-pottier-12}. This feature is has been used to
produce a certified parser for the CompCert certified C
compiler~\cite{compcert}.
When used with the
\ocoq option, menhir expects a file whose name ends in \texttt{.vy}, and generates
a \texttt{.v} file. Like an \texttt{.mly} file, a \texttt{.vy} file a grammar
specification, with embedded semantic actions. The difference is that the
semantic actions in a \texttt{.vy} file are expressed in Coq instead
of \ocaml. \texttt{.vy} files use the same syntax as \texttt{.mly}
files. There are however, several additional restrictions:
\begin{itemize}
\item Error handling is not supported: thus, the use of
......@@ -1989,7 +1994,7 @@ function. Two theorems are provided, \verb+entry_point_correct+ and
\verb+entry_point_complete+.
Parsers generated with the Coq back-end need to be compiled with
libraries: those can be found in the CompCert tree, under the
libraries: those can be found in the CompCert tree~\cite{compcert}, under the
\verb+cparser/validator+ subdirectory. Additionnally, CompCert can be
used as an example if one wants to use menhir to generate formally
verified parsers in another project.
......
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