Overcoming performance barriers: Efficient verification techniques for logical frameworks

Abstract

In recent years, logical frameworks which support formalizing language specifications together with their meta-theory have been pervasively used in small and large-scale applications, from certifying code [2] to advocating a general infrastructure for formalizing the meta-theory and semantics of programming languages [5]. In particular, the logical framework LF [9], based on the dependently typed lambdacalculus, and light-weight variants of it like LF4 [17] have played a major role in these applications. While the acceptance of logical framework technology has grown and they have matured, one of the most criticized points is concerned with the run-time performance. In this tutorial we give a brief introduction to logical frameworks, describe its state-of-the art and present recent advances in addressing some of the existing performance issues. © Springer-Verlag Berlin Heidelberg 2006.