To support a proposed extension of constructor unboxing in OCaml, we need to compute a property of OCaml type expressions by repeatedly unfolding the definition of datatype constructors. In presence of mutually-recursive datatype definitions, it is not obvious to do such repeated unfolding without losing termination. We present an unfolding algorithm using dynamic cycle detection, which is more permissive than the traditional static cycle detection approach.
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