并发调度的一种证明论观点
A proof-theoretic view on scheduling in concurrency
摘要：
本文阐述了一种新的方法的问题的证明理论研究的并发交互称为“证据的时间表”。观察证明理论是非常适合于描述合流系统，而并发具有非确定性作为一个基本特征，我们开发了一个对应的证明提供了什么是需要并发系统合流，即调度。在我们的逻辑系统中，进程和验证者在证明语言的不同片段中显式地显示为证明，并且它们之间的切割消除确实对应于并发系统的执行。这种角色的分离为过程的指称语义提供了新的见解，也为将π演算转换为无前缀的形式主义（如solos）提供了新的方法，作为证明系统之间转换的操作对应物。
英文摘要：
This paper elaborates on a new approach of the question of the proof-theoretic study of concurrent interaction called "proofs as schedules". Observing that proof theory is well suited to the description of confluent systems while concurrency has non-determinism as a fundamental feature, we develop a correspondence where proofs provide what is needed to make concurrent systems confluent, namely scheduling. In our logical system, processes and schedulers appear explicitly as proofs in different fragments of the proof language and cut elimination between them does correspond to execution of a concurrent system. This separation of roles suggests new insights for the denotational semantics of processes and new methods for the translation of pi-calculi into prefix-less formalisms (like solos) as the operational counterpart of translations between proof systems.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
