### Abstract

The introduction of a general definition of function was key to Frege’s formalisation of logic. Self-application 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 13-17, 2015, Proceedings |

Publisher | Springer International Publishing |

Pages | 262-282 |

Number of pages | 21 |

ISBN (Electronic) | 978-3-319-20297-6 |

ISBN (Print) | 978-3-319-20296-9 |

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) | 0302-9743 |

### Conference

Conference | 10th International Computer Science Symposium in Russia 2015 |
---|---|

Abbreviated title | CSR 2015 |

Country | Russian Federation |

City | Listvyanka |

Period | 13/07/15 → 17/07/15 |

### Keywords

- Automath
- Type inclusion
- Unicity of types

### ASJC Scopus subject areas

- Computer Science(all)
- 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)

## Cite this

*Computer Science -- Theory and Applications: 10th International Computer Science Symposium in Russia, CSR 2015, Listvyanka, Russia, July 13-17, 2015, Proceedings*(pp. 262-282). (Lecture Notes in Computer Science; Vol. 9139). Springer International Publishing. https://doi.org/10.1007/978-3-319-20297-6_17