Interacting Safely with an Unsafe Environment

TL;DR

This paper presents a new perspective on Pure type systems allowing ill-formed contexts, facilitating extensions with computation rules in logical frameworks like Dedukti.

Contribution

It introduces an alternative formulation of Pure type systems that accommodates non-well-formed contexts, enabling more flexible extensions with computation rules.

Findings

Equivalent to the standard presentation of Pure type systems

Allows declaration of constants before computation rules

Facilitates extensions in logical frameworks like Dedukti

Abstract

We give a presentation of Pure type systems where contexts need not be well-formed and show that this presentation is equivalent to the usual one. The main motivation for this presentation is that, when we extend Pure type systems with computation rules, like in the logical framework Dedukti, we want to declare the constants before the computation rules that are needed to check the well-typedness of their type.