Tutorial on Twelf and LLF Seminars/Workshops

Abstract

• Twelf
• LLF

Logical frameworks are meta-languages designed to specify and reason about deductive systems. Twelf is an implementation of the LF logical framework which allows very elegant encodings (via higher-order abstract syntax) of many systems of interest to programming language researchers (e.g. type theories, evaluation semantics, logics). Additionally, through the judgements as types paradigm, Twelf can smoothly represent much of the meta-theory of such systems (e.g. proof of type-preservation, proof of cut-elimination). Twelf is also a constraint logic programming language and can be used to execute its specifications. Recent work on Twelf has resulted in an extension which can automatically prove many meta-theoretic results.

I will begin with a review of the Edinburgh Logical Framework (LF), whose underlying theory is a dependently typed lambda calculus. I will review the standard representation techniques of LF, including higher-order abstract syntax, the judgement-as-types principle and notion of an adequate representation. Next I will describe the implementation of LF as a constraint logic programming language (Twelf) and demonstrate its use through several example representations. I will end discussion of Twelf by reviewing some recent work on automating the meta-theory of deductive systems which allows Twelf to automatically prove type preservation of mini-ml and cut-elimination of classical/intuitionistic logic, among other things. Finally, I will introduce a conservative extension of LF with linear types, the Linear Logical Framework (LLF), and its implementation as a linear extension of Twelf. I will begin with a review of (intuitionistic) Linear Logic and the dependently typed linear lambda calculus used in LLF. I will briefly discusss the implementation of LLF as a linear logic programming language. I will conclude with some examples of how linear types may be put to use.