Expressiveness of subtyped pi-calculus

Romain Demangeon

Subtyping allows one to give a program a type that is more inclusive that its original type. Subtyping has been well-studied for sequential programming, for both functional and imperative programs. I present a form of subtyping for distributed applications interacting with messages: subtyping stems from the ability to be able to offer a larger choice of options of communication to another party.

I use a concise subtyped pi-calculus as a formal language and study its expressiveness through the fully abstract encodings of both a subtyped lambda-calculus and a session-calculus.