Automath Type Inclusion in Barendregt’s Cube

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish
Title of host publicationComputer Science -- Theory and Applications
Subtitle of host publication10th International Computer Science Symposium in Russia, CSR 2015, Listvyanka, Russia, July 13-17, 2015, Proceedings
PublisherSpringer International Publishing
Pages262-282
Number of pages21
ISBN (Electronic)978-3-319-20297-6
ISBN (Print)978-3-319-20296-9
DOIs
Publication statusPublished - 23 Jun 2015
Event10th International Computer Science Symposium in Russia 2015 - Listvyanka, Russian Federation
Duration: 13 Jul 201517 Jul 2015

Publication series

NameLecture Notes in Computer Science
PublisherSpringer International Publishing
Volume9139
ISSN (Print)0302-9743

Conference

Conference10th International Computer Science Symposium in Russia 2015
Abbreviated titleCSR 2015
CountryRussian Federation
CityListvyanka
Period13/07/1517/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.

Cite this