Reference. ACGtk: A toolkit for developing and running abstract categorial grammars
Cite
Cited by (1)
Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus intrinsic-verification-of-parsers
We present Dependent Lambek Calculus (Lambek), a domain-specific dependent type theory for verified parsing and formal grammar theory. In Lambek, linear types are used as a syntax for formal grammars, and parsers can be written as linear terms. The linear typing restriction provides a form of intrinsic verification that a parser yields only valid parse trees for the input string. We demonstrate the expressivity of this system by showing that the combination of inductive linear types and dependency on non-linear data can be used to encode commonly used grammar formalisms such as regular and context-free grammars as well as traces of various types of automata. Using these encodings, we define parsers for regular expressions using deterministic automata, as well as examples of verified parsers of context-free grammars.
We present a denotational semantics of our type theory that interprets the linear types as functions from strings to sets of abstract parse trees and terms as parse transformers. Based on this denotational semantics, we have made a prototype implementation of Lambek using a shallow embedding in the Agda proof assistant. All of our examples parsers have been implemented in this prototype implementation.
Cites 32 works (1 here)
External (31)
- Applicative Abstract Categorial Grammars in Full Swing (2017)
- A syntax-semantics interface for Tree-Adjoining Grammars through Abstract Categorial Grammars (2017)
- Parsing and generation as datalog query evaluation (Kanazawa, IfCoLog J.) (2017)
- Discourse modeling with abstract categorial grammars (Maskharashvili, PhD thesis) (2016)
- Abstract Categorial Parsing as Linear Logic Programming (2015)
- Applicative Abstract Categorial Grammar (2015)
- A generalized view on parsing and translation (Koller, Kuhlmann, IWPT 2011) (2011)
- Grammatical Framework: Programming with Multilingual Grammars (Ranta) (2011)
- Second-Order Abstract Categorial Grammars as Hyperedge Replacement Grammars (2009)
- A prefix-correct Earley recognizer for multiple context-free grammars (Kanazawa, TAG+9) (2008)
- Parsing and generation as datalog queries (Kanazawa, ACL 2007) (2007)
- Generating control languages with abstract categorial grammars (Kanazawa, Salvati, FG 2007) (2007)
- Encoding second order string ACG with deterministic tree walking transducers (Salvati, FG 2006) (2006)
- The complexity and generative capacity of lexicalized abstract categorial grammars (2005)
- Problèmes de filtrage et problèmes d'analyse pour les grammaires catégorielles abstraites (Salvati, PhD thesis) (2005)
- Vector addition tree automata (2004)
- On the Expressive Power of Abstract Categorial Grammars: Representing Context-Free Formalisms (2004)
- Continuations and the Nature of Quantification (2002)
- Tree-adjoining grammars as abstract categorial grammars (de Groote, TAG+6) (2002)
- Towards abstract categorial grammars (2001)
- Linear higher-order matching is NP-complete (2000)
- Proof-search in implicative linear logic as a matching problem (2000)
- The Zipper (1997)
- Tree-Adjoining Grammars (1997)
- Foundations of Databases (Abiteboul, Hull, Vianu) (1995)
- Principles of Database and Knowledge-Base Systems, Volume II (Ullman) (1990)
- Characterizing mildly context-sensitive grammar formalisms (Weir, PhD thesis) (1988)
- Characterizing structural descriptions produced by various grammatical formalisms (1987)
- Tree adjunct grammars (1975)
- The Proper Treatment of Quantification in Ordinary English (1973)
- Some logical aspects of grammatical structure (1961)