Past Meeting Notes
- Apr 3 - Meeting
- Apr 9 - Seminar
- Apr 10 - Meeting
- Apr 17 - Meeting
- Apr 30 - Meeting
- May 5 - Notes
- May 15 - Meeting
Wild Ideas
-
Use a identify function encoding seen in F-ing modules, to encode the reflexivity constraint in iso-recursive subtyping, mutual subtyping? unfolding lemma?
-
Use the translation based model for iso-recursive subtyping (along with results in distributivity), to address the problem of subtyping in session types (along with distributivity over choice/receive operators)
-
Modularity in Process calculus
Although it is straightforward to add a type system to channel-based languages, adding a type system to actor languages is less straightforward, as process names (process IDs or PIDs) must be parameterised by a type that supports all messages that can be received. The type is therefore less precise, requiring subtyping [He et al. 2014] or synchronisation [de Boer et al. 2007; Tasharofi et al. 2013] to avoid a total loss of modularity [Fowler et al. 2017].
-
Bitmaps as free variables to well scoped de brujns seminar
-
Logical relation for type soundness for merge operator seminar
- (free from consistency, runtime subtyping, help find more correct rules)