A Polymorphic Type System for Staged Exceptions Seminars/Workshops

Abstract

I will present our on-going work on a type and effect system for a let-polymorphic multi-staged language with exceptions. The proposed type and effect system checks if we safely synthesize complex controls with exceptions in multi-staged programming. The proposed exception constructs in multi-staged programming has no artificial restriction. Exception-raise and -handle expressions can appear in expressions of any stage. Exceptions can be raised during code composition and may escape stages and can be handled only at stage 0. Our effect type system support such features. Our system guarantees that empty effect means the input program has no uncaught exceptions during its execution.

This is a joint work with Kwangkeun Yi and Ik-Soon Kim.