A Type Theoretic Treatment of Context-Free Languages Without Mutual Recursion

None, None; None, None

A Type Theoretic Treatment of Context-Free Languages Without Mutual Recursion

Conference Paper (2025)

Author(s)

Jaro Reinders (TU Delft - Programming Languages)

Casper Bach (University of Southern Denmark)

Research Group

Programming Languages

DOI related publication

https://doi.org/10.1007/978-3-031-99751-8_12

Parsing Type theory Formal languages

To reference this document use:

https://resolver.tudelft.nl/uuid:a72e4f4d-a42a-4ea6-86a1-39ae895908f0

More Info

expand_more

Publication Year

2025

Language

English

Research Group

Programming Languages

Bibliographical Note

Green Open Access added to TU Delft Institutional Repository as part of the Taverne amendment. More information about this copyright law amendment can be found at https://www.openaccess.nl. Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public. @en

Volume number

15652

Pages (from-to)

283-301

ISBN (print)

978-3-031-99750-1

ISBN (electronic)

978-3-031-99751-8

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Abstract

Parsing is the process of recovering structure from strings, an essential part of implementing programming languages. Previous work has shown that formalizing languages and parsers using an idiomatic type theoretic approach can be simple and enlightening. Unfortunately, this approach has only been applied to regular languages, which are not expressive enough for many practical applications. We have extended the type theoretic formalization to context-free languages (without mutual recursion) which are substantially more expressive. We hope our formalization can serve as a foundation for reasoning about new disambiguation techniques and even more expressive formalisms such as data-dependent grammars.

Files

978-3-031-99751-8_12.pdf

(pdf | 0.923 Mb)

License info not available

File under embargo until 04-05-2026