effects-as-sessions icon indicating copy to clipboard operation
effects-as-sessions copied to clipboard

Published 20 hours ago • verified publisher icon dorchard
→

Metadata

Formalised embedding of an imperative language with effect system into session-typed pi calculus.

This code is a formalisation in Agda that accompanies the paper "Using session types as an effect system" by Orchard and Yoshida in PLACES 2015.

Mainly this is contained in the places15 directory. Appendix B of the paper gives some explanation.

← Metadata

27
Stars
2
Forks
Watchers

Owner

verified publisher icon dorchard

Metadata

Formalised embedding of an imperative language with effect system into session-typed pi calculus.

Back