Unified Approach to Type Theory through a Refined lambda-Calculus

摘要

Lambda-calculus is at the heart of type theory while type theory has been themost stimulating part of the theory of Computation. The presence however of various type systems provokes attempts at finding a unified way of describing these systems. Barendregt's cube for example, is such an attempt. Based on these observations, the authors will devise a new lambda-notation which enables categorizing most of the known systems in a unified way. More precisely, the authors will sketch the general structure of a system of typed lambda calculus and show that this system has enough expressive power for the description of various existing systems, ranging from Automath-like systems to singly-typed Pure Type Systems.