Reference. Type Logics in Grammar

Wojciech Buszkowski · Trends in Logic · 2003 · categorial-grammar · DOI

Cite
Cite as @buszkowskiTypeLogicsGrammar2003 (helia, typst) · \cite{buszkowskiTypeLogicsGrammar2003} (LaTeX)
BibTeX
bibtex · 17 lines
@incollection{buszkowskiTypeLogicsGrammar2003,
 title = {Type {Logics} in {Grammar}},
 author = {Buszkowski, W.},
 year = {2003},
 isbn = {978-90-481-6414-1 978-94-017-3598-8},
 doi = {10.1007/978-94-017-3598-8_12},
 url = {http://link.springer.com/10.1007/978-94-017-3598-8_12},
 urldate = {2024-08-07},
 booktitle = {Trends in {Logic}},
 editor = {Wójcicki, Ryszard and Mundici, Daniele and Orłowska, Ewa and Priest, Graham and Segerberg, Krister and Urquhart, Alasdair and Wansing, Heinrich and Hendricks, Vincent F. and Malinowski, Jacek},
 volume = {21},
 pages = {337--382},
 publisher = {Springer Netherlands},
 address = {Dordrecht},
 note = {Series Title: Trends in Logic},
 language = {en}
}
hayagriva YAML (typst)
yaml · 30 lines
buszkowskiTypeLogicsGrammar2003:
  type: anthos
  title: Type {Logics} in {Grammar}
  author: Buszkowski, W.
  date: 2003
  editor:
  - Wójcicki, Ryszard
  - Mundici, Daniele
  - Orłowska, Ewa
  - Priest, Graham
  - Segerberg, Krister
  - Urquhart, Alasdair
  - Wansing, Heinrich
  - Hendricks, Vincent F.
  - Malinowski, Jacek
  page-range: 337-382
  url:
    value: http://link.springer.com/10.1007/978-94-017-3598-8_12
    date: 2024-08-07
  serial-number:
    doi: 10.1007/978-94-017-3598-8_12
    isbn: 978-90-481-6414-1 978-94-017-3598-8
  note: 'Series Title: Trends in Logic'
  parent:
    type: anthology
    title: Trends in {Logic}
    publisher:
      name: Springer Netherlands
      location: Dordrecht
    volume: 21
Download: buszkowskiTypeLogicsGrammar2003.bib · buszkowskiTypeLogicsGrammar2003.yml
Cited by (1)

Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus intrinsic-verification-of-parsersPLDI · 2025

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.

PDF · DOI · arXiv (extended version) · Source code · pldb
Cites 83 works (3 here)
With notes (3)

Action logic and pure induction prattActionLogicPure1991Logics in AI · 1991
In Floyd-Hoare logic, programs are dynamic while assertions are static (hold at states). In action logic the two notions become one, with programs viewed as on-the-fly assertions whose truth is evaluated along intervals instead of at states. Action logic is an equational theory ACT conservatively extending the equational theory REG of regular expressions with operations preimplication a→b (had a then b) and postimplication b←a (b if-ever a). Unlike REG, ACT is finitely based, makes a∗ reflexive transitive closure, and has an equivalent Hilbert system. The crucial axiom is that of pure induction, (a→a)∗ = a→a.
DOI

Linear logic girard_linear_1987TCS · 1987
The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality “of course” which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.
DOI

The mathematics of sentence structure lambek58Amer. Math. Monthly · 1958
DOI
External (80)
buszkowskiTypeLogicsGrammar2003 reference entries/refs/buszkowskiTypeLogicsGrammar2003/buszkowskiTypeLogicsGrammar2003.hel