Archive for the 'HOAS' 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

Hybrid: A Defintional Two Level Approach to Reasoning with Higher-Order Abstract Syntax

By Amy Felty and Alberto Monigliano, accepted in the Journal of Automated Reasoning 2010, available from Amy Felty’s website:

Combining higher-order abstract syntax and (co)-induction in a logical framework is well known to be problematic. We describe the theory and the practice of a tool called Hybrid, within Isabelle/HOL and Coq, which aims to address many of these difficulties. It allows object logics to be represented using higher-order abstract syntax, and reasoned about using tactical theorem proving and principles of (co)induction. Moreover, it is definitional, which guarantees consistency within a classical type theory. The idea is to have a de Bruijn representation of λ-terms providing a definitional layer that allows the user to represent object languages using higher-order abstract syntax, while offering tools for reasoning about them at the higher level. In this paper we describe how to use Hybrid in a multi-level reasoning fashion, similar in spirit to other systems such as Twelf and Abella. By explicitly referencing provability in a middle layer called a specification logic, we solve the problem of reasoning by (co)induction in the presence of non-stratifiable hypothetical judgments, which allow very elegant and succinct specifications of object logic inference rules. We first demonstrate the method on a simple example, formally proving type soundness (subject reduction) for a fragment of a pure functional language, using a minimal intuitionistic logic as the specification logic. We then prove an analogous result for a continuation-machine presentation of the operational semantics of the same language, encoded this time in an ordered linear logic that serves as the specification layer. This example demonstrates the ease with which we can incorporate new specification logics, and also illustrates a significantly more complex object logic whose encoding is elegantly expressed using features of the new specification logic.

Relating nominal and higher-order abstract syntax specifications

By Andrew Gacek, from PPDP 2010, available from Andrew Gacek’s website:

Nominal abstract syntax and higher-order abstract syntax provide a means for describing binding structure which is higher-level than traditional techniques. These approaches have spawned two different communities which have developed along similar lines but with subtle differences that make them difficult to relate. The nominal abstract syntax community has devices like names, freshness, name-abstractions with variable capture, and the new-quantifier, whereas the higher-order abstract syntax community has devices like lambda-binders, lambda conversion, raising, and the nabla-quantifier. This paper aims to unify these communities and provide a concrete correspondence between their different devices. In particular, we develop a semantics-preserving translation from alpha-Prolog, a nominal abstract syntax based logic programming language, to G-, a higher-order abstract syntax based logic programming language. We also discuss higher-order judgments, a common and powerful tool for specifications with higher-order abstract syntax, and we show how these can be incorporated into G-. This establishes G- as a language with the power of higher-order abstract syntax, the fine-grained variable control of nominal specifications, and the desirable properties of higher-order judgments.

The nabla-calculus. Functional programming with higher-order encodings.

By Carsten Schurmann, Adam Poswolsky and Jeffrey Sarnat, from TLCA 2005, available from the Elphin website:

Higher-order encodings use functions provided by one language to represent variable binders of another. They lead to concise and elegant representations, which historically have been difficult to analyze and manipulate.
In this paper we present the nabla-calculus, a calculus for defining general recursive functions over higher-order encodings. To avoid problems commonly associated with using the same function space for representations and computations, we separate one from the other. The simply-typed λ-calculus plays the role of the representation level. The computation level contains not only the usual computational primitives but also an embedding of the representation-level. It distinguishes itself from similar systems by allowing recursion under representation-level λ-binders while permitting a natural style of programming which we believe scales to other logical frameworks. Sample programs include bracket abstraction, parallel reduction, and an evaluator for a simple language with first-class continuations.

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.

Free variable types

By Edwin Westbrook, from TFP 2006, available from Aaron Stump’s website:

Higher-order abstract syntax (HOAS) has been shown to be useful in formal systems for reasoning about programming languages. How to recurse over HOAS representations, however, is a well-known problem. This is because, in most current systems, it is generally impossible to recurse on the body of a λ-abstraction without creating a fresh variable, which must itself be bound. This in turn makes it impossible, for instance, to extract first-order data from higher-order data. One previous approach to this problem has been to allow the creation of fresh variables that are not bound to pass to λ-abstractions as long as they can be shown not to escape their scope. Current systems cannot show these do not escape their scope without a runtime check. In this paper, we propose a novel type system that allows explicit reasoning about free variables. This type system can ensure these fresh variables do not escape their scopes without runtime checks. The usefulness of this approach is shown with a simple example.

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.