Computational Classical Logic

这个博士学位的目的是研究经典逻辑和计算之间的对应关系，重点是类型理论和操作符，允许控制程序的继续。类型理论允许程序及其规范用相同的语言编写，但传统上由于“纯粹性”而缺乏效果。在这些理论中，效应可以通过单体来模拟，但它们不能很好地与依赖类型交互。延续是一种非常强的效应，能够模仿许多其他类型，而连续运算和类型理论的成功结合将允许对具有效应的依赖类型演算进行更一般的描述。研究的重点是这些理论的语义，因为这些理论允许我们得出关于理论的有用的可靠性结果。

The purpose of this PhD is to investigate the correspondence between classical logic and computation, with a focus on type theories with operators allowing for control over the program continuation.Type theories allow a program and its specification to be written in the same language, but traditionally lack effects due to 'purity'. Effects can be emulated in these theories via monads, but these do not interact well with dependent types.Continuations are a very 'strong' effect, able to emulate many others, and a successful combination of continuation operators and type theory would allow for a more general description of dependently typed calculi with effects.The particular focus of the research is in the semantics of such theories, as these allow us to conclude useful soundness results about a theory.