Andrés Viso

Encoding Tight Typing in a Unified Framework

2021 · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)

This paper explores how the intersection type theories of call-by-name (CBN) and call-by-value (CBV) can be unified in a more general framework provided by call-by-push-value (CBPV). Indeed, we propose tight type systems for CBN and …