论文标题
呼叫可溶解性和多种类型
Call-by-Value Solvability and Multi Types
论文作者
论文摘要
本文提供了使用逐个价值多类型的呼叫可溶解性的表征。我们的工作基于Accattoli和Paolini对可解决的术语的表征，因为终止了价值替代计算的求解策略的术语，这是对Plotkin的逐次呼叫$λ$ calculus的完善。在这里，我们表明，当$ t $以某种方式在Ehrhard的逐个价值关系语义上引起的多类型系统中，$ t $仅在$ t $中终止$ t $。此外，我们展示了如何从类型系统中提取求解评估的长度以及其正常形式的大小的精确界限，从而适应了de carvalho的逐个名称的技术。
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.
