系统F的语法数据类型
逻辑
2009-05-07 v1
摘要
本文给出了系统F的输入和输出类型的纯语法定义。我们将语法数据类型定义为输入和输出类型。我们证明了任何具有正量词的类型都是语法数据类型，并且输入类型是输出类型。我们对∀-消去规则施加了一些限制，以证明输出类型是输入类型。
引用
@article{arxiv.0905.0754,
title = {Les types de donn\'ees syntaxiques du syst\`eme F},
author = {Samir Farkh and Karim Nour},
journal= {arXiv preprint arXiv:0905.0754},
year = {2009}
}