Locations and session types in a language with higher-order reflection

We propose the localised ρ-calculus, a process calculus that uses an identification of processes and names in higher-order communication along with a notion of locations. These are named, bounded areas for computation, organised in a hierarchy, and processes can move from one to another by crossing their boundaries. Process migration becomes higher-order communication. To control the usage of channels we develop a type system with binary session types for the localised ρ-calculus, based on work by Giunti and Vasconcelos, and prove that it is sound.