Session Type Inference in Haskell

Abstract

We present an inference system for a version of the Pi-calculus in Haskellfor the session type proposed by Honda et al. The session type is very usefulin checking if the communications are well-behaved. The full session typeimplementation in Haskell was first presented by Pucella and Tov, which is'semi-automatic' in that the manual operations for the type representation wasnecessary. We give an automatic type inference for the session type by using amore abstract representation for the session type based on the 'de Bruijnlevels'. We show an example of the session type inference for a simple SMTPclient.