Computing at Glasgow University
Paper ID: 6963
DCS Tech Report Number: TR-2003-132

Bounded Polymorphism in Session Types
Hole,M.J. Gay,S.J.

Publication Type: Tech Report (internal)
Appeared in: DCS Tech Report
Page Numbers :
Publisher: Dept of Computing Science, University of Glasgow
Year: 2003

We review work on session types and the pi-calculus, and give an example identifying a use for bounded polymorphic types in this setting. We then define a variant of the pi-calculus with the appropriate syntax, and propose a static bounded polymorphic type system, for which we prove type soundness. We use our rules to give a typing derivation and show the sequence of reductions in our example. Finally, we discuss related work and possible future work in this area.

Keywords: Types, pi calculus, session types, polymorphism, protocol verification

PDF Bibtex entry Endnote XML