License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2021.14
URN: urn:nbn:de:0030-drops-134481
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13448/
Go to the corresponding LIPIcs Volume Portal

Broda, Sabine

Pregrammars and Intersection Types

pdf-format:
LIPIcs-CSL-2021-14.pdf (0.6 MB)

Abstract

A representation of intersection types in terms of pregrammars is presented. Pregrammar based rewriting relations, corresponding respectively to type checking and inhabitation are defined and the latter is used to implement a Wajsberg/Ben-Yelles style alternating semi-decision algorithm for inhabitation. The usefulness of the framework is illustrated by revisiting and partially extending standard inhabitation related results for intersection types, as well as establishing new ones. It is shown how the notion of bounded multiset dimension emerges naturally and the relation between the two settings is clarified. A meaningful rank independent superset of the set of rank 2 types is identified for which EXPSPACE-completeness for inhabitation as well as for counting is proved. Finally, a standard result on negatively non-duplicated simple types is extended to intersection types.

BibTeX - Entry

@InProceedings{broda:LIPIcs:2021:13448,
  author =	{Sabine Broda},
  title =	{{Pregrammars and Intersection Types}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{14:1--14:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Christel Baier and Jean Goubault-Larrecq},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/13448},
  URN =		{urn:nbn:de:0030-drops-134481},
  doi =		{10.4230/LIPIcs.CSL.2021.14},
  annote =	{Keywords: Intersection Types, Pregrammars, Inhabitation}
}

Keywords: Intersection Types, Pregrammars, Inhabitation
Collection: 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)
Issue Date: 2021
Date of publication: 13.01.2021

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI