Modern Logical Frameworks Design

Throughout the years, logical frameworks have been a successful tool for prototyping and developing a number of logics and programming languages. However, to use the full power of the LF approach, the behaviour of variables in the system being mechanised must match the behaviour of those used in the LF variant. While this is not a problem when working with more standard logical systems, it severely limits the usefulness of LF-like frameworks for less typical applications. A more practical consideration is that many of the existing frameworks do not have implementations, and even those that do lack support for reasoning about, or programming with, the mechanised systems.

Our main motivation is to eventually make it possible to model and reason about complex concurrent systems and protocols. No matter the application, be it the development of a logic for multiparty session types or a cryptographic protocol used in a voting system, we need the ability to model and reason about both the building blocks of these systems and the intricate connections between them.

To this end, this dissertation is an investigation into LF-based formalisms that might help address the aforementioned issues. We design and provide the meta-theory of two new frameworks, HyLF and Lincx. The former aims to extend the expressiveness of LF to include proof irrelevance and some user-defined behaviours, using ideas from hybrid logics. The latter is a showcase for an easier to implement framework, while also allowing more properties of the mechanised system to be expressed.