[Prev][Next][Index][Thread]
Reasoning with Higher-Order Abstract Syntax
I would like to announce the availability of the following paper.
Comments and suggestions are most welcome.
Regards,
Raymond McDowell
------------------------------------------------------------------------
Reasoning with Higher-Order Abstract Syntax in a Logical Framework
Raymond McDowell and Dale Miller
ABSTRACT: Logical frameworks based on intuitionistic or linear logics with
higher-type quantification have been successfully used to give high-level,
modular, and formal specifications of many important judgments in the area
of programming languages and inference systems. Given such specifications,
it is natural to consider proving properties about the specified systems
in the framework: for example, given the specification of evaluation for a
functional programming language, prove that the language is deterministic
or that evaluation preserves types. One challenge in developing a
framework for such reasoning is that higher-order abstract syntax (HOAS),
an elegant and declarative treatment of object-level abstraction and
substitution, is difficult to treat in proofs involving induction. In this
paper, we present a meta-logic that can be used to reason about judgments
coded using HOAS; this meta-logic is an extension of a simple
intuitionistic logic that admits higher-order quantification over simply
typed lambda-terms (key ingredients for HOAS) as well as induction and a
notion of definition. The latter concept of definition is a
proof-theoretic device that allows certain theories to be treated as
``closed'' or as defining fixed points. We explore the difficulties of
formal meta-theoretic analysis of HOAS encodings by considering encodings
of intuitionistic and linear logics, and formally derive the admissibility
of cut for important subsets of these logics. We then propose an approach
to avoid the apparent tradeoff between the benefits of higher-order
abstract syntax and the ability to analyze the resulting encodings. We
illustrate this approach through examples involving the simple functional
and imperative programming languages PCF and PCF:=. We formally derive
such properties as unicity of typing, subject reduction, determinacy of
evaluation, and the equivalence of transition semantics and natural
semantics presentations of evaluation.
This paper is available electronically from my web page
<http://cc.kzoo.edu/~mcdowell/current/research.html>
and through the Computing Research Repository
<http://xxx.lanl.gov/abs/cs.LO/0003062> .