Syntax and Models of a non-Associative Composition of Programs and Proofs. (Syntaxe et modèles d'une composition non-associative des programmes et des preuves)
Syntax and Models of a non-Associative Composition of Programs and Proofs. (Syntaxe et modèles d'une composition non-associative des programmes et des preuves)
复制标题
程序和证明的非关联组合的语法和模型。
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Guillaume Munch
中科院分区：
文献类型：
--
作者：
Guillaume Munch
本论文是对理解编程语言、证明理论和分类模型中极化的性质、作用和机制的贡献。极化对应于我们可以放松组合的结合性的想法，正如我们通过将我们的极化的直接模型二倍体与结合相关联所表明的那样。因此，极化是许多计算模型的基础，我们通过分解连续传递式定界控制模型的三个基本步骤进一步展示了这一点。它还解释了构造性相关的现象，在证明理论，我们说明了提供一个公式作为类型的解释极化一般，特别是对合否定。我们的方法的基石是一个交互式的基于术语的表示证明和程序（L演算），它暴露了极性的结构。它基于抽象机器和微积分之间的对应关系，旨在综合各种趋势：编程语言中的控制、评估顺序和效果的建模，对范畴对偶和连续性之间关系的探索，以及证明论中的交互式构造概念。我们给出了一个温和的介绍我们的方法，只假设简单类型的λ演算和重写的基本知识。
The thesis is a contribution to the understanding of the nature, role, and mechanisms of polarisation in programming languages, proof theory and categorical models. Polarisation corresponds to the idea that we can relax the associativity of composition, as we show by relating duploids, our direct model of polarisation, to adjunctions. As a consequence, polarisation underlies many models of computation, which we further show by decomposing continuation-passing-style models of delimited control in three fundamental steps. It also explains constructiveness-related phenomena in proof theory, which we illustrate by providing a formulae-as-types interpretation for polarisation in general and for an involutive negation in particular. The cornerstone of our approach is an interactive term-based representation of proofs and programs (L calculi) which exposes the structure of polarities. It is based on the correspondence between abstract machines and sequent calculi, and it aims at synthesising various trends: the modelling of control, evaluation order and effects in programming languages, the quest for a relationship between categorical duality and continuations, and the interactive notion of construction in proof theory. We give a gentle introduction to our approach which only assumes elementary knowledge of simply-typed λ calculus and rewriting.