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.