and

In the area of foundations of mathematics and computer science, three related topics dominate. These are -calculus, type theory and logic. There are moreover, many versions of -calculi and type theories. In these versions, the presence of logic ranges from the non-existant to the domi-nant. In fact, the three subjects of -calculus, logic and type theory, got separated due to the appearence of the paradoxes. Moreover, the exis-tence of various versions of each topic is due to the need to get back to the lost paradise which allowed a great freedom in mixing expressivity and logic. In any case, the presence of such a variety of systems calls for a framework to unify them all. Barendregt's cube for example, is an attempt to unify various type systems and his associated logic cube is an attempt to nd connections between type theories and logic. We devise a new -notation which enables categorising most of the known systems in a unied way. More precisely, we sketch the general structure of a system of typed lambda calculus and show that this system has enough expres-sive power for the description of various existing systems, ranging from Automath-like systems to singly-typed Pure Type Systems. The system We are grateful for Erik Poll who has read the paper carefully and for his productive comments. We are also grateful for discussions with Henk Barendregt, Inge Bethke, Tijn Borghuis and for the helpful remarks received from them. Furthermore, we are indebted to the anonymous referee for his/her useful suggestions and remarks.