2 Search Results for "Roux, Cody"

Document
DOI: 10.4230/LIPIcs.ITP.2019.24
A Verified LL(1) Parser Generator

Authors: Sam Lasser, Chris Casinghino, Kathleen Fisher, and Cody Roux

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)

Abstract
An LL(1) parser is a recursive descent algorithm that uses a single token of lookahead to build a grammatical derivation for an input sequence. We present an LL(1) parser generator that, when applied to grammar G, produces an LL(1) parser for G if such a parser exists. We use the Coq Proof Assistant to verify that the generator and the parsers that it produces are sound and complete, and that they terminate on all inputs without using fuel parameters. As a case study, we extract the tool’s source code and use it to generate a JSON parser. The generated parser runs in linear time; it is two to four times slower than an unverified parser for the same grammar.
Cite as

Sam Lasser, Chris Casinghino, Kathleen Fisher, and Cody Roux. A Verified LL(1) Parser Generator. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{lasser_et_al:LIPIcs.ITP.2019.24,
  author =	{Lasser, Sam and Casinghino, Chris and Fisher, Kathleen and Roux, Cody},
  title =	{{A Verified LL(1) Parser Generator}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{24:1--24:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.24},
  URN =		{urn:nbn:de:0030-drops-110794},
  doi =		{10.4230/LIPIcs.ITP.2019.24},
  annote =	{Keywords: interactive theorem proving, top-down parsing}
}
Document
DOI: 10.4230/LIPIcs.RTA.2011.299
Refinement Types as Higher-Order Dependency Pairs

Authors: Cody Roux

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

Abstract
Refinement types are a well-studied manner of performing in-depth analysis on functional programs. The dependency pair method is a very powerful method used to prove termination of rewrite systems; however its extension to higher-order rewrite systems is still the subject of active research. We observe that a variant of refinement types allows us to express a form of higher-order dependency pair method: from the rewrite system labeled with typing information, we build a type-level approximated dependency graph, and describe a type level embedding preorder. We describe a syntactic termination criterion involving the graph and the preorder, which generalizes the simple projection criterion of Middeldorp and Hirokawa, and prove our main result: if the graph passes the criterion, then every well-typed term is strongly normalizing.
Cite as

Cody Roux. Refinement Types as Higher-Order Dependency Pairs. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 299-312, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{roux:LIPIcs.RTA.2011.299,
  author =	{Roux, Cody},
  title =	{{Refinement Types as Higher-Order Dependency Pairs}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{299--312},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.299},
  URN =		{urn:nbn:de:0030-drops-31273},
  doi =		{10.4230/LIPIcs.RTA.2011.299},
  annote =	{Keywords: Dependency Pairs, Higher-Order, Refinement Types}
}
  • Refine by Author
  • 2 Roux, Cody
  • 1 Casinghino, Chris
  • 1 Fisher, Kathleen
  • 1 Lasser, Sam

  • Refine by Classification
  • 1 Software and its engineering → Formal software verification
  • 1 Software and its engineering → Parsers
  • 1 Theory of computation → Grammars and context-free languages

  • Refine by Keyword
  • 1 Dependency Pairs
  • 1 Higher-Order
  • 1 Refinement Types
  • 1 interactive theorem proving
  • 1 top-down parsing

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2011
  • 1 2019

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact