Write a Blog >>
Sat 25 Jan 2020 14:00 - 14:32 at Orleans - Coercions Chair(s): Jeremy G. Siek

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 Jan
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

14:00 - 15:05: WGT - Coercions at Orleans
Chair(s): Jeremy G. SiekIndiana University, USA
wgt-2020-papers14:00 - 14:32
Kuang-Chen LuIndiana University Bloomington, Jeremy G. SiekIndiana University, USA, Andre KuhlenschmidtIndiana University
wgt-2020-papers14:32 - 15:05
Yuya TsudaKyoto University, Atsushi IgarashiKyoto University, Japan, Tomoya TabuchiKyoto University