Scifaro

中文

AF2系统类型类的完备性结果

逻辑 2009-05-06 v1

作者: Samir Farkh , Karim Nour

在 arXiv 上查看 ↗ PDF ↗

摘要

J.-L. Krivine引入了AF2类型系统，旨在通过编写函数全总性的证明来获得计算函数的程序（λ项）。我们在本文中给出了AF2的某些类型以及多种归约概念的完备性结果。这些结果推广了R. Labib-Sami在J.-Y. Girard的系统F中建立的一个定理。

关键词

AF2类型系统完备性 λ演算类型类归约程序提取

引用

@article{arxiv.0905.0575,
  title  = {R\'esultats de compl\'etude pour des classes de types du syst\`eme AF2},
  author = {Samir Farkh and Karim Nour},
  journal= {arXiv preprint arXiv:0905.0575},
  year   = {2009}
}