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.
-
Notifications
You must be signed in to change notification settings - Fork 1
dorchard/effects-as-sessions
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
Formalised embedding of an imperative language with effect system into session-typed pi calculus.
Resources
Stars
Watchers
Forks
Releases
No releases published