Intersection Types for Unboundedness Problems

Intersection Types for Unboundedness Problems

Intersection types have been originally developed as an extension of simple types, but they can also be used for refining simple types. In this survey we concentrate on the latter option; more precisely, on the use of intersection types for describing quantitative properties of simply typed lambda-t...

Full description

Bibliographic Details
Main Author: Paweł Parys
Format: Article
Language:English
Published: Open Publishing Association 2019-04-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1904.10105v1
id doaj-e07c9d6ceddc40d6a992e0b8b1a9b6d6
record_format Article
spelling doaj-e07c9d6ceddc40d6a992e0b8b1a9b6d62020-11-25T01:36:21ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802019-04-01293Proc. DCM 2018 and ITRS 201872710.4204/EPTCS.293.2:1Intersection Types for Unboundedness ProblemsPaweł Parys0 Institute of Informatics, University of Warsaw Intersection types have been originally developed as an extension of simple types, but they can also be used for refining simple types. In this survey we concentrate on the latter option; more precisely, on the use of intersection types for describing quantitative properties of simply typed lambda-terms. We present two type systems. The first allows to estimate (by appropriately defined value of a derivation) the number of appearances of a fixed constant 'a' in the beta-normal form of a considered lambda-term. The second type system is more complicated, and allows to estimate the maximal number of appearances of the constant 'a' on a single branch.http://arxiv.org/pdf/1904.10105v1
collection DOAJ
language English
format Article
sources DOAJ
author Paweł Parys
spellingShingle Paweł Parys
Intersection Types for Unboundedness Problems
Electronic Proceedings in Theoretical Computer Science
author_facet Paweł Parys
author_sort Paweł Parys
title Intersection Types for Unboundedness Problems
title_short Intersection Types for Unboundedness Problems
title_full Intersection Types for Unboundedness Problems
title_fullStr Intersection Types for Unboundedness Problems
title_full_unstemmed Intersection Types for Unboundedness Problems
title_sort intersection types for unboundedness problems
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2019-04-01
description Intersection types have been originally developed as an extension of simple types, but they can also be used for refining simple types. In this survey we concentrate on the latter option; more precisely, on the use of intersection types for describing quantitative properties of simply typed lambda-terms. We present two type systems. The first allows to estimate (by appropriately defined value of a derivation) the number of appearances of a fixed constant 'a' in the beta-normal form of a considered lambda-term. The second type system is more complicated, and allows to estimate the maximal number of appearances of the constant 'a' on a single branch.
url http://arxiv.org/pdf/1904.10105v1
work_keys_str_mv AT pawełparys intersectiontypesforunboundednessproblems
_version_ 1725063497822240768

Similar Items