Guidi, Ferruccio
(2015)
*Extending the Applicability Condition in the Formal System \lambda\delta.*
[Preprint]

Full text available as:

## Abstract

The formal system \lambda\delta is a typed lambda calculus
derived from \Lambda\infinity, aiming to support the foundations of Mathematics that require an underlying theory of expressions (for example the Minimal Type Theory).
The system is developed in the context of the Hypertextual Electronic Library of Mathematics as a machine-checked digital specification, that is not the formal counterpart of previous informal material. The first version of the calculus appeared in 2006 and proved unsatisfactory for some reasons. In this article we present a revised version of the system and we prove three relevant desired properties: the confluence of reduction, the strong normalization of an extended form of reduction, known as the ``big tree'' theorem, and the preservation of validity by reduction. To our knowledge, we are presenting here
the first fully machine-checked proof of the ``big tree'' theorem for a calculus that includes \Lambda\infinity.

Abstract

The formal system \lambda\delta is a typed lambda calculus
derived from \Lambda\infinity, aiming to support the foundations of Mathematics that require an underlying theory of expressions (for example the Minimal Type Theory).
The system is developed in the context of the Hypertextual Electronic Library of Mathematics as a machine-checked digital specification, that is not the formal counterpart of previous informal material. The first version of the calculus appeared in 2006 and proved unsatisfactory for some reasons. In this article we present a revised version of the system and we prove three relevant desired properties: the confluence of reduction, the strong normalization of an extended form of reduction, known as the ``big tree'' theorem, and the preservation of validity by reduction. To our knowledge, we are presenting here
the first fully machine-checked proof of the ``big tree'' theorem for a calculus that includes \Lambda\infinity.

Document type

Preprint

Creators

Keywords

explicit substitutions,
extended applicability condition,
extended transition system,
infinite degrees of terms,
preservation of validity,
strong normalization,
terms as types

Subjects

DOI

Deposit date

09 Dec 2015 08:25

Last modified

15 Dec 2015 08:06

URI

## Other metadata

Document type

Preprint

Creators

Keywords

explicit substitutions,
extended applicability condition,
extended transition system,
infinite degrees of terms,
preservation of validity,
strong normalization,
terms as types

Subjects

DOI

Deposit date

09 Dec 2015 08:25

Last modified

15 Dec 2015 08:06

URI

## Downloads

## Downloads

Staff only: