arXiv subjects
Publications and source records attributed to Karim Nour.
In this paper, we extend the system AF2 in order to have the subject reduction for the $βη$-reduction. We prove that the types with positive quantifiers are complete for models that are stable by weak-head expansion.
In this paper, we present an extension of $λμ$-calculus called $λμ^{++}$-calculus which has the following properties: subject reduction, strong normalization, unicity of the representation of data and thus confluence only on data types. This calculus allows also to program the parallel-or.
We prove in this paper that the types of system F inhabited uniquely by ?I-terms (the I-types) have a positive quantifier. We give also consequences of this result and some examples.