Abstract

The recently proposed CP language adopts Compositional Programming: a new modular programming style that solves challenging problems such as the Expression Problem. CP is implemented on top of a polymorphic core language with disjoint intersection types called Fi+ . The semantics of Fi+ employs an elaboration to a target language and relies on a sophisticated proof technique to prove the coherence of the elaboration. Unfortunately, the proof technique is technically challenging and hard to scale to many common features, including recursion or impredicative polymorphism. Thus, the original formulation of F+i does not support the two later features, which creates a gap between theory and practice, since CP fundamentally relies on them.

The paper presents a new formulation of F+i based on a type-directed operational semantics (TDOS). Our work shows that the TDOS approach can be extended to languages with disjoint polymorphism and model the full Fi+ calculus. Unlike the elaboration semantics, which gives the semantics to F+i indirectly via a target language, the TDOS approach gives a semantics to F+i directly. With a TDOS, there is no need for a coherence proof. Instead, we can simply prove that the semantics is deterministic. The proof of determinism only uses simple reasoning techniques, such as straightforward induction, and is able to handle problematic features such as recursion and impredicative polymorphism. This removes the gap between theory and practice and validates the original proofs of correctness for CP.

This is the practice talk for ECOOP 2022.

Join Zoom Meeting https://hku.zoom.us/j/3037428888 Meeting ID: 303 742 8888