On Stratified Regions

Type and effect systems are a tool to analyse statically the behaviour of programs with effects. We present a proof based on the so called reducibility candidates that a suitable stratification of the type and effect system entails the termination of the typable programs. The proof technique covers a simply typed, multi-threaded, call-by-value lambda-calculus, equipped with a variety of scheduling (preemptive, cooperative) and interaction mechanisms (references, channels, signals). Keywords Types and effects. Termination. Reducibility candidates.

• Type: Conference
• Year: 2009
• Where: APLAS
• Authors: Roberto M. Amadio
• Keywords: APLAS 2009, Effect System, Programming Languages, Reducibility Candidates, Suitable Stratification