A Verified LL(1) Parser Generator

DOI10.4230/LIPICS.ITP.2019.24MaRDI QIDQ5875434zbMATH OpenOpenAlexFDO

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

Publication date 3 February 2023

Full work available at URL https://drops.dagstuhl.de/opus/volltexte/2019/11079/pdf/LIPIcs-ITP-2019-24.pdf/

zbMATH Keywords

interactive theorem provingtop-down parsing

Mathematics Subject Classification ID

Cites work

• scientific article; zbMATH DE number 5277949 (Why is no real title available?)
• scientific article; zbMATH DE number 1027560 (Why is no real title available?)
• A theory of type polymorphism in programming
• Extraction in Coq: An Overview
• Mechanized semantics for the clight subset of the C language
• Parsing expression grammars: a recognition-based syntactic foundation
• Program-ing finger trees in Coq
• TRX: a formally verified parser interpreter
• Validating LR(1) Parsers
• Verified, Executable Parsing

Cited in

(1)

• Validating LR(1) Parsers

Describes a project that uses

Uses Software

• ML
• Coq

This page was built for publication: A Verified LL(1) Parser Generator

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5875434)