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.