Type checking and normalisation
Type checking and normalisation
复制标题
类型检查和规范化
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
James Chapman
中科院分区：
文献类型：
--
作者：
James Chapman
本文是关于马丁-洛夫的直觉主义类型理论（类型理论）的。类型论同时也是数学证明的形式系统和依赖类型的编程语言。依赖类型是依赖于数据的类型，因此要对依赖类型编程进行类型检查，我们需要在类型中执行计算（规范化）。
类型论的实现（通常是某种自动定理证明器或解释器）的核心是类型检查器。类型理论的类型检查器的实现在其核心有一个规范器。在这篇论文中，我认为类型检查，因为它可能形成的基础上实现的类型理论的函数语言Haskell，然后规范化的依赖类型语言Epigram和Agda的更严格的设置。我研究了一种证明规范化的方法，称为大步规范化（BSN）。我申请BSN的一些越来越复杂的结石，并提供机器检查证明Meta理论的属性。
This thesis is about Martin-Lof's intuitionistic theory of types (type theory). Type theory is at the same time a formal system for mathematical proof and a dependently typed programming language. Dependent types are types which depend on data and therefore to type check dependently typed programming we need to perform computation(normalisation) in types.
Implementations of type theory (usually some kind of automatic theorem prover or interpreter) have at their heart a type checker. Implementations of type checkers for type theory have at their heart a normaliser. In this thesis I consider type checking as it might form the basis of an implementation of type theory in the functional language Haskell and then normalisation in the more rigorous setting of the dependently typed languages Epigram and Agda. I investigate a method of proving normalisation called Big-Step Normalisation (BSN). I apply BSN to a number of calculi of increasing sophistication and provide machine checked proofs of meta theoretic properties.