按值调用可解性和多类型
Call-by-Value Solvability and Multi Types
摘要：
本文利用按值调用的多个类型给出了按值调用可解性的一个刻画。我们的工作是基于Accattoli和Paolini的特征调用值可解的条款，这些终止相对于解决策略的值替换演算，一个改进的Plotkin的调用值$λ$演算。在这里，我们表明，解决策略终止于一个长期$t$当且仅当$t$是以某种方式在Ehrhard的调用值关系语义诱导的多类型系统的类型。此外，我们展示了如何从类型系统中提取精确的边界上的长度的解决评估和其范式的大小，适应德卡瓦略的技术，按名称调用。
英文摘要：
This paper provides a characterization of call-by-value solvability using call-by-value multi types. Our work is based on Accattoli and Paolini's characterization of call-by-value solvable terms as those terminating with respect to the solving strategy of the value substitution calculus, a refinement of Plotkin's call-by-value $λ$-calculus. Here we show that the solving strategy terminates on a term $t$ if and only if $t$ is typable in a certain way in the multi type system induced by Ehrhard's call-by-value relational semantics. Moreover, we show how to extract from the type system exact bounds on the length of the solving evaluation and on the size of its normal form, adapting de Carvalho's technique for call-by-name.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
