The Delta-framework

TL;DR

The paper introduces LF-Delta, a dependent type theory extending LF with strong proof-functional connectives that reflect proof shapes, enabling advanced type disciplines and subtyping, and can be integrated into proof assistants.

Contribution

LF-Delta is a novel dependent type theory incorporating strong proof-functional connectives, broadening type discipline expressiveness and subsuming refinement types.

Findings

LF-Delta supports a wide range of type disciplines.

It includes strong intersection, relevant implication, and strong union.

The framework can be integrated into existing proof assistants.

Abstract

We introduce the Delta-framework, LF-Delta, a dependent type theory based on the Edinburgh Logical Framework LF, extended with the strong proof-functional connectives, i.e. strong intersection, minimal relevant implication and strong union. Strong proof-functional connectives take into account the shape of logical proofs, thus reflecting polymorphic features of proofs in formulae. This is in contrast to classical or intuitionistic connectives where the meaning of a compound formula depends only on the truth value or the provability of its subformulae. Our framework encompasses a wide range of type disciplines. Moreover, since relevant implication permits to express subtyping, LF-Delta subsumes also Pfenning's refinement types. We discuss the design decisions which have led us to the formulation of LF-Delta, study its metatheory, and provide various examples of applications. Our strong proof-functional type theory can be plugged in existing common proof assistants.