Reference. agdarsec — total parser combinators
Cite
Cited by (2)
Certified, total serialisers with an application to Huffman encoding hinze-2023-certified
The other day, I was assembling lecture material for a course on Agda. Pursuing an application-driven approach, I was looking for correctness proofs of popular algorithms. One of my all-time favourites is Huffman data compression (Huffman, 1952). Even though it is probably safe to assume that you are familiar with this algorithmic gem, a brief reminder of the essential idea may not be amiss.
A type- and scope-safe universe of syntaxes with binding: their semantics and proofs allais-2021-a
The syntax of almost every programming language includes a notion of binder and corresponding bound occurrences, along with the accompanying notions of α-equivalence, capture-avoiding substitution, typing contexts, runtime environments, and so on. In the past, implementing and reasoning about programming languages required careful handling to maintain the correct behaviour of bound variables. Modern programming languages include features that enable constraints like scope safety to be expressed in types. Nevertheless, the programmer is still forced to write the same boilerplate over again for each new implementation of a scope-safe operation (e.g., renaming, substitution, desugaring, printing), and then again for correctness proofs. We present an expressive universe of syntaxes with binding and demonstrate how to (1) implement scope-safe traversals once and for all by generic programming; and (2) how to derive properties of these traversals by generic proving. Our universe description, generic traversals and proofs, and our examples have all been formalised in Agda and are available in the accompanying material available online at https://github.com/gallais/generic-syntax .
Cites 17 works (4 here)
With notes (4)
Validating LR(1) Parsers jourdanValidatingLRParsers2012
An LR(1) parser is a finite-state automaton, equipped with a stack, which uses a combination of its current state and one lookahead symbol in order to determine which action to perform next. We present a validator which, when applied to a context-free grammar G and an automaton A, checks that A and G agree. Validating the parser provides the correctness guarantees required by verified compilers and other high-assurance software that involves parsing. The validation process is independent of which technique was used to construct A. The validator is implemented and proved correct using the Coq proof assistant. As an application, we build a formally-verified parser for the C99 language.
Total parser combinators danielssonTotalParserCombinators2010
A monadic parser combinator library which guarantees termination of parsing, while still allowing many forms of left recursion, is described. The library’s interface is similar to those of many other parser combinator libraries, with two important differences: one is that the interface clearly specifies which parts of the constructed parsers may be infinite, and which parts have to be finite, using dependent types and a combination of induction and coinduction; and the other is that the parser type is unusually informative.
The library comes with a formal semantics, using which it is proved that the parser combinators are as expressive as possible. The implementation is supported by a machine-checked correctness proof.
Applicative programming with effects mcbride-2008-applicative
In this article, we introduce Applicative functors – an abstract characterisation of an applicative style of effectful programming, weaker than Monads and hence more widespread. Indeed, it is the ubiquity of this programming pattern that drew us to the abstraction. We retrace our steps in this article, introducing the applicative pattern by diverse examples, then abstracting it to define the Applicative type class and introducing a bracket notation that interprets the normal application syntax in the idiom of an Applicative functor. Furthermore, we develop the properties of applicative functors and the generic operations they support. We close by identifying the categorical structure of applicative functors and examining their relationship both with Monads and with Arrow.
Derivatives of Regular Expressions brzozowskiDerivativesRegularExpressions1964
Kleene’s regular expressions, which can be used for describing sequential circuits, were defined using three operators (union, concatenation and iterate) on sets of sequences. Word descriptions of problems can be more easily put in the regular expression language if the language is enriched by the inclusion of other logical operations. However, in the problem of converting the regular expression description to a state diagram, the existing methods either cannot handle expressions with additional operators, or are made quite complicated by the presence of such operators.In this paper the notion of a derivative of a regular expression is introduced and the properties of derivatives are discussed. This leads, in a very natural way, to the construction of a state diagram from a regular expression containing any number of logical operators.
External (13)
- Certified context-free parsing: A formalisation of Valiant's algorithm in Agda (2016)
- Nom, a byte oriented, streaming, zero copy, parser combinators library in rust (2015)
- Guarded recursive types in type theory (2015)
- Copatterns: programming infinite structures by observations (2013)
- Idris, a general-purpose dependently typed programming language: Design and implementation (2013)
- Dependent type providers (2013)
- The CompCert veri ed compiler (2012)
- Dependently typed programming in Agda (2009)
- Parser combinators in Scala (2008)
- The Coq proof assistant reference manual (2004)
- Monadic parsing in Haskell (1998)
- Building domain-specific embedded languages (1996)
- How to replace failure by a list of successes (1985)