Archive for the 'Twelf' Category

Higher-order representations of substructural logics

Now I’ve settled in to Italy (and my new job), it’s time to resurrect the blog.

By Karl Crary, from ICFP 2010, available from Karl Crary’s website:

We present a technique for higher-order representation of substructural logics such as linear or modal logic. We show that such logics can be encoded in the (ordinary) Logical Framework, without any linear or modal extensions. Using this encoding, metatheoretic proofs about such logics can easily be developed in the Twelf proof assistant.

Associated Twelf code can be found here.

Advertisements

Reasoning with higher-order abstract syntax and contexts

By Amy Felty and Brigitte Pientka, from ITP 2010, available from Amy Felty’s website:

A variety of logical frameworks support the use of higher-order abstract syntax (HOAS) in representing formal systems given via axioms and inference rules and reasoning about them. In such frameworks, object-level binding is encoded directly using meta-level binding. Although these systems seem superficially the same, they differ in a variety of ways; for example, in how they handle a context of assumptions and in what theorems about a given formal system can be expressed and proven. In this paper, we present several case studies which highlight a variety of different aspects of reasoning using HOAS, with the intention of providing a basis for qualitative comparison of different systems. We then carry out such a comparison among three systems: Twelf, Beluga, and Hybrid. We also develop a general set of criteria for comparing such systems. We hope that others will implement these challenge problems, apply these criteria, and further our understanding of the trade-offs involved in choosing one system over another for this kind of reasoning.

Associated proof scripts can be found here.

Optimizing higher-order pattern unification

By Brigitte Pientka and Frank Pfenning, from CADE 2003, available from Frank Pfenning’s website:

We present an abstract view of existential variables in a dependently typed lambda-calculus based on modal type theory. This allows us to justify optimizations to pattern unification such as linearization, which eliminates many unnecessary occurs-checks. The presented modal framework explains a number of features of the current implementation of higher-order unification in Twelf and provides insight into several optimizations. Experimental results demonstrate significant performance improvement in many example applications of Twelf, including those in the area of proof-carrying code.

Higher-order term indexing using substitution trees

By Brigitte Pientka, from ACM Transactions on Computational Logic, available from Brigitte Pientka’s website:

We present a higher-order term indexing strategy based on substitution trees for simply typed lambda-terms. There are mainly two problems in adapting first-order indexing techniques. First many operations used in building an efficient term index and retrieving a set of candidate terms from a large collection are undecidable in general for higher-order terms. Second, the scoping of variables and binders in the higher-order case presents challenges. The approach taken in this paper is to reduce the problem to indexing linear higher-order
patterns, a decidable fragment of higher-order terms, and delay solving terms outside of this fragment. We present insertion of terms into the index based on computing the most specific linear generalization of two linear higher-order patterns, and retrieval based on matching two linear higher-order patterns. Our theoretical framework maintains that terms are in βη-normal form, thereby eliminating the need to re-normalize and raise terms during insertion and retrieval. Finally, we prove correctness of our presented algorithms. This indexing structure is implemented as part of the Twelf system to speed up the execution of the tabled higher-logic programming interpreter.

Abstracting syntax

By Brian Aydemir, Stephan A. Zdancewic and Stephanie Weirich, University of Pennsylvania Technical Report, available from the UPenn Tech Report website:

Binding is a fundamental part of language specification, yet it is both difficult and tedious to get right. In previous work, we argued that an approach based on locally nameless representation and a particular style for defining inductive relations can provide a portable, transparent, lightweight methodology to define the semantics of binding. Although the binding infrastructure required by this approach is straightforward to develop, it leads to duplicated effort and code as the number of binding forms in a language increases.

In this paper, we critically compare a spectrum of approaches that attempt to ameliorate this tedium by unifying the treatment of variables and binding. In particular, we compare our original methodology with two alternative ideas: First, we define variable binding in the object language via variable binding in a reusable library. Second, we present a novel approach that collapses the syntactic categories of the object language together, permitting variables to be shared between them.

Our main contribution is a careful characterization of the benefits and drawbacks of each approach. In particular, we use multiple solutions to the POPLMARK challenge in the Coq proof assistant to point out specic consequences with respect to the size of the binding infrastructure, transparency of the definitions, impact to the metatheory of the object language, and adequacy of the object language encoding.