Hypercoercions and a Framework for Equivalence of Cast Calculi
Designing a space-efficient cast representation that is good for both mechanized metatheory and implementation is challenging. Existing solutions (i.e. coercions, threesomes, and supercoercions) are good for one or the other. This paper presents a new cast representation, named hypercoercions, that is good for both. On the way to proving the correctness of hypercoercions, this paper also makes progress on a general framework for proving the correctness of cast representations.
Sat 25 JanDisplayed time zone: Saskatchewan, Central America change
14:00 - 15:05
|Hypercoercions and a Framework for Equivalence of Cast Calculi|
Kuang-Chen Lu Indiana University Bloomington, Jeremy G. Siek Indiana University, USA, Andre Kuhlenschmidt Indiana UniversityPre-print
|Space-Efficient Gradual Typing in Coercion-Passing Style|
Yuya Tsuda Kyoto University, Atsushi Igarashi Kyoto University, Japan, Tomoya Tabuchi Kyoto UniversityPre-print