Abstract
The introduction of a general definition of function was key to Frege’s formalisation of logic. Selfapplication of functions was at the heart of Russell’s paradox. Russell introduced type theory to control the application of functions and avoid the paradox. Since, different type systems have been introduced, each allowing different functional power. Most of these systems use the two binders λ and Π to distinguish between functions and types, and allow βreduction but not Πreduction. That is, (Formula Presented.) is only allowed when π is λ but not when it is Π. Since Πreduction is not allowed, these systems cannot allow unreduced typing. Hence types do not have the same instantiation right as functions. In particular, when b has type B, the type of (Formula Presented.) is immediately given as B[x := C] instead of keeping it as (λ_{x}:A.B)C to be Πreduced to B[x := C] later. Extensions of modern type systems with both β and Πreduction and unreduced typing have appeared in [11,12] and lead naturally to unifying the λ and Π abstractions [9,10]. The Automath system combined the unification of binders λ and Π with β and Πreduction together with a type inclusion rule that allows the different expressions that define the same term to share the same type. In this paper we extend the cube of 8 influential type systems [3] with the Automath notion of type inclusion [5] and study its properties.
Original language  English 

Title of host publication  Computer Science  Theory and Applications 
Subtitle of host publication  10th International Computer Science Symposium in Russia, CSR 2015, Listvyanka, Russia, July 1317, 2015, Proceedings 
Publisher  Springer 
Pages  262282 
Number of pages  21 
ISBN (Electronic)  9783319202976 
ISBN (Print)  9783319202969 
DOIs  
Publication status  Published  23 Jun 2015 
Event  10th International Computer Science Symposium in Russia 2015  Listvyanka, Russian Federation Duration: 13 Jul 2015 → 17 Jul 2015 
Publication series
Name  Lecture Notes in Computer Science 

Publisher  Springer International Publishing 
Volume  9139 
ISSN (Print)  03029743 
Conference
Conference  10th International Computer Science Symposium in Russia 2015 

Abbreviated title  CSR 2015 
Country/Territory  Russian Federation 
City  Listvyanka 
Period  13/07/15 → 17/07/15 
Keywords
 Automath
 Type inclusion
 Unicity of types
ASJC Scopus subject areas
 General Computer Science
 Theoretical Computer Science
Fingerprint
Dive into the research topics of 'Automath Type Inclusion in Barendregt’s Cube'. Together they form a unique fingerprint.Profiles

Fairouz Dib Kamareddine
 School of Mathematical & Computer Sciences  Professor
 School of Mathematical & Computer Sciences, Computer Science  Professor
Person: Academic (Research & Teaching)