|
Stefan Sokolowski
Intersection of functional subset types
825
Abstract
It is shown that, under reasonable assumptions, the intersection of a
family of functional subset types expressible in the language
described in``Hindley-Milner
for dependent and subset types'' by Sokolowski and Wadler (with a
few modifications) is a functional subset type. Such intersections
are necessary to type lambda-terms without explicit type
annotations, so it is good to know that the whole fits into a single
framework.
|
|
 |
 |
