Commit 83fc6d59 authored by POTTIER Francois's avatar POTTIER Francois

Cite Jourdan and Pottier (2017) in the manual.

parent f268a31a
......@@ -226,3 +226,16 @@
pages = "606--611",
URL = "",
author = "Jacques-Henri Jourdan and François Pottier",
title = "A simple, possibly correct {LR} parser for {C11}",
journal = "ACM Transactions on Programming Languages and
month = aug,
year = "2017",
volume = "39",
number = "4",
pages = "14:1--14:36",
URL = "",
......@@ -4249,7 +4249,10 @@ not at the time offer generalized algebraic data types (GADTs). Today, \ocaml
has GADTs, but, as the saying goes, ``if it ain't broken, don't fix it''.
The main ideas behind the Coq back-end are described in a paper by Jourdan,
Pottier and Leroy~\cite{jourdan-leroy-pottier-12}.
Pottier and Leroy~\cite{jourdan-leroy-pottier-12}. The C11 parser in the
CompCert compiler~\cite{compcert} is constructed by Menhir and verified by
Coq, following this technique. How to construct a correct C11 parser using
Menhir is described by Jourdan and Pottier~\cite{jourdan-pottier-17}.
The approach to error reports presented in \sref{sec:errors:new} was
proposed by Jeffery~\cite{jeffery-03} and further explored by
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