Canonical typing and Π-conversion in the Barendregt Cube

作     者：Kamareddine, Fairouz Nederpelt, Rob 

作者机构：Department of Computing Science University of Glasgow Glasgow G12 8QQ 17 Lilybank Gardens United Kingdom Dept. of Math. and Computing Science Eindhoven University of Technology 5600 MB Eindhoven P.O.Box 513 Netherlands 

出 版 物：《Journal of Functional Programming》 (J. Funct. Program.)

年 卷 期：1996年第6卷第2期

页      面：245-267页

学科分类：08[工学] 0835[工学-软件工程] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 081202[工学-计算机软件与理论] 

基　　金：Department of Mathematics and Computing Science Technische Universiteit Eindhoven, TU/e 

摘      要：In this article, we extend the Barendregt Cube with Π-conversion (which is the analogue of β-conversion, on product type level) and study its properties. We use this extension to separate the problem of whether a term is typable from the problem of what is the type of a term.