Conjunctive Types and SKInT

Abstract

The λ-calculus and its typed versions are important tools for studying most fundamental computation and deduction paradigms. However, the non-trivial nature of substitution, as used in the definition of λ-reduction notably, has spurred the design of various first-order languages representing λ-terms, λ-reduction and λ-conversion, where computation is simple, first-order rewriting, and substitution becomes an easy notion again. Let us cite Curry’s combinators [7], Curien’s categorical combinators [5], the myriad of so-called λ-calculi with explicit substitutions, among which λσ [1], λσ⇑. [12], λυ [17], λζ [19], etc. Unfortunately, each one of these calculi has defects: Curry’s combinators do not model λ-conversion fully, categorical combinators, λσ and λσ⇑ do not normalize strongly in the typed case [18], λυ is not confluent in the presence of free variables (a.k.a. metavariables), λζ models λ-conversion but not λ-reduction, etc.

This work has been done in the context of Dyade (Bull/Inria R&D joint venture).