ECOOP 2022
Mon 6 June - Thu 7 July 2022 Berlin, Germany
Thu 16 Jun 2022 16:45 - 17:15 at Zoom - VCOOP 2 Chair(s): Sophia Drossopoulou

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 of coherence is technically challenging and hard to scale to many common features, including recursion or impredicative polymorphism. Thus, the original formulation of Fi+ does not support the two later features, which creates a gap between theory and practice, since CP fundamentally relies on them.

This paper presents a new formulation of Fi+ based on a type-directed operational semantics (TDOS). The TDOS approach was recently proposed to model the semantics of languages with disjoint intersection types (but without polymorphism). 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 Fi+ indirectly via a target language, the TDOS approach gives a semantics to Fi+ 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 uses only simple reasoning techniques, such as straightforward induction, and is able to easily 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. We formalized the TDOS variant of the Fi+ calculus, together with its type-soundness and determinism proof in the Coq proof assistant.

Thu 16 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:45 - 18:15
VCOOP 2Research Papers at Zoom
Chair(s): Sophia Drossopoulou Facebook and Imperial College London
Direct Foundations for Compositional ProgrammingArtifacts Evaluated - ReusableArtifacts Evaluated - FunctionalVCOOP 2022
Research Papers
Andong Fan Zhejiang University, Xuejing Huang The University of Hong Kong, Han Xu Peking University, Yaozhu Sun University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
Pre-print Media Attached
Experience: Model-Based Feedback-Driven Greybox Fuzzing for Web ApplicationsVCOOP 2022
Research Papers
François Gauthier Oracle Labs, Behnaz Hassanshahi Oracle Labs, Australia, Benjamin Selwyn-Smith Oracle Labs, Trong Nhan Mai Oracle Labs, Max Schlüter Oracle Labs, Micah Williams Oracle
A Self-Dual Distillation of Session Types (Pearl)Artifacts Evaluated - FunctionalVCOOP 2022ECOOP 2022
Research Papers
Jules Jacobs Radboud University Nijmegen