Validating LR(1) Parsers
Jacques-Henri Jourdan1,2 , François Pottier2 , and Xavier Leroy212École Normale Supérieure
INRIA Paris-Rocquencourt

Abstract. An LR(1) parser is a ﬁnite-state automaton, equipped witha stack, which uses a combination of its current state and one lookahead
symbol in order to determine which action to perform next. We present
a validator which, when applied to a context-free grammar G and an
automaton A, checks that A and G agree. Validating the parser provides the correctness guarantees required by veriﬁed compilers and otherhigh-assurance software that involves parsing. The validation process is
independent of which technique was used to construct A. The validator
is implemented and proved correct using the Coq proof assistant. As anapplication, we build a formally-veriﬁed parser for the C99 language.

1

Introduction

Parsing remains an essential component of compilers and other programs that
input textual representations of structured data. Its theoretical foundations arewell understood today, and mature technology, ranging from parser combinatorlibraries to sophisticated parser generators, is readily available to help implementing parsers.
The issue we focus on in this paper is that of parser correctness: how to
obtain formal evidence that a parser is correct with respect to its speciﬁcation?
Here, following established practice, we choose to specify parsers via context-freegrammars enriched with semantic actions.
One application area where the parser correctness issue naturally arises isformally-veriﬁed compilers such as the CompCert veriﬁed C compiler [14]. Indeed, in the current state of CompCert, the passes that have been formally veriﬁed start at abstract syntax trees (AST) for the CompCert C subset of C andextend to ASTs for three assembly languages. Upstream of these veriﬁed passes
are lexing, parsing, type-checking and elaboration passes that are still in need offormal veriﬁcation in order to attain end-to-end veriﬁcation. The present paper
addresses this need for the parsing pass. However, its results are more generally
applicable to all high-assurance software systems where parsing is an issue.
There are many ways to build conﬁdence in a parser. Perhaps the simplest
way is to instrument an unveriﬁed parser so that it produces full parse trees,
and, at every run of the compiler, check that the resulting parse tree conforms
to the grammar. This approach is easy to implement but does not establish
completeness (all valid inputs are accepted) or unambiguity (for each input,
there is at most one parse tree). Another approach is to apply program proof

Fig. 1. General architecture.

directly to a hand-written or generated parser. However, such a proof is tedious,
especially if the parser was automatically generated, and must be re-done every
time the the parser is modiﬁed. Yet another approach, developed by Barthwal
and Norrish [4,3], is to formally verify, once and for all, a parser generator,
guaranteeing that whenever the veriﬁed generator succeeds, the parser that it
produces is correct with respect to the input grammar. However, Barthwal and
Norrish’s proof is speciﬁc to a particular parser generator that only accepts SLR
grammars. It so happens that the ISO C99 grammar we are interested in is not
SLR. Before being applicable to CompCert, Barthwal and Norrish’s work would,
therefore, have to be extended in nontrivial ways to a richer class of grammars
such as LALR.
In this paper, we develop a fourth approach: a posteriori veriﬁed validation ofan LR(1) automaton produced by an untrusted parser generator, as depicted inFig. 1. After every run of the parser generator (that is, at compile-compile time),
the source grammar G, the generated automaton A, and auxiliary information
acting as a certiﬁcate are fed in a validator, which checks whether A recognizes
the same language as G. If so, the build of the compiler proceeds; if not, it isaborted with an error.
The ﬁrst contribution of this paper is the algorithm that performs this validation. It is relatively simple, and, to the best of our knowledge, original. It applies
indiﬀerently to many ﬂavors of LR(1) automata, including LR(0) (a degeneratecase), SLR [5], LALR [2], Pager’s method [17], and canonical LR(1) [12]. The
second contribution is a soundness proof for this algorithm, mechanized using
the Coq proof assistant, guaranteeing with the highest conﬁdence that if thevalidation of an automaton A against a grammar G succeeds, then the automaton A and the interpreter that executes it form a correct parser for G. The lastcontribution is an experimental assessment of our approach over the ISO C99
grammar, demonstrating applicability to realistic parsers of respectable size.
In summary, the approach to high-conﬁdence parsing developed in this paper
is attractive for several reasons: (1) it provides correctness guarantees about anLR(1) parser as strong as those obtained by verifying a LR(1) parser generator;(2) only the validator needs to be formally veriﬁed, but not the parser generator
itself, reducing the overall proof eﬀort; (3) the validator and its soundness proof
are reusable with diﬀerent parser generators and diﬀerent ﬂavors of LR(1) parsing; (4) existing, mature parser generators such as Menhir [19] can be used withminimal instrumentation, giving users the beneﬁts of the extensive diagnostics
produced by these generators.
This paper is organized as follows. In §2, we review context-free grammars,
LR(1) automata, and their meaning. In §3, we establish three properties of automata, namely soundness (§3.1), safety (§3.2) and completeness (§3.3). Safety
and completeness are true only of some automata: we present a set of conditions
that are suﬃcient for these properties to hold and that can be automaticallychecked by a validator. After presenting some facts about our Coq implementation (§4), we discuss its application to a C99 parser in the setting of CompCert(§5). We conclude with discussions of related work (§6) and directions for future
work (§7).
Our modiﬁcations to Menhir are available as part of the standard release [19].
Our Coq code is not yet part of the CompCert release, but is available online [10].

2Grammars and Automata

2.1

Symbols

We ﬁx an alphabet of terminal symbols a and an alphabet of non-terminal symbols A, where an alphabet is a ﬁnite set. A symbol X is either a terminal symbol
or a non-terminal symbol. We write α for a sentential form, that is, a ﬁnite
sequence of symbols.
2.2

Grammars

We ﬁx a grammar G, where a grammar consists of:
1. a start symbol S;
2. an alphabet of productions p;
3. for every symbol X, a type JXK.
The ﬁrst two components are standard. (The syntax of productions will be presented shortly.) The third component, which is not usually found in textbooks,
arises because we are interested not in recognition, but in parsing: that is, wewould like not only to decide whether the input is valid, but also to construct
a semantic value. In other words, we would like to consider that a grammar
deﬁnes not just a language (a set of words) but a relation between words andsemantic values. However, before we do so, we must answer the question: what is
the type of semantic values? It should be decided by the user, that is, it shouldbe part of the grammar. Furthermore, one should allow distinct symbols to carrydiﬀerent types of semantic values. For instance, a terminal symbol that stands

for an identiﬁer might carry a string, while a non-terminal symbol that stands
for an arithmetic expression might carry an abstract syntax tree, that is, a valueof a user-deﬁned inductive type. If we were to force the user to adopt a single
universal type of semantic values, the user’s code would become polluted withtags and dynamic tests, and it would not be possible for the user to argue thatthese tests cannot fail. For this reason, for every symbol X, we allow the user
to choose the type JXK of the semantic values carried by X. (In Coq, JXK has
type Type.) By abuse of notation, if α is a (possibly empty) sequence of symbols
X1 . . . Xn , we write JαK for the tuple type JX1 K × . . . × JXn K.
How are semantic values constructed? The answer is two-fold. The semantic
values carried by terminal symbols are constructed by the lexer: in other words,
they are part of the input that is submitted to the parser. The semantic values
carried by non-terminal symbols are constructed by the parser: when a production is reduced, a semantic action is executed. Let us now examine each of these
two aspects in greater detail.
The input of the parser is a stream of tokens, where a token is a dependentpair (a, v) of a terminal symbol a and a semantic value v of type JaK. We assume
that this stream is inﬁnite. There is no loss of generality in this assumption:
if one wishes to work with a ﬁnite input stream, one can complete it with an
inﬁnite number of copies of a new “end-of-stream” token. In the following, we
write w for a ﬁnite sequence of tokens and ω for an inﬁnite stream of tokens.
A production p is a triple of the form A −→ α {f }. (Above, we have written that productions form an alphabet, that is, they are numbered. We abusenotation and elide the details of the mapping from productions-as-numbers to
productions-as-triples.) The left-hand side of a production is a non-terminal
symbol A. The right-hand side consists of a sentential form α and a semantic
action f of type JαK → JAK. The semantic action, which is provided by theuser, indicates how a tuple of semantic values for the right-hand side α can betransformed into a semantic value for the left-hand side A. In our approach, thesemantic action plays a dual role: on the one hand, it is part of the grammar, andplays a role in the deﬁnition of the semantics of the grammar; on the other hand,
it is used, at runtime, by the parser. The semantic action is a Coq function andis supplied by the user as part of the grammar. (The parser generator Menhir
views semantic actions as pieces of text, so no modiﬁcation is needed for it to
support Coq semantic actions instead of Objective Caml semantic actions.)

2.3

Semantics of Grammars

The semantics of grammars is usually deﬁned in terms of a relation between
symbols X and words w, written X −→ w, pronounced: “X derives w”. Asannounced earlier, we extend this relation with a third parameter, a semanticvvalue v of type JXK. Thus, we write X −→ w, pronounced: “X derives w pro-

ducing v”. The inductive deﬁnition of this relation is as follows:va −→ (a, v)

A −→ X1 . . . Xn {f } is a productionvi∀i ∈ {1, . . . , n}
Xi −→
wi
A

f (v1 ,...,vn )−→w1 . . . wn

This semantics is used when we state that the parser is sound and completewith respect to the grammar (Theorems 1 and 3).
2.4

Automata

We ﬁx an automaton A, where an automaton consists of:
1. an alphabet of states σ, with a distinguished initial state, written init;
2. an action table;
3. a goto table;
4. for every non-initial state σ, an incoming symbol, written incoming(σ).
A non-initial state is a state other than init.
An action table is a total mapping of pairs (σ, a) to actions. The idea is, if σ isthe current state of the automaton and a is the terminal symbol currently foundat the head of the input stream, then the corresponding action instructs theautomaton what to do next. An action is one of shift σ 0 (where σ 0 is non-initial),
reduce p (where p is a production), accept, and reject. In particular, the situation
where the action table maps (σ, a) to shift σ 0 can be thought of graphically as
an edge, labeled a, from σ to σ 0 .
Remark 1. Our description of the action table as a mapping of pairs (σ, a) toactions appears to imply that the parser must peek at the next input token a
before it can decide upon the next action. This might seem perfectly acceptable:
because we have assumed that the input stream is inﬁnite, there always is one
more input token. In practice, however, more care is required. There are situations where the input stream is eﬀectively inﬁnite and nevertheless one must notallow the parser to systematically peek at the next token. For instance, the input
stream might be connected to a keyboard, where a user is entering commands.
If the parser has been asked to recognize one command, then, upon ﬁnding theend of a command, it should terminate and report success without attempting
to read one more token: otherwise, it runs the risk of blocking until further
keyboard input is available!
In order to address this problem, we allow our automata to sometimes take adefault action without peeking at the next input token. We adopt the following
convention: if, for a certain state σ and for all terminal symbols a, the entries
found at (σ, a) in the action table are identical, then the automaton, when instate σ, determines which action should be taken without consulting the input
stream3 .
3

Of course, it would be ineﬃcient to naı̈vely test whether one entire column of theaction table contains identical entries. In reality, Menhir produces (and our Coq

A goto table is a partial mapping of pairs (σ, A) to non-initial states. If thegoto table maps (σ, A) to σ 0 , then the automaton can take a transition from σ
to σ 0 after recognizing a word that derives from A. This can be thought ofgraphically as an edge, labeled A, from σ to σ 0 . This table is a partial mapping:a state σ may have no outgoing edge labeled A.
A well-formed LR automaton has the property that, for every non-initialstate σ, all of the edges that enter σ carry a common label. (The initial state
init has no incoming edges.) We refer to this label as the incoming symbol of σ.
Although we could have our validator reconstruct this information, we ask theuser to supply it as part of the description of the automaton. We require that
this information be consistent with the action and goto tables, as follows. If theaction table maps (σ, a) to shift σ 0 , then we require incoming(σ 0 ) = a. Similarly,
if the goto table maps (σ, A) to σ 0 , then we require incoming(σ 0 ) = A. We
encode these requirements directly in the types of the action and goto tables,using dependent types, so we do not need to write validation code for them.
2.5

Semantics of Automata

We give semantics to automata by deﬁning an interpreter for automata. Theinterpreter is a function named parse(·, ·). Its ﬁrst (and main) argument is atoken stream ω. We need an auxiliary argument, the “fuel”, which is discussed
further on.
The interpreter maintains a stack s, which is a list of dependent pairs ofa non-initial state σ and a semantic value v of type Jincoming(σ)K. Indeed,
incoming(σ) is the (terminal or non-terminal) symbol that was recognized prior
to entering state σ, and v is a semantic value associated with this symbol. We
write s(σ, v) for a stack whose top cell is the pair (σ, v) and whose tail is thestack s. At the beginning of a run, the stack is empty. At every moment, thecurrent state of the automaton is the state found in the top stack cell if the stack
is non-empty; it is the initial state init if the stack is empty4 .
In several places, the interpreter can generate an internal error, revealing a
ﬂaw in the automaton. Indeed, it is sometimes much easier to write an interpreterthat can encounter an internal error, and prove a posteriori that this situation
never arises if the automaton satisﬁes certain properties, than to deﬁne a priori
an interpreter than never encounters an internal error. In other words, insteadof hardwiring safety (that is, the absence of internal errors) into the deﬁnitionof the interpreter, we make it a separate theorem (Theorem 2).
We use an error monad to deal with internal errors. In this paper, we use to
denote an internal error. By abuse of notation, we elide the “return” operation
code uses) a two-level action table, where the ﬁrst level is indexed only by a state σ
and indicates whether there exists a default action, and the second level (which isconsulted only if there is no default action) is indexed by a state σ and a terminal
symbol a.
4
In many textbooks, one does not consider semantic values, so the stack is a list of
states; at the beginning of a run, the stack is a singleton list of the state init; thestack is never empty, so the current state is always the one found on top of the stack.

of the error monad. Thus, the interpreter produces either or a parse result(deﬁned below).
We also need a way of dealing with the possibility of non-termination. Again,
it is not possible to prove a priori that the interpreter terminates. When an LR
automaton reduces a unit production (of the form A −→ A0 ) or an epsilon
production (of the form A −→ ε), the size of the stack does not decrease. There
do exist automata, as per the deﬁnition of §2.4, whose interpretation does not
terminate. It is not clear, at present, what property one could or should requireof the automaton in order to ensure termination. (We discuss this issue in §7.)
We adopt a simple and pragmatic approach to this problem: in addition to
the token stream, the interpreter requires an integer argument n, which we referto as the fuel. In the main loop of the interpreter, each iteration consumes one
unit of fuel. If the interpreter runs out of fuel, it stops and reports that it was
not able to terminate normally. We write out-of-fuel for this outcome.
Thus, a parse result is one of: out-of-fuel, which was explained above; reject,which means that the input is invalid; and parsed v ω, which means that the
input is valid, that the semantic value associated with the preﬁx of the inputthat was recognized is v, and that the remainder of the input is ω. (The value v
has type JSK, where S is the start symbol of the grammar. The value ω is atoken stream.)
In summary, the interpreter accepts a token stream and a certain amount offuel and produces either or a parse result, as deﬁned above.
The interpreter works in a standard manner. At each step, it looks up theaction table at (σ, a), where σ is the current state of the automaton and (a, v)
is the next input token. Then,
1. if the action is shift σ 0 , the input token (a, v) is consumed, and the newcell (σ 0 , v) is pushed onto the stack. Because incoming(σ 0 ) = a holds, it ispossible to cast the value v from the type JaK to the type Jincoming(σ 0 )K:
this is required for this new stack cell to be well-typed.
2. if the action is reduce A −→ X1 . . . Xn {f }, the interpreter attempts to
pop n cells oﬀ the stack, say (σ1 , v1 ) . . . (σn , vn ), and dynamically checks that
incoming(σi ) = Xi holds for every i ∈ {1, . . . , n}. If the stack does not haveat least n cells, or if this check fails, then an internal error occurs. Otherwise,
thanks to the success of these dynamic checks, each of the semantic values vi
can be cast from the type Jincoming(σi )K to the type JXi K. Thus, the tuple(v1 , . . . , vn ) admits the type JX1 . . . Xn K, and is a suitable argument for thesemantic action f . The application of f to this tuple yields a new semantic
value v of type JAK. There remains for the interpreter to consult the goto
table at the current state and at the non-terminal symbol A. If this entry in
the goto table is undeﬁned, an internal error occurs. Otherwise, this entry
contains a state σ 0 , and (after another cast) the new cell (σ 0 , v) is pushed
onto the stack.
3. if the action is accept, the interpreter attempts to pop one cell oﬀ the stack,say (σ, v), and checks that incoming(σ) = S holds, where S is the startsymbol of the grammar. Thus, the value v can be cast to the type JSK.

(This can be thought of as reducing a special production S 0 −→ S.) The
interpreter then checks that the stack is now empty and terminates with theparse result parsed v ω, where ω is what remains of the input stream.
4. if the action is reject, the interpreter stops with the parse result reject.
In summary, there are four possible causes for an internal error: a dynamic
check of the form incoming(σ) = X may fail; an attempt to pop a cell oﬀ thestack fails if the stack is empty; an attempt to consult the goto table fails if thedesired entry is undeﬁned; an attempt to accept fails if the stack is nonempty.

3

Correctness Properties and Validation

We now show how to establish three properties of the automaton A with respect
to the grammar G. These properties are soundness (the parser accepts only valid
inputs), safety (no internal error occurs), and completeness (the parser accepts
all valid inputs). By design of our interpreter, the ﬁrst property is true of all
automata, whereas the latter two are true only of some automata. For safety
and for completeness, we present a set of conditions that are suﬃcient for thedesired property to hold and that can be automatically checked by a validator.
3.1

Soundness

The soundness theorem states that if the parser accepts a ﬁnite preﬁx w of the
input stream ω, then (according to the grammar) the start symbol S derives w.
More precisely, if the parser accepts w and produces a semantic value v, then v
is the value associated with this particular derivation of w from S, that is, thev
relation S −→ w holds.
Theorem 1 (Soundness). If parse(ω, n) = parsed v ω 0 holds, then there existsv
a word w such that ω = wω 0 and S −→ w.
No hypotheses about the automaton are required, because the situations
where “something is wrong” and soundness might be endangered are detected
at runtime by the interpreter and lead to internal errors. In other words, wehave shifted most of the burden of the proof from the soundness theorem to thesafety theorem.
In order to prove this theorem, it is necessary to establish an invariant statingthat the symbols associated with the states found in the stack derive the input
word that has been consumed. For this purpose, we introduce a new predicate,
written s =⇒ w, which relates a stack s with a token word w. It is inductively
deﬁned as follows:v

ε =⇒ εs =⇒ w1
incoming(σ) −→ w2s(σ, v) =⇒ w1 w2Then, the main soundness invariant can be stated as follows: if the parser has
consumed the input word w and if the current stack is s, then s =⇒ w holds.

3.2

SafetyThe safety theorem states that if the automaton passes the safety validator(which we describe further on) then the interpreter never encounters an internal
error. A validator is a Coq term of type bool, which has access to the grammar,
to the automaton, and to certain additional annotations that serve as hints (andwhich we describe below as well). Thus, the safety theorem takes the following
form:
Theorem 2 (Safety). If the criteria enforced by the safety validator are satisﬁed, then parse(ω, n) 6= for every input stream ω and for every integer “fuel” n.
All of the causes of internal errors that were previously listed (§2.5) haveto do with a stack that does not have the expected shape (e.g., it has too few
cells) or contents (e.g. some cell contains a semantic value of inappropriate type,or contains a state for which no entry exists in the goto table). Thus, in orderto ensure safety, we must have precise control of the shape and contents of thestack.
Recall that a stack s is a sequence of pairs (σ1 , v1 ) . . . (σn , vn ). In what follows, it is convenient to abstractly describe the structure of such a stack in two
ways. First, we are interested in the underlying sequence of symbols: we write
symbols(s) for the sequence of symbols incoming(σ1 ) . . . incoming(σn ). Second,
we are interested in the underlying sequence of states: we write states(s) for
the sequence of singleton sets {init}{σ1 } . . . {σn }. (We use singleton sets here
because we will shortly be interested in approximating these singleton sets withlarger sets of states Σ.)
A key remark is the following: the sequences symbols(s) and states(s) are notarbitrary. They follow certain patterns, or, in other words, they respect a certain
invariant. This invariant will be suﬃcient to guarantee safety.
How do we ﬁnd out what this invariant is? Two approaches come to mind:
either the safety validator could reconstruct this invariant by performing a static
analysis of the automaton (this would require a least ﬁxed point computation),or the parser generator could produce a description of this invariant, which
the safety validator would verify (this would require checking that a candidate
ﬁxed point is indeed a ﬁxed point). We somewhat arbitrarily adopt the latterapproach. The former approach appears viable as well, especially if one exploits
a pre-existing veriﬁed library for computing least ﬁxed points.
Thus, the annotations that the safety validator requires (and that the parser
generator must produce) form a description of the safety invariant. For each
non-initial state σ, these annotations are:
1. a sequence of symbols, written pastSymbols(σ);
2. a sequence of sets of states, written pastStates(σ).
(There is a redundancy, which we discuss in §7.) These annotations are meant torepresent approximate (conservative) information about the shape and contentsof the stack. In order to explain their meaning, let us now deﬁne the safety
invariant in terms of these annotations.

We begin by deﬁning the relations that exist between abstract descriptionsof the stack and concrete stacks. We need two such relations. The suﬃx ordering
between two sequences of symbols is deﬁned in the usual way: that is, Xm . . . X1
is a suﬃx of Xn0 . . . X10 if and only if m ≤ n holds and Xi = Xi0 holds for everyi ∈ {1, . . . , m}. The suﬃx ordering between two sequences of sets of states isdeﬁned in the same manner, up to pointwise superset ordering: that is, Σm . . . Σ1
is a suﬃx of Σn0 . . . Σ10 if and only if m ≤ n and Σi ⊇ Σi0 holds for everyi ∈ {1, . . . , m}.
Equipped with these suﬃx orderings, which serve as abstraction relations, we
can deﬁne the safety invariant. This is a predicate over a stack, written safe s.
It is inductively deﬁned as follows:

safe εpastSymbols(σ) is a suﬃx of symbols(s)pastStates(σ) is a suﬃx of states(s)safe ssafe s(σ, v)

A stack s(σ, v) is safe if (a) the annotations pastSymbols(σ) and pastStates(σ)
associated with the current state σ are correct approximate descriptions of thetail s of the stack and (b) the tail s is itself safe. Less formally, pastSymbols(σ)
and pastStates(σ) are static descriptions of a suﬃx of the stack (i.e., the partof the stack that is closest to the top). The rest of the stack, beyond this statically known suﬃx, is unknown. Nevertheless, this information is suﬃcient (ifvalidation succeeds) to show that internal errors cannot occur: for instance, itguarantees that, whenever we attempt to pop k cells oﬀ the stack, at least kcells are present.
Now, in order to ensure that safe s is indeed an invariant of the interpreter,
the validator must check that the annotations pastSymbols(σ) and pastStates(σ)
are consistent. Furthermore, the validator must verify a few extra conditions
which, together with the invariant, ensure safety. The safety validator checks
that the following properties are satisﬁed:
1. For every transition, labeled X, of a state σ to a new state σ 0 ,– pastSymbols(σ 0 ) is a suﬃx of pastSymbols(σ)incoming(σ),– pastStates(σ 0 ) is a suﬃx of pastStates(σ){σ}.
2. For every state σ that has an action of the form reduce A −→ α {f },– α is a suﬃx of pastSymbols(σ)incoming(σ),– If pastStates(σ){σ} is Σn . . . Σ0 and if the length of α is k, then for every
state σ 0 ∈ Σk , the goto table is deﬁned at (σ 0 , A). (If k is greater than n,take Σk to be the set of all states.)
3. For every state σ that has an accept action,– σ 6= init,– incoming(σ) = S,
– pastStates(σ) = {init}.
Thanks to the ﬁniteness of the alphabets, these conditions are clearly andeﬃciently decidable.

These conditions do not depend in any way on the manner in which lookahead
is exploited to determine the next action. In other words, an LR(1) automaton
is safe if and only if the underlying non-deterministic LR(0) automaton is safe.
Thus, the safety validator is insensitive to which method was used to construct
the LR(1) automaton.
3.3

CompletenessThe completeness theorem states that if the automaton passes the completenessvalidator (which we describe further on), if a preﬁx w of the input is valid, andif enough fuel is supplied, then the parser accepts w and constructs a correct
semantic value. (The theorem also allows for the possibility that the parser might
encounter an internal error. This concern was dealt with in §3.2, so we need notworry about it here.)
Theorem 3 (Completeness). If the criteria enforced by the completeness valv
idator are satisﬁed and if S −→ w holds, then there exists n0 such that for all ωand for all n ≥ n0 , either parse(wω, n) = or parse(wω, n) = parsed v ω.
The Coq version of this result is in fact more precise. We prove that a suitablevvalue of n0 is the size of the derivation tree for the hypothesis S −→ w, and we
prove that this is the least suitable value, that is, n < n0 implies parse(wω, n) =out-of-fuel .
In order to guarantee that the automaton is complete, the validator must
check that each state has “enough” permitted actions for every valid input tobe eventually accepted. But how do we know, in a state σ, which actions shouldbe permitted? We can answer this question if we know which set of LR(1) items
is associated with σ. Recall that an item is a quadruple A −→ α1 • α2 [a],where A −→ α1 α2 {f } is a production and a is a terminal symbol. The intuitive
meaning of an item is: “we have recognized α1 ; we now hope to recognize α2 andﬁnd that it is followed with a; if this happens, then we will be able to reduce theproduction A −→ α1 α2 {f }”.
Our items are relative to an augmented grammar, where a virtual production
S 0 −→ S has been added. This means that we can have items of the form
S 0 −→ • S [a] (these appear in the initial state of the automaton) and items of
the form S 0 −→ S • [a] (these appear in the ﬁnal, accepting state).
The parser generator knows which set of items is associated with each stateof the automaton. We require that this information be transmitted to the completeness validator. (One could instead reconstruct this information, and one
would not even need to prove the correctness of the algorithm that reconstructs
it; but it is not clear what one would gain by doing so.)With this information, the validator carries out two kinds of checks. First, it
checks that each state σ has “enough” actions: that is, the presence of certain
items in items(σ) implies that certain actions must be permitted. Second, it
checks that the sets items(σ) are closed and consistent: that is, the presence of
certain items in items(σ) implies that certain items must be present in items(σ)

(this is closure) and in items(σ 0 ), where σ 0 ranges over the successor states of σ
(this is consistency).
The deﬁnition of the closure property, which appears below, relies on theknowledge of the “ﬁrst” sets, which in turn requires the knowledge of which
non-terminal symbols are “nullable”. It is well-known that “ﬁrst” and “nullable”
form the least ﬁxed point of a certain system of positive equations. Again, we
could have the validator compute this least ﬁxed point; instead, we require thatit be transmitted from the parser generator to the validator, and the validator
just checks that it is a ﬁxed point.
In summary, the annotations that the completeness validator requires (andthat the parser generator must produce) are:
1. for each state σ, a set of items, written items(σ).
2. for each non-terminal symbol A, a set of terminal symbols ﬁrst(A);3. for each non-terminal symbol A, a Boolean value nullable(A).
The properties that the completeness validator enforces are:
1. “ﬁrst” and “nullable” are ﬁxed points of the standard deﬁning equations.
2. For every state σ, the set items(σ) is closed, that is, the following implication
holds:A −→ α1 • A0 α2 [a] ∈ items(σ)
A0 −→ α0 {f 0 } is a productiona0 ∈ ﬁrst(α2 a)
A0 −→ • α0 [a0 ] ∈ items(σ)
3. For every state σ, if A −→ α • [a] ∈ items(σ), where A 6= S 0 , then the action
table maps (σ, a) to reduce A −→ α {f }.
4. For every state σ, if A −→ α1 • aα2 [a0 ] ∈ items(σ), then the action tablemaps (σ, a) to shift σ 0 , for some state σ 0 such that:A −→ α1 a • α2 [a0 ] ∈ items(σ 0 )5. For every state σ, if A −→ α1 • A0 α2 [a0 ] ∈ items(σ), then the goto table
either is undeﬁned at (σ, A0 ) or maps (σ, A0 ) to some state σ 0 such that:A −→ α1 A0 • α2 [a0 ] ∈ items(σ 0 )6. For every terminal symbol a, we have S 0 −→ • S [a] ∈ items(init).
7. For every state σ, if S 0 −→ S • [a] ∈ items(σ), then σ has a default accept
action.
These conditions are clearly decidable. In order to achieve reasonable eﬃciency, we represent items in a compact way: ﬁrst, we group items that have acommon LR(0) core; second, we use a natural number to indicate the position of
the “bullet”. Thus, in the end, we manipulate triples of a production identiﬁer p,
an integer index into the right-hand side of p, and a set of terminal symbols.

Furthermore, we use the standard library FSets [6], which implements ﬁnite sets
in terms of balanced binary search trees, in order to represent sets of items.
The various known methods for constructing LR(1) automata diﬀer only in
how they decide to merge, or not to merge, certain states that have a common
LR(0) core. The completeness validator is insensitive to this aspect: as long as
no conﬂict arises due to excessive merging, an arbitrary merging strategy can be
employed.
There is a relatively simple intuition behind the proof of Theorem 3. Supposevan oracle gives us a proof of S −→ w, that is, a parse tree. Then, the parser,
confronted with the input w, behaves in a very predictable way: it eﬀectively
performs a depth-ﬁrst traversal of this parse tree. When the parser performsa shift action, it visits a (terminal) leaf of the parse tree; when it performs a
reduce action, it visits a (non-terminal) node of the parse tree. At any time,
the parser’s stack encodes the path that leads from the root of the tree down
to the current node of the traversal, and holds the semantic values associatedwith parse tree nodes that have been fully processed, but whose parent has notbeen fully processed yet. At any time, the unconsumed input corresponds to thefringe of the part of the parse tree that has not been traversed yet.
This invariant allows us to prove that the parser cannot reject the input wω.
Instead, it keeps shifting and reducing until it has traversed the entire parsetree. At this point, it has consumed exactly w, and it must accept and produce
exactly v. Note that there is no need to implement an “oracle”. We simply provethat if there exists a parse tree, then the parser behaves as if it were traversing
this parse tree, and accepts at the end.
In order to make this intuition precise, we deﬁne an invariant that relates
the stack, the unconsumed input, and a path in the parse tree provided by the“oracle”. The deﬁnition of this invariant is quite technical, but can be summed
up as follows. There exists a path in the “oracle” parse tree such that:
1. The path begins at the root of the parse tree.
2. For each node in this path, the children of this node can be divided in threeconsecutive segments (or, at the last node in the path, in two segments):– children that have already been visited: the semantic value associatedwith each of these children is stored in a stack cell;– the child that is being visited (absent if we are at the bottom of thepath): this child is the next node in the path;– children that will be visited in the future: their fringes correspond tosegments of the unconsumed input stream.
3. The unconsumed input begins with the concatenation of the fringes of the“unvisited children” of all nodes in the path.
4. The sequence of all stack cells is in one-to-one correspondence with the concatenation of the sequences of “visited children” of all nodes in the path.
5. As per the previous item, each stack cell (σ, v) is associated with a certain
child y of a certain node x in the path. Then, the semantic value carried by
the node y must be precisely v. Furthermore, if the node x is labeled with the
production A −→ α1 Xα2 and if the child y corresponds to the symbol X,then the item A −→ α1 X • α2 [a] appears in items(σ), where a is the ﬁrst
symbol in the partial fringe that begins “after” the node x.
During parsing, this path evolves in the following ways:
1. Between two actions: if the ﬁrst unvisited child of the last node of the pathexists and is not a terminal leaf, then the next action of the automaton willtake place under this child. It is then necessary to extend the path: thischild becomes the last node of the path. This extension process is repeatedas many times as possible.
2. When shifting: if the ﬁrst unvisited child of the last node exists and is aterminal leaf, then the next action must be a shift action. This child isconsidered visited and transferred to the ﬁrst segment of children of the lastnode. The path itself is unchanged.
3. When reducing: if the last node of the path has no unvisited child, then thenext action must be a reduce action for the production that corresponds tothis node. Then, the path is shortened by one node: that is, if x and y are
the last two nodes in the path, then x becomes the last node in the path,and y becomes the last visited child of x.
3.4

Unambiguity

It is easy to prove the following result.
Theorem 4. Suppose there exists a token. If the criteria enforced by the safety
and completeness validators are satisﬁed, then the grammar is unambiguous.
The proof goes as follows. Suppose that the automaton is safe and complete.
v1
v2
Suppose further that, for some word w, both S −→w and S −→w hold. By thesafety hypothesis, the parser never encounters an internal error . Thus, by thecompleteness hypothesis, given a suﬃciently large amount of fuel, the parser,
applied to wω (where ω is arbitrary), must produce v1 , and by a similar argument, must produce v2 . However, our automata are deterministic by deﬁnition:parse is a function. Thus, v1 and v2 must coincide.

4

Coq Formalization

All of the results presented in this paper were mechanized using the Coq 8.3pl1
proof assistant. The Coq formalization is fairly close to the deﬁnitions, theorems
and proofs outlined in this paper.
We use of dependent types to support semantic values and semantic actions
whose types are functions of the corresponding symbols and productions. This
enables us to support user-supplied semantic actions with essentially no proof
overhead compared with a “pure” parser that only produces a parse tree.
We make good use of Coq’s module system: the validator and the interpreter
are functors parameterized over abstract types for terminal and non-terminal

symbols. The only constraints over these two types of symbols are that theymust be ﬁnite (so that it is possible to decide universal quantiﬁcations oversymbols) and they must come with a decidable total order (so that they can beused in conjunction with the FSets library).
The Coq formalization is pleasantly small: about 2500 lines, excluding comments. The executable speciﬁcations of the safety validator and the completenessvalidator are about 200 lines each. The proofs of soundness, safety, and completeness account for 200, 500, and 700 lines, respectively.

5

Experimentation on a C99 Parser

The grammar. Our starting point is the context-free grammar given in Annex Aof the ISO C99 standard [9]. We omit the productions that support unprototyped“K&R-style” function deﬁnitions, since such old-style deﬁnitions are considered“an obsolescent feature” [9, section 6.11.7] and are not supported by subsequentpasses of the CompCert compiler.
Both this slightly simpliﬁed C grammar and the original ISO C99 grammar
are ambiguous. There are three distinct sources of ambiguity.
The ﬁrst source of ambiguity is the classic “dangling-else” problem, which
introduces a shift-reduce conﬂict in the LR(1) automaton. We eliminated thisconﬂict by a slight modiﬁcation to the grammar, distinguishing two non-terminal
symbols for statements: one that prohibits if statements without an else part,and the other that permits them.
The second source of ambiguity is the well-known problem with typedef
names (identiﬁers bound to a type by a typedef declaration), which must be
distinguished from other identiﬁers. For example, “a * b;” is to be parsed asa declaration of a variable b of type “pointer to a” if a is a typedef name, butstands for the multiplication of a by b otherwise. To avoid major ambiguities in
the grammar, it is mandatory to use two distinct terminal symbols, typedef-nameand variable-name, and rely on the lexer to classify identiﬁers into one of these
two terminal symbols. The traditional way of doing so, aﬀectionately referred toas “the lexer hack”, is to have the semantic actions of the parser maintain a table of typedef names currently in scope, and to have the lexer consult this table
to classify identiﬁers. We were reluctant to perform such side eﬀects within thesemantic actions of our veriﬁed parser. Instead, like Padioleau [16], we interposea “pre-parser” between the lexer and the veriﬁed parser, whose sole purpose
is to keep track of typedef names currently in scope and classify identiﬁers as
either typedef-name or variable-name in the token stream that feeds the veriﬁed
parser. For simplicity of implementation, the pre-parser is actually a full-ﬂedged
but unveriﬁed C99 parser that implements the standard “lexer hack” scheme.
The third and last source of ambiguity is also related to typedef names, butmore subtle. Consider the declaration “int f(int (a));” where a is a typedef
name. It can be read as “a function f with one parameter named a of type int”,
but also as “a function f with one anonymous parameter of function type a →int”. The original ISO C99 standard leaves this ambiguity open, but TechnicalCorrigendum 2 speciﬁes that the second interpretation is the correct one [9,clause 6.7.5.3(11)]. Again, we rely on our pre-parser to correctly resolve thisambiguity (via well-chosen precedence annotations) and to ensure that identiﬁers
in binding positions are correctly classiﬁed as typedef names (if previously boundby typedef and not to be redeclared, as in the example above) or as variablenames (in all other cases, even if previously bound by typedef).
Generating the parser. We use the Menhir parser generator [19] modiﬁed to
produce not only an LR(1) automaton but also a representation of the source
grammar as well as the various annotations needed by the validator. All outputs
are produced as Coq terms and deﬁnitions that can be directly read into Coq.
The modiﬁcations to Menhir are small (less than 500 lines of Caml code) and
reside in just one new module.
Our modiﬁed C99 grammar comprises 87 terminal symbols, 72 non-terminal
symbols, and 263 productions. The LR(1) automaton generated by Menhir using
Pager’s method contains 505 states. (The grammar is in fact LALR, and theautomaton produced by Menhir is indeed identical to the LALR automatonthat would be produced by an LALR parser generator.) The generated Coq ﬁleis approximately 4.5 Mbytes long, of which 6% correspond to the automaton,
2% to the description of the grammar, and the remaining 92% are annotations(item sets, mostly).

Validating the parser. Running the validator on this output, using Coq’s builtin virtual machine execution engine (the Eval vm_compute tactic), takes 19
seconds: 4s to validate safety and 15s to validate completeness5 . Coq takes anadditional 32s to read and type-check the ﬁle generated by Menhir, for a total
processing time of 51s. While not negligible, these validation times are acceptablein practice. In order to further reduce the validation time, one could probably use
improved data structures or extract the validator to natively-compiled OCaml
code; but there is no pressing need.

Running the parser. With some elbow grease, we were able to replace CompCert
1.9’s unveriﬁed parser (an LALR automaton produced by OCamlYacc) with our
new veriﬁed parser. The veriﬁed parser runs about 5 times slower than the oldone, increasing overall compilation times by about 20%. There are two major
reasons for this slowdown. One is that we eﬀectively parse the input twice: oncein the pre-parser, to track typedef names, and once “for good” in the veriﬁed
parser. Another reason is that the interpreter that executes the veriﬁed parser iswritten in Coq, then extracted to Caml, and performs redundant runtime checks
compared with OCamlYacc’s execution engine, which is coded in C and performs
no runtime checks whatsoever. (We discuss the issue of redundant checks in §7.)
5

All timings were measured on a Core i7 3.4GHz processor, using a single core.

6

Related Work

Although parsing is a classic and extremely well-studied topic, the constructionof veriﬁed parsers seems to have received relatively little interest.
Pottier and Régis-Gianas [20] show that, for a ﬁxed LR(1) automaton, theinductive invariant that describes the stack and guarantees safety (§3.2) can be
expressed as a generalized algebraic data type (GADT). They show that if one
constructs a parser by specializing the interpreter for this automaton, then a
type-checker equipped with GADTs can verify the safety of this parser. In addition to a safety guarantee, this approach yields a performance gain with respect
to an ML implementation, because the weaker type system of ML imposes theuse of redundant tags and dynamic checks (e.g. stack cells must be redundantly
tagged with nil or cons). Here, the interpreter is generic, and, even though it isprovably safe, it does perform redundant dynamic checks. (We discuss this issuein §7.)
Barthwal and Norrish [4] and Barthwal [3] use the HOL4 proof assistant toformalize SLR [5] parsing. For a context-free grammar, they construct an SLR
parser, and are able to prove it sound and complete: the guarantees that theyobtain are analogous to our Theorems 1 and 3. Like us, they omit a proof thatthe parser terminates when presented with an illegal input. (We discuss this issuein §7.) Although their parsers are executable, they are probably not eﬃcient, because the parser construction and parser execution phases are not distinguishedin the usual manner: in particular, while the parser is running, states are still
represented as sets of LR(1) items. Because Barthwal and Norrish formalize theparser construction process, their formalization is relatively heavyweight andrepresents over 20 000 lines of deﬁnitions and proofs. In contrast, because werely on a validator, our approach is more lightweight (2500 lines). It is also moreversatile: we can validate LR(1) automata constructed by any means, includingLR(0), SLR, LALR, Pager’s method, and Knuth’s canonical LR(1) construction. We believe that this versatility is important in practice: for instance, wehave veriﬁed that the C99 grammar is LALR but not SLR. One disadvantage
of our approach is that we cannot exclude the possibility that the parser generator (which is not veriﬁed) fails or produces an incorrect automaton. Fortunately,
this problem is detected at validation time. In our application to CompCert, it isdetected when CompCert itself is built, that is, before CompCert is distributed
to its users.
Parsing Expression Grammars (PEGs) are a declarative formalism for specifying recursive descent parsers. Ford [7,8] and other authors [24] have investigated their use as an alternative to the more traditional and better establishedcontext-free grammars. Koprowski and Binsztok [13] formalize the semantics
of PEGs, extended with semantic actions, in Coq. They implement a wellformedness check, which ensures that the grammar is not left-recursive. Under
this assumption, they are able to prove that a straightforward (non-memoizing)
PEG interpreter is terminating. The soundness and completeness of the interpreter are immediate, because the interpreter is just a functional version of thesemantics of PEGs, which is originally presented under a relational form. Wis-

nesky et al. [25] implement a veriﬁed packrat parser (that is, a PEG parser
that achieves linear time and space complexity via memoization) using the experimental programming language Ynot, which is itself embedded within Coq.
Because Ynot is a Hoare logic for partial correctness, the parser is not proved
to terminate.
We are deﬁnitely not the ﬁrst to embrace a posteriori validation as an eﬀective way to obtain correctness guarantees for compilers and program generators.
This idea goes back at least to Samet’s 1975 Ph.D. thesis [21] and was further
developed under the name translation validation by Pnueli et al. [18] and by
Necula [15]. Tristan and Leroy exploit the idea that formally-veriﬁed validators
for advanced compiler optimizations provide soundness guarantees as strong as
direct compiler veriﬁcation [23]. Another example of a formally-veriﬁed validator
is the JVM bytecode veriﬁer of Klein and Nipkow [11].

7Conclusions and Future Work

The approach to high-assurance parsing that we have developed, based on aposteriori validation of an untrusted parser generator, appears eﬀective so far.
The validation algorithms are simple enough that they could be integrated into
production parser generators and used as sanity checkers and debugging aids,
even in contexts where strong assurance is not required.
This work can be extended in several directions, including proving additional
properties of our LR(1) parser, improving its eﬃciency, and extending our work
to more expressive parsing formalisms. We now review some of these directions.
We have not proved that our parser terminates. Completeness (Theorem 3)
implies that it terminates when supplied with a valid input. However, there
remains a possibility that it might diverge when faced with an invalid input. In
fact, we have proof that the properties enforced by the safety and completenessvalidators are not suﬃcient to ensure termination. So, more requirements must
be enforced, but we are not sure, at present, what these requirements should be.
Aho and Ullman prove that canonical LR(1) parsers terminate [1, Theorem 5.13].
Their argument exploits the following property of canonical LR(1) parsers: “assoon as [the consumed input and] the ﬁrst input symbol of the remaining input
are such that no possible suﬃx could yield a sentence in L(G), the parser willreport error”. This property, however, is not true of non-canonical LR(1) parsers.
By merging several states of the canonical automaton that have a common LR(0)core, the non-canonical construction methods introduce spurious reductions: a
non-canonical automaton can perform a few extra reductions before it detects
an error. Thus, Aho and Ullman’s proof does not seem to apply to non-canonical
LR(1) parsers.
We have not proved that our parser does not peek one token past the end of
the desired input. We claim that this property holds: the automata produced by
Menhir use default actions for this purpose (see Remark 1 in §2.4). However, atpresent, we cannot even state this property, because it is an intensional propertyof the function parse: “if parse(ω, n) = parsed v ω 0 , then ω 0 has not been forced”.

In order to allow this property to be stated, one approach would be to reformulate
the parser so that it no longer has access to the token stream, but must instead
interact explicitly with the producer of the token stream, by producing “peek”
or “discard” requests together with a continuation.
We have deﬁned a “cautious” interpreter, which can in principle encounter
an internal error, and we have proved, after the fact, that (if the safety validator is satisﬁed, then) this situation never arises. This allows us to separate thedeﬁnition of the interpreter and the safety argument. A potentially signiﬁcantdrawback of this approach is that it entails a performance penalty at runtime:even though we have a proof that the dynamic checks performed by the cautious
interpreter are redundant, these checks are still present in the code, and slow
down the parser. An anonymous reviewer pointed out that, without modifying
any of our existing code, it should be possible to deﬁne an “optimistic” interpreter, which performs no runtime checks, and is subject to the precondition thatthe cautious interpreter does not fail. Sozeau’s “Program” extensions [22] could
be used to facilitate the construction of this optimistic interpreter. In the end,
only the optimistic interpreter would be executed, and the cautious interpreter
would serve only as part of the proof. We would like to thank this reviewer forthis attractive idea, which we have not investigated yet.
Some of the hints that we require are redundant. In particular, pastSymbols(§3.2) is entirely redundant, since it can in fact be deduced from pastStates andincoming. This redundancy is due to historical reasons, and could be eliminated.
This might help speed up the type-checking and validation of the annotations.
Beyond LR(1) parsing, we believe that validation techniques can apply toother parsing formalisms. It would be particularly interesting to study GLR, forwhich we hope that our validators could be re-used with minimal changes.
Our experience with the C99 grammar agrees with common wisdom on theimportance of supporting precedence and associativity declarations in order tokeep parser speciﬁcations concise and readable. It is well-known how to take thesedeclarations into account when generating LR(1) automata, but the resulting
automata are no longer complete with respect to the grammar. How could we
modify our deﬁnition of the meaning of a grammar so as to take precedence
declarations into account? How could we then extend our validation algorithms?

References
1. Aho, A.V., Ullman, J.D.: The theory of parsing, translation, and compiling. Prentice Hall (1972)
2. Anderson, T., Eve, J., Horning, J.J.: Eﬃcient LR(1) parsers. Acta Informatica 2,
12–39 (1973)
3. Barthwal, A.: A formalisation of the theory of context-free languages in higher
order logic. Ph.D. thesis, Australian National University (Dec 2010)
4. Barthwal, A., Norrish, M.: Veriﬁed, executable parsing. In: European Symposiumon Programming (ESOP). Lecture Notes in Computer Science, vol. 5502, pp. 160–
174. Springer (2009)5. DeRemer, F.L.: Simple LR(k) grammars. Communications of the ACM 14(7), 453–
460 (1971)
6. Filliâtre, J.C., Letouzey, P.: Functors for proofs and programs. In: European Symposium on Programming (ESOP). Lecture Notes in Computer Science, vol. 2986,
pp. 370–384. Springer (Mar 2004)
7. Ford, B.: Packrat parsing: simple, powerful, lazy, linear time. In: ACM International Conference on Functional Programming (ICFP). pp. 36–47 (Oct 2002)
8. Ford, B.: Parsing expression grammars: a recognition-based syntactic foundation.
In: ACM Symposium on Principles of Programming Languages (POPL). pp. 111–
122 (Jan 2004)
9. ISO/IEC: Programming languages — C (2007), international standard ISO/IEC
9899:TC3
10. Jourdan, J.H., Pottier, F., Leroy, X.: Coq code for validating LR(1) parsers, http://www.eleves.ens.fr/home/jjourdan/parserValidator.tgz
11. Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM Transactions on Programming Languages andSystems 28(4), 619–695 (2006)
12. Knuth, D.E.: On the translation of languages from left to right. Information &Control 8(6), 607–639 (Dec 1965)
13. Koprowski, A., Binsztok, H.: TRX: A formally veriﬁed parser interpreter. Logical
Methods in Computer Science 7(2) (2011)
14. Leroy, X.: Formal veriﬁcation of a realistic compiler. Communications of the ACM
52(7), 107–115 (2009)
15. Necula, G.C.: Translation validation for an optimizing compiler. In: ACM Conference on Programming Language Design and Implementation (PLDI). pp. 83–95.
ACM Press (2000)
16. Padioleau, Y.: Parsing C/C++ code without pre-processing. In: Compiler Construction. Lecture Notes in Computer Science, vol. 5501, pp. 109–125. Springer(2009)
17. Pager, D.: A practical general method for constructing LR(k) parsers. Acta Informatica 7, 249–268 (1977)
18. Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Tools and Algorithms for Construction and Analysis of Systems, TACAS ’98. Lecture Notes in
Computer Science, vol. 1384, pp. 151–166. Springer (1998)
19. Pottier, F., Régis-Gianas, Y.: The Menhir parser generator, http://gallium.
inria.fr/~fpottier/menhir/
20. Pottier, F., Régis-Gianas, Y.: Towards eﬃcient, typed LR parsers. Electronic Notes
in Theoretical Computer Science 148(2), 155–180 (2006)
21. Samet, H.: Automatically Proving the Correctness of Translations Involving Optimized Code. Ph.D. thesis, Stanford University (1975)
22. Sozeau, M.: Program-ing ﬁnger trees in Coq. In: ACM International Conference
on Functional Programming (ICFP). pp. 13–24 (Sep 2007)
23. Tristan, J.B., Leroy, X.: A simple, veriﬁed validator for software pipelining. In:
ACM Symposium on Principles of Programming Languages (POPL). pp. 83–92.
ACM Press (2010)
24. Warth, A., Douglass, J.R., Millstein, T.D.: Packrat parsers can support left recursion. In: ACM Workshop on Evaluation and Semantics-Based Program Manipulation (PEPM). pp. 103–110 (Jan 2008)
25. Wisnesky, R., Malecha, G., Morrisett, G.: Certiﬁed web services in Ynot. In: Workshop on Automated Speciﬁcation and Veriﬁcation of Web Systems (Jul 2009)