Adequate and computational encodings in the logical framework Dedukti

TL;DR

This paper introduces a novel approach for encoding Functional Pure Type Systems in Dedukti that ensures both adequacy and computational representation, addressing limitations of previous encodings.

Contribution

It presents the first correct, adequate, and computational encoding method for Functional Pure Type Systems in Dedukti, with simplified conservativity proofs.

Findings

Proposed encodings are both adequate and conservative.

The approach allows direct representation of computation in Dedukti.

First proof of correct, computational, adequate encodings in Dedukti.

Abstract

Dedukti is a very expressive logical framework which unlike most frameworks, such as the Edinburgh Logical Framework (LF), allows for the representation of computation alongside deduction. However, unlike LF encodings, Dedukti encodings proposed until now do not feature an adequacy theorem -- i.e., a bijection between terms in the encoded system and in its encoding. Moreover, many of them also do not have a conservativity result, which compromises the ability of Dedukti to check proofs written in such encodings. We propose a different approach for Dedukti encodings which do not only allow for simpler conservativity proofs, but which also restore the adequacy of encodings. More precisely, we propose in this work adequate (and thus conservative) encodings for Functional Pure Type Systems. However, in contrast with LF encodings, ours is computational -- that is, represents computation directly as computation. Therefore, our work is the first to present and prove correct an approach allowing for encodings that are both adequate and computational in Dedukti.