7.3 Logical Frameworks 151from a domain with a decidable equality theory. This appears to be a reasonablecompromise that can make the expressive power of dependent types availableto the programmer without sacrificing decidable and efficient type-checking.7.3 Logical FrameworksIn the previous section, we illustrated how (linear) type theory could be usedas the foundation of (linear) functional programming. The demands of a com-plete functional language and, in particular, the presence of data types andrecursion makes it difficult to attain decidable type-checking. In this section wediscuss another application of linear type theory as the foundation for a logicalframework.A logical framework is a meta-language for the specification and implemen-tation of deductive systems. This includes applications in various logics andprogramming languages For surveys of logical frameworks and their applica-tions, see [Pfe96, BM01, Pfe01].One of the most expressive current frameworks is LF [HHP93] which is basedon a λ-calculus with dependent types. There are many elegant encodings of de-ductive systems in such a framework that can be found in the references above.However, there are also many systems occurring both in logic and program-ming languages, for which encodings are awkward. Examples are substructurallogic (such as linear logic), calculi for concurrency (such as the π-calculus), orprogramming languages with state (such as Mini-ML with mutable references).Even for pure languages such as Haskell, some aspects of the operational seman-tics such as laziness and memoization are difficult to handle. This is because ata lower level of abstraction, the implementations of even the purest languagesare essentially state-based.In response to these shortcomings, a linear logical framework (LLF) has beendeveloped [CP96, Cer96, CP98]. This framework solved some of the problemsmentioned above. In particular, it allows natural encodings of systems withstate. However, it did not succeed with respect to intrinsic notions of concur-rency. We will try to give an intuitive explanation of why this is so after showingwhat the system looks like.First, in a nutshell, the system LF. The syntax has the following form:Types A ::= aM1...Mn|Πx:A1...A2Objects M ::= c | x | λx:A. M | M1M2Here, a ranges over type families indexed by object Mi, c ranger over objectconstants. Unlike the functional language above, these are not declared byformation rules, introduction rules, and elimination rules. In fact, we must avoidadditional introduction and elimination rules because the corresponding localreductions make the equational theory (and therefore type checking) difficult tomanage.Instead, all judgments will be parametric in these constants! They are de-clared in a signature Σ which is a global analogue of the context Γ. We needDraft of December 4, 2001152 Linear Type Theorykinds in order to classify type families.Kinds K ::= Πx1:A1...Πxn:An.typeSignatures Σ ::= ·|Σ,a:K |Σ,c:AAs a simple example, we consider a small imperative language. We distin-guish expressions (which have a value, but no effect) from commands (whichhave an effect, but no value). Expressions are left unspecified, except that vari-ables are allowed as expressions and that we must have boolean values trueand false. In other words, our example is parametric in the language of ex-pressions; the only requirements are that they cannot have an effect, and thatthey must allow variables. Commands are no-ops (skip), sequential composition(C1; C2), parallel composition (C1k C2), assignment (x := e) and the alloca-tion of a new local variable (new x. C). We also have a conditional construct(if e then C1else C2)andalooploop l. C.Expression Types τ ::= bool | ...Expressions e ::= x | true | false | ...Commands C ::= skip | C1; C2| C1k C2| x := e | new x:τ. C| if e then C1else C2| loop l. CFor the loop construct loop l. C, we introduce a label l with scope C.Thislabel is considered a new command in C, where invoking l corresponds to a copyof the loop body. Thus executing loop l. C reduces to executing [loop l. C/l]C.Note that this only allows backwards jumps and does not model a general goto.Its semantics is also different from goto if it is not the “last” command in a loop(see Exercise ?? where you are also asked to model a while-loop using loop).The simplest infinite loop is loop l. l.We now turn to the representation of syntax. We have a framework typetp representing object language types, and index expressions by their objectlanguage type. We show the representation function pτq and peq.tp : typepboolq = bool bool : tpvar : tp → typeexp : tp → typepxq = v pτ q x v : ∀t:tp. var(t) → exp(t)ptrueq = true true : exp(bool)pfalseq = false false : exp(bool)One of the main points to note here is that variables of our imperativelanguage are represented by variables in the framework. For the sake of conve-nience, we choose the same name for a variable and its representation. The typeof such a variable in the framework will be var(pτq) depending on its declaredtype. v is the coercion from a variable of type τ to an expression of type τ.Ithas to be indexed by a type t, because it could be applied to an expression ofany type.Draft of December 4, 20017.3 Logical Frameworks 153Commands on the other hand do not return a value, so their type is notindexed. In order to maintain the idea the variables are represented by vari-ables, binding constructs in the object language (namely new and loop)mustbe translated so they bind the corresponding variable in the meta-language.This idea is called higher-order abstract syntax [PE88], since the type of suchconstructs in generally of order 2 (the constructors new and loop take functionsas arguments).pskipq = skippC1; C2q = seq pC1qpC2qpC1kC2q = par pC1qpC2qpx:= eq = assign pτ q x peq for x and e of type τpnew x:τ. Cq = new pτ q (λx:var(pτ q). pCq)pif e then C1else C2q = if peqpC1qpC2q for e of type boolploop l. Cq = loop (λl:cmd. pCq)In the declarations below, wee see that assign and new need to be indexed bytheir type, and that a conditional command branches depending on a booleanexpression. In that way only well-typed commands can be represented—otherswill be rejected as ill-typed in the framework.cmd : typeskip : cmdseq : cmd → cmd → cmdpar : cmd → cmd → cmdassign : ∀t:tp. var(t) → exp(t) → cmdnew : ∀t:tp. (var(t) → cmd) → cmdif : exp(bool) → cmd → cmdloop :(cmd → cmd) →