FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
A Unifying Framework for Type Inhabitation

Authors: Sandra Alves and Sabine Broda

Paper Information

Title:A Unifying Framework for Type Inhabitation
Authors:Sandra Alves and Sabine Broda
Proceedings:FSCD Presented Papers
Editor: Helene Kirchner
Keywords:simple types, type inhabitation, rewriting, PSPACE
Abstract:

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.

Pages:16
Talk:Jul 10 11:00 (Session 54B: Types)
Paper: