Towards Extracting Explicit Proofs from Totality Checking in Twelf

TL;DR

This paper presents a method to extract explicit proofs from Twelf's totality checking by translating totality steps into formal proofs in logic M2, aiming to make meta-theorem proofs verifiable.

Contribution

It introduces a translation of Twelf totality checking steps into explicit proofs in logic M2 for a restricted setting, enabling proof verification.

Findings

Successfully translated totality checking steps into M2 proofs

Validated the translation in a restricted Twelf setting

Lays groundwork for extending proof extraction to full Twelf system

Abstract

The Edinburgh Logical Framework (LF) is a dependently type lambda calculus that can be used to encode formal systems. The versatility of LF allows specifications to be constructed also about the encoded systems. The Twelf system exploits the correspondence between formulas and types to give specifications in LF a logic programming interpretation. By interpreting particular arguments as input and others as output, specifications can be seen as describing non-deterministic functions. If particular such functions can be shown to be total, they represent constructive proofs of meta-theorems of the encoded systems. Twelf provides a suite of tools for establishing totality. However, all the resulting proofs of meta-theorems are implicit: Twelf's totality checking does not yield a certificate that can be given to a proof checker. We begin the process here of making these proofs explicit. We treat the restricted situation in Twelf where context definitions (regular worlds) and lemmas are not used. In this setting we describe and prove correct a translation of the steps in totality checking into an actual proof in the companion logic M2. We intend in the long term to extend our translation to all of Twelf and to use this work as the basis for producing proofs in the related Abella system.