2 Search Results for "Broda, Sabine"

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-dev.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-dev.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}
}
  • Refine by Author
  • 2 Broda, Sabine
  • 1 Alves, Sandra

  • Refine by Classification
  • 2 Theory of computation → Lambda calculus
  • 2 Theory of computation → Type theory
  • 1 Theory of computation → Logic
  • 1 Theory of computation → Rewrite systems

  • Refine by Keyword
  • 1 Inhabitation
  • 1 Intersection Types
  • 1 PSPACE
  • 1 Pregrammars
  • 1 rewriting
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2018
  • 1 2021

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact