Abstract. This paper presents a polymorphic type system for a language with delimited control operators, shift and reset. Based on the monomorphic type system by Danvy and Filinski...
In this paper, we propose a new proof method for strong normalization of calculi with control operators, and, by this method, we prove strong normalization of the system
We present a method of lifting to explicit substitution calculi some characterizations of the strongly normalizing terms of λ-calculus by means of intersection type systems. The m...
This paper presents simple, syntactic strong normalization proofs for the simply-typed -calculus and the polymorphic -calculus (system F) with the full set of logical connectives, ...