标题： 带栈的可逆计算与“故障的可逆管理” 显示英文标题

标题： Reversible Computation with Stacks and "Reversible Management of Failures"

摘要： 这项工作专注于使某些计算模型具有可逆性。 我们从一个想法出发，即“可逆化”应意味着一个使计算模型具有操作语义的过程，该过程能够将每个项解释为双射函数。 最常用的可逆化方法创建的操作语义在无法从产生的计算状态唯一确定起始状态时会停止计算；因此，项被解释为部分双射函数。 我们引入$\textsf{S-CORE}$，这是一种允许操作变量和栈的项的语言。 对于$\textsf{S-CORE}$，我们定义了操作语义$\textsf{R-semantics}$。 借助证明助手，我们验证了$\textsf{R-semantics}$使得$\textsf{S-CORE}$成为一个可逆的命令式计算模型，其中所有项都被解释为适当状态空间上的全双射函数。 显示英文摘要

摘要： This work focuses on making certain computational models reversible. We start with the idea that "reversibilizing" should mean a process that gives a computational model an operational semantics capable of interpreting each term as a bijection. The most commonly used method of reversibilization creates operational semantics that halt computation when it is not possible to uniquely determine the starting state from a produced computational state; thus, terms are interpreted as partial bijective functions. We introduce $\textsf{S-CORE}$, a language of terms that allows manipulation of variables and stacks. For $\textsf{S-CORE}$, we define the operational semantics $\textsf{R-semantics}$. With the help of a proof assistant, we certify that $\textsf{R-semantics}$ makes $\textsf{S-CORE}$ a reversible imperative computational model where all terms are interpreted as total bijections on an appropriate state space.