A simple type-theoretic language: Mini-TT

A simple type-theoretic language: Mini-TT
复制标题

一种简单的类型论语言：Mini-TT

DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
M. Takeyama
M. Takeyama
中科院分区：
--
文献类型：
--
作者：
T. Coquand;Y. Kinoshita;Bengt Nordström;M. Takeyama

文献摘要

相似文献

本文给出了一种小型函数式语言的形式化描述 依赖类型。该语言包含数据类型，相互递归/ 归纳定义和小类型的宇宙。语法， 语义和类型系统是以这样一种方式指定的， 解析器、解释器和类型检查器的集成是很简单的。 主要的困难在于如何设计转换算法 它适用于开放式表达。本文以一个完整的 Haskell实现（大约400行代码）。
This paper presents a formal description of a small functional language with dependent types. The language contains data types, mutual recursive/ inductive definitions and a universe of small types. The syntax, semantics and type system is specified in such a way that the implementation of a parser, interpreter and type checker is straightforward. The main difficulty is to design the conversion algorithm in such a way that it works for open expressions. The paper ends with a complete implementation in Haskell (around 400 lines of code).