TL;DR
This paper introduces a new type-directed operational semantics for Fi+ that supports recursion and impredicative polymorphism, simplifying proofs and bridging the gap between theoretical foundations and practical implementation of the CP language.
Contribution
It extends the TDOS approach to model the full Fi+ calculus, eliminating the need for complex coherence proofs and supporting features like recursion and impredicative polymorphism.
Findings
TDOS supports full Fi+ calculus with polymorphism and recursion
Simplifies proofs by establishing determinism of semantics
Formalized in Coq, validating the approach
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 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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
