DROPS

Document

DOI: 10.4230/LIPIcs.ITP.2023.27

POSIX Lexing with Bitcoded Derivatives

Authors: Chengsong Tan and Christian Urban

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract

Sulzmann and Lu describe a lexing algorithm that calculates Brzozowski derivatives using bitcodes annotated to regular expressions. Their algorithm generates POSIX values which encode the information of how a regular expression matches a string - that is, which part of the string is matched by which part of the regular expression. This information is needed in the context of lexing in order to extract and to classify tokens. The purpose of the bitcodes is to generate POSIX values incrementally while derivatives are calculated. They also help with designing an "aggressive" simplification function that keeps the size of derivatives finitely bounded. Without simplification the size of some derivatives can grow arbitrarily big, resulting in an extremely slow lexing algorithm. In this paper we describe a variant of Sulzmann and Lu’s algorithm: Our variant is a recursive functional program, whereas Sulzmann and Lu’s version involves a fixpoint construction. We (i) prove in Isabelle/HOL that our variant is correct and generates unique POSIX values (no such proof has been given for the original algorithm by Sulzmann and Lu); we also (ii) establish finite bounds for the size of our derivatives.

Cite as

Chengsong Tan and Christian Urban. POSIX Lexing with Bitcoded Derivatives. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 27:1-27:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{tan_et_al:LIPIcs.ITP.2023.27,
  author =	{Tan, Chengsong and Urban, Christian},
  title =	{{POSIX Lexing with Bitcoded Derivatives}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{27:1--27:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.27},
  URN =		{urn:nbn:de:0030-drops-184027},
  doi =		{10.4230/LIPIcs.ITP.2023.27},
  annote =	{Keywords: POSIX matching and lexing, derivatives of regular expressions, Isabelle/HOL}
}

Document

DOI: 10.4230/LIPIcs.ECOOP.2017.5

Modelling Homogeneous Generative Meta-Programming

Authors: Martin Berger, Laurence Tratt, and Christian Urban

Published in: LIPIcs, Volume 74, 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract

Homogeneous generative meta-programming (HGMP) enables the generation of program fragments at compile-time or run-time. We present a foundational calculus which can model both compile-time and run-time evaluated HGMP, allowing us to model, for the first time, languages such as Template Haskell. The calculus is designed such that it can be gradually enhanced with the features needed to model many of the advanced features of real languages. We demonstrate this by showing how a simple, staged type system as found in Template Haskell can be added to the calculus.

Cite as

Martin Berger, Laurence Tratt, and Christian Urban. Modelling Homogeneous Generative Meta-Programming. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 5:1-5:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{berger_et_al:LIPIcs.ECOOP.2017.5,
  author =	{Berger, Martin and Tratt, Laurence and Urban, Christian},
  title =	{{Modelling Homogeneous Generative Meta-Programming}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{5:1--5:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{M\"{u}ller, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.5},
  URN =		{urn:nbn:de:0030-drops-72775},
  doi =		{10.4230/LIPIcs.ECOOP.2017.5},
  annote =	{Keywords: Formal Methods, Meta-Programming, Operational Semantics, Types, Quasi-Quotes, Abstract Syntax Trees}
}

Search Results

Documents authored by Urban, Christian

POSIX Lexing with Bitcoded Derivatives

Abstract

Cite as

Modelling Homogeneous Generative Meta-Programming

Abstract

Cite as

Thanks for your feedback!

Could not send message