Type abstraction, the phase distinction, and computational effects all play an important role in the design and implementation of ML-style module systems. We propose a simple type theoretic metalanguage φML for multi-phase modularity in which these concepts are treated individually, supporting the definition of high-level modular constructs such as generative and applicative functors, as well as all extant forms of structure sharing.
Thu 26 AugDisplayed time zone: Seoul change
23:30 - 01:00
|A metalanguage for multi-phase modularity|
|Unfolding ML datatype declarations without loops|
MLPre-print Media Attached
|Verifying Multiparty Communication Protocols using ML Type Systems|
Keigo Imai Gifu University, Rumyana Neykova Brunel University London, Nobuko Yoshida Imperial College London, Shoji Yuen Nagoya UniversityFile Attached