Session types

Session types for the π-calculus: binary protocols and their duality, linear endpoint typing with ownership contexts, subject reduction, progress by priorities, typing up to protocol equivalence, and shared and recursive services.

• Finite binary sessions
• Linear endpoint typing for the π-calculus
• Subject reduction for endpoint typing
• Global progress for session typing with priorities
• Session typing up to protocol equivalence
• Session typing with shared services
• Recursive sessions through replicated services

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.