  In this paper, we present a derivative-based, functional recognizer and
parser generator for visibly pushdown grammars. The generated parser accepts
ambiguous grammars and produces a parse forest containing all valid parse trees
for an input string in linear time. Each parse tree in the forest can then be
extracted also in linear time. Besides the parser generator, to allow more
flexible forms of the visibly pushdown grammars, we also present a translator
that converts a tagged CFG to a visibly pushdown grammar in a sound way, and
the parse trees of the tagged CFG are further produced by running the semantic
actions embedded in the parse trees of the translated visibly pushdown grammar.
The performance of the parser is compared with a popular parsing tool ANTLR and
other popular hand-crafted parsers. The correctness of the core parsing
algorithm is formally verified in the proof assistant Coq.
