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 Jan Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change
|14:00 - 14:32|
Kuang-Chen LuIndiana University Bloomington, Jeremy G. SiekIndiana University, USA, Andre KuhlenschmidtIndiana UniversityPre-print
|14:32 - 15:05|