**Date:**
Wed 11 Dec

**Time:**
15.00

**Place:**
room 214

**Speaker:**
Dale Miller (Univ. of Pennsylvania)

**Title:**
A Logic for Reasoning with Logic Specifications

**Abstract.**
Meta-logics and logical frameworks have been successfully used to give
high-level, modular, and formal specifications of many important judgments
made in programming languages, including, for example, the definition of
dynamic (eg, evaluation) and static (eg, typing) semantics for programming
languages. With recent advances in the implementation of such logical
systems, it is possible to turn these specifications into prototype
implementations where extended experiments with specifications can be done.
It is desirable, of course, to be able to prove properties about such
judgments: for example, to prove that evaluation is deterministic or that
evaluation preserves types. After providing an overview and several
examples of the specification of such judgment in a logical language, I
discuss some recent work on formalizing a meta-logic for reasoning about
such judgments. In particular, I will describe how a commonly used
meta-logic, higher-order intuitionistic logic, can be extended with the two
proof-theoretic principles of ``definitions'' and induction over natural
numbers. We briefly discuss the meta-theory of this logic and provide
several example proofs in it. This is joint work with Ray McDowell.