Gluing together Proof Environments: Canonical extensions of LF Type Theories featuring Locks

TL;DR

This paper introduces two extensions of LF Type Theory with monadic locks, enabling external oracle calls for constraints and witnesses, facilitating integration of diverse proof systems and encoding complex theories.

Contribution

The paper presents canonical extensions of LF with monadic locks, allowing external oracle interactions for constraints and witnesses, and demonstrates their applications in encoding various logical systems.

Findings

Encoding of Fitch-Prawitz Set theory within the extended system

Representation of call-by-value lambda-calculi

Characterization of strongly normalizing terms using Fitch-Prawitz Set Theory

Abstract

We present two extensions of the LF Constructive Type Theory featuring monadic locks. A lock is a monadic type construct that captures the effect of an external call to an oracle. Such calls are the basic tool for gluing together diverse Type Theories and proof development environments. The oracle can be invoked either to check that a constraint holds or to provide a suitable witness. The systems are presented in the canonical style developed by the CMU School. The first system, CLLFP, is the canonical version of the system LLFP, presented earlier by the authors. The second system, CLLFP?, features the possibility of invoking the oracle to obtain a witness satisfying a given constraint. We discuss encodings of Fitch-Prawitz Set theory, call-by-value lambda-calculi, and systems of Light Linear Logic. Finally, we show how to use Fitch-Prawitz Set Theory to define a type system that types precisely the strongly normalizing terms.