|Title:||Intersection types for explicit substitution with resource control||Conference:||Sixth Workshop on Intersection Types and Related Systems (ITRS 2012)||Issue Date:||2012||URL:||https://iris.unito.it/retrieve/handle/2318/133236/178883/main_itrs_2012.pdf||Abstract:||
We propose an intersection type assignment system for a term calculus with explicit substitution and resource control, which is due to the presence of weakening and contraction operators. The main contribution is the complete characterisation of strong normalisation of reductions using a combination of well-orders and suitable embeddings of terms as well as head subject expansion.
Show full item record
checked on Jan 30, 2023
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.