Language Primitives and Type Discipline for Structured Communication-Based Programming, Subject Reduction and Type Safety Theorems
Session primitives and types provide a flexible programming style for structural interaction, and are used to statically check the safe and consistent composition of protocols in communication-centric distributed software. Unfortunately authors working on session types have recently realised that so...
| Autor principal: | |
|---|---|
| Outros Autores: | |
| Formato: | report |
| Idioma: | por |
| Publicado em: |
2009
|
| Texto completo: | http://hdl.handle.net/10451/14108 |
| País: | Portugal |
| Oai: | oai:repositorio.ul.pt:10451/14108 |
| Resumo: | Session primitives and types provide a flexible programming style for structural interaction, and are used to statically check the safe and consistent composition of protocols in communication-centric distributed software. Unfortunately authors working on session types have recently realised that some of the previously published systems fail to satisfy the basic theorems of Subject Reduction and Type Safety. This report discusses the issues involved in higher-order session communication, presents a formulation of the recursive types as well as proofs of the Subject Reduction and Type Safety Theorems of the original session typing system by Honda-Vasconcelos-Kubo in ESOP'98. It also proposes a new session typing system which allows a more liberal higher-order session communication based on an idea of Gay and Hole. |
|---|