A Verified LL(1) Parser Generator

DOI10.4230/LIPICS.ITP.2019.24OpenAlexW2978834141MaRDI QIDQ5875434FDOQ5875434

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

• A theory of type polymorphism in programming
• Mechanized semantics for the clight subset of the C language
• TRX: a formally verified parser interpreter
• Verified, Executable Parsing
• Title not available (Why is that?)
• Validating LR(1) Parsers
• Parsing expression grammars: a recognition-based syntactic foundation
• Program-ing finger trees in Coq
• Title not available (Why is that?)
• Extraction in Coq: An Overview

Cited In (1)

• Validating LR(1) Parsers

Uses Software

• Coq
• ML

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)