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.