Bridging Curry and Church's typing style

Research output: Contribution to journalArticle

21 Downloads (Pure)

Abstract

There are two versions of type assignment in the λ-calculus: Church-style, in which the type of each variable is fixed, and Curry-style (also called "domain free"), in which it is not. As an example, in Church-style typing, λx:A.x is the identity function on type A, and it has type A→A but not B→B for a type B different from A. In Curry-style typing, λx.x is a general identity function with type C→C for every type C. In this paper, we will show how to interpret in a Curry-style system every Pure Type System (PTS) in the Church-style without losing any typing information. We will also prove a kind of conservative extension result for this interpretation, a result which implies that for most consistent PTSs of the Church-style, the corresponding Curry-style system is consistent. We will then show how to interpret in a system of the Church-style (a modified PTS, stronger than a PTS) every PTS-like system in the Curry style.

Original languageEnglish
Pages (from-to)42-70
Number of pages29
JournalJournal of Applied Logic
Volume18
Early online date16 Jun 2016
DOIs
Publication statusPublished - Nov 2016

Keywords

  • Church-style typing
  • Curry-style typing
  • Domain-free typing
  • Domain-full typing

ASJC Scopus subject areas

  • Logic
  • Applied Mathematics

Fingerprint Dive into the research topics of 'Bridging Curry and Church's typing style'. Together they form a unique fingerprint.

  • Cite this