Pregrammars and Intersection Types

• Type: Article in International Conference Proceedings Book
• Date: 2021

Authors

Broda, S (Author) FCUP

Conference proceedings International

Title: 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25-28, 2021, Ljubljana, Slovenia (Virtual Conference).

Initial page: 14:1

29th EACSL Annual Conference on Computer Science Logic, CSL 2021

25 January 2021 through 28 January 2021

Indexing

Scopus - 0 Citations

Scientific classification

FOS: Natural sciences

CORDIS: Technological sciences

FOS: Natural sciences > Computer and information sciences ; Natural sciences > Mathematics

Other information

Authenticus ID: P-00T-D5A

DOI: 10.4230/lipics.csl.2021.14

Abstract (EN): 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. © Sabine Broda.

Language: English

Type (Professor's evaluation): Scientific