Inference of Session Types From Control Flow

This is a study of a technique for deriving the session type of a program written in a statically typed imperative language from its control flow. We impose on our unlabelled session type syntax a well-formedness constraint based upon normalisation and explore the effects thereof. We present our inference algorithm declaratively and in a form suitable for implementation, and illustrate it with examples. We then present an implementation of the algorithm using a program analysis and transformation toolkit.

• Type: Journal
• Year: 2010
• Where: ENTCS
• Authors: Peter Collingbourne, Paul H. J. Kelly
• Keywords: ENTCS 2010, Information Technology, Session Type, Statically Typed, Unlabelled Session Type