在统一框架中编码严格类型
Encoding Tight Typing in a Unified Framework
摘要：
本文探讨了如何将按名称调用（CBN）和按值调用（CBV）的交集类型论统一到按推值调用（CBPV）提供的更一般的框架中。事实上，我们提出了紧类型系统的CBN和CBV都可以编码在一个独特的紧类型系统CBPV。所有这些系统都是定量的，即。它们提供了关于归一化序列到范式的长度以及这些范式的大小的精确信息。此外，减少序列的长度根据其乘法和指数性质，从线性逻辑继承的概念进行区分。最后但并非最不重要的是，可以从CBPV中相应的编码中提取CBN和CBV的定量测量。
英文摘要：
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 CBV that can be both encoded in a unique tight type system for CBPV. All such systems are quantitative, ie. they provide exact information about the length of normalization sequences to normal form as well as the size of these normal forms. Moreover, the length of reduction sequences are discriminated according to their multiplicative and exponential nature, a concept inherited from linear logic. Last but not least, it is possible to extract quantitative measures for CBN and CBV from their corresponding encodings in CBPV.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
