Title:	Construction of a Type System for Layered Control Operators
	(in Japanese)
Authors: Terunobu Suzuki and Yukiyoshi Kameyama
Affiliation: Department of Computer Science,
	     Graduate School of Systems and Information Engineering, 
	     University of Tsukuba

Abstract:

We construct a type system for control operators in functional programming 
languages. Specifically, we study the layered version of the control 
operators shift and reset whose semantics is defined in terms of (iterated) 
CPS translations. While shift and reset are capable of representing 
various control structures, we cannot have two or more different uses 
of shift and reset in a single program since they may interfere with each 
other. In order to avoid this interference, shift and reset should be 
layered, that is, we should assign to each occurrence of shift and reset
a natural number which designates its level.

Although it is apparent that a sound type system for layered shift and
reset is necessary to introduce them to practical programming languages, 
no work has ever tried to construct a sufficiently expressive type system 
for them. In this paper we refine our previous work which solved this 
problem for the case of level-2, and propose a type system for an arbitrary 
level. We show that desirable properties such as type soundness hold for 
this type system, which enables one to introduce the layered shift and 
reset to statically typed programming languages.