DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2021.14

Pregrammars and Intersection Types

Authors: Sabine Broda

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

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.

Cite as

Sabine Broda. Pregrammars and Intersection Types. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 14:1-14:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{broda:LIPIcs.CSL.2021.14,
  author =	{Broda, Sabine},
  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 =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.14},
  URN =		{urn:nbn:de:0030-drops-134481},
  doi =		{10.4230/LIPIcs.CSL.2021.14},
  annote =	{Keywords: Intersection Types, Pregrammars, Inhabitation}
}

Document

DOI: 10.4230/LIPIcs.FSCD.2018.5

A Unifying Framework for Type Inhabitation

Authors: Sandra Alves and Sabine Broda

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract

In this paper we define a framework to address different kinds of problems related to type inhabitation, such as type checking, the emptiness problem, generation of inhabitants and counting, in a uniform way. Our framework uses an alternative representation for types, called the pre-grammar of the type, on which different methods for these problems are based. Furthermore, we define a scheme for a decision algorithm that, for particular instantiations of the parameters, can be used to show different inhabitation related problems to be in PSPACE.

Cite as

Sandra Alves and Sabine Broda. A Unifying Framework for Type Inhabitation. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{alves_et_al:LIPIcs.FSCD.2018.5,
  author =	{Alves, Sandra and Broda, Sabine},
  title =	{{A Unifying Framework for Type Inhabitation}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{5:1--5:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.5},
  URN =		{urn:nbn:de:0030-drops-91758},
  doi =		{10.4230/LIPIcs.FSCD.2018.5},
  annote =	{Keywords: simple types, type inhabitation, rewriting, PSPACE}
}

Search Results

Documents authored by Broda, Sabine

Pregrammars and Intersection Types

Abstract

Cite as

A Unifying Framework for Type Inhabitation

Abstract

Cite as

Thanks for your feedback!

Could not send message