Jesse Alama

Generalizing Theorems of the Mizar Mathematical Library by Type

Promotion and Property Omission

When a formal proof is conducted, one generally employs mathematical concepts so that previously formalized knowledge can be reused. Such reuse of previously established knowledge is obviously important for many reasons.  From a logical point of view, though, the concepts employed in a formal proof are often more specific thanwhat is truly needed for the proof to be successful: the proof might be able to succeed using less logical or mathematical information than was actually employed.  Indeed, when formalizing proofs with interactive theorem provers, it often happens that extra background knowledge (declarative or procedural) about mathematical concepts is employed to help the formalizer focus on the relevant details of the proof.  In this note we describe an experiment conducted on the Mizar Mathematical Library in finding exact information about what is needed through two means: removing implicit properties of functions and relations (so that we can get a better handle on what implicit information an interactive theorem prover is actually needed), and ``promoting'' the types of terms (so that a term having a type is treated uniformly as having a more general type).

Andreas Abel and Nicolai Kraus

A Lambda Term Representation Based on Linear Ordered Logic

We introduce a new nameless representation of lambda terms based on ordered logic.  At a lambda abstraction, number and relative position of all occurrences of the bound variable are stored, and application carries the additional information where to cut the variable context into function and argument part.  This way, complete information about free variable occurrence is available at each subterm without requiring a traversal, and environments can be kept exact such that they only assign values to variables that actually occur in the associated term. Our approach avoids space leaks in interpreters that build  function closures.  

In this article, we prove correctness of the new representation and present an experimental evaluation of its performance in a proof checker for the Edinburgh Logical Framework.

Henk Barendregt

Accepting Formalized Proofs

It has been over 40 years since Dick de Bruijn introduced the technology of formalizing and machine verifying mathematical proofs. Among general mathematicians the acceptance was slow: one can arguably say that this only happened during the last five years. The reason for this slow reaction was psychological. Mathematicians felt that in a formal proof the 'soul' of their subject had been removed. But the formal proofs are alive and kicking and will bring

mathematics and its applications in the 21-st century to an even higher level than they had been enjoying. Still there is considerable work to do for this to happen.

Maxime Beauquier and Carsten Schuermann

A Bigraph Relational Model

In this paper, we present a model based on relations for bigraphical reactive system [Milner09]. Its defining characteristics are that validity and reaction relations are captured as traces in a multi-set rewriting system. The relational model is derived from Milner's graphical definition and directly amenable to implementation.

Mathieu Boespflug and Brigitte Pientka

Multi-level Contextual Type Theory

Contextual type theory distinguishes between bound variables and meta-variables and has been used to give concise explanations of higher-order unification, characterize holes in proofs, and develop a foundation for programming with higher-order abstract syntax as found

in the programming and reasoning environment Beluga. However,  to reason about these applications, we need to introduce meta2-variables which can characterize the dependency on meta-variables and bound variables. In other words, we must go beyond a  two-level system which distinguishes between meta-variables and bound variables.   

In this paper we generalize and extend contextual type theory to multiple levels by indexing variables with their respective level. We give a decidable bi-directional type system which characterizes beta-eta normal forms together with a generalized substitution operation.

Ranald Clouston

Nominal Logic with Equations Only

Many formal systems, particularly in computer science, may be captured by equations modulated by side conditions asserting the ``freshness of names''; these can be reasoned about with Nominal Equational Logic (NEL). Like most logics of this sort NEL employs this notion of freshness as a first class logical connective. However, this can become inconvenient when attempting to translate results from standard equational logic to the nominal setting. This paper presents proof rules for a logic whose only connectives are equations, which we call Nominal Equation-only Logic (NEoL). We prove that NEoL is just as expressive as NEL. We then give a simple description of equality in the empty NEoL-theory, then extend that result to describe freshness in the empty NEL-theory.

Derek Dreyer

MixML Remixed

In a paper at ICFP 2008, Andreas Rossberg and I proposed a novel module system design called MixML, which synthesizes ML modules and Bracha-style ``mixin'' modules in order to provide a seamless integration of hierarchical module composition, translucent ML-style

data abstraction, and mixin-style recursive linking of separately compilable modules.  However, the original paper and conference talk focused primarily on the design and static semantics of MixML. Little attention was paid to its operational semantics, which was defined (in the appendix) via a rather involved destination-passing-style elaboration translation into RTG, a type system for recursively-defined ADTs that I had developed previously.

Since then, however, we have made various improvements to the semantics of MixML.  These include (1) a cleaner and more expressive variant of the internal RTG calculus, employing ``linear reference types'' and ``linear kinds'' to ensure that all term and type components of a MixML module are defined exactly once, and (2) a careful description of the full three-pass typechecking algorithm for MixML modules and its soundness.  In this talk, I will give a brief overview of our remixed MixML, and highlight the improvements to its semantics (which are covered in a brand new journal version of our paper, presently under submission).

Murdoch Gabbay and Dominic Mulligan

Nominal semantics of simply-typed lambda-calculus

We investigate a new class of models for the simply typed lambda-calculus in which variables map to names in the denotation and lambda-abstraction maps to a (non-functional) name-abstraction operation. The resulting denotations are smaller and better-behaved, in ways we make precise, than functional valuation-based models. Using these new models, we then develop a generalisation of lambda-term syntax enriching them with meta-variables, thus yielding a theory of incomplete functions. This incompleteness is orthogonal to the usual notion of incompleteness given by function abstraction and application, and corresponds to holes and incomplete objects.

Alan J. Martin and Amy Felty

An Improved Implementation and Abstract Interface for Hybrid

Hybrid is a formal theory implemented in Isabelle/HOL that provides an interface for representing and reasoning about object languages using higher-order abstract syntax (HOAS).  This interface is built around an HOAS variable-binding operator that is constructed definitionally from a de Bruijn index representation.  In this paper we make a variety of improvements to Hybrid, culminating in an abstract interface that on one hand makes Hybrid a more mathematically satisfactory theory, and on the other hand has important practical benefits.  We start with a modification of Hybrid's type of terms that better hides its implementation in terms of de Bruijn indices, by excluding at the type level terms with dangling indices.  We present an improved set of definitions, and a series of new lemmas that provide a complete characterization of Hybrid's primitives in terms of properties stated at the HOAS level.  Benefits of this new package include a new proof of adequacy and improvements to reasoning about object logics.  Such proofs are carried out at the higher level with no involvement of the lower level de Bruijn syntax.

Aleksandar Nanevski

How to make ad hoc proof automation less ad hoc

Most interactive theorem provers provide support for some form of user-customizable proof automation. In a number of popular systems, such as Coq and Isabelle, this automation is achieved primarily through tactics, which are programmed in a separate language from that of the prover’s base logic. While tactics are clearly useful in practice, they can be difficult to maintain and compose because, unlike lemmas, their behavior cannot be specified within the expressive type system of the prover itself.

In this talk, I will present a novel approach to proof automation in Coq that allows the user to specify the behavior of custom automated routines in terms of Coq’s own type system. The approach involves a sophisticated application of Coq’s canonical structures, which generalize Haskell type classes and facilitate a flexible style of dependently-typed logic programming. Specifically, just as Haskell type classes are used to infer the canonical implementation of an overloaded term at a given type, canonical structures can be used to infer the canonical proof of an overloaded lemma for a given instantiation of its parameters.  I will also present a few design patterns for canonical structure programming that enable one to carefully and predictably coax Coq’s type inference engine into triggering the execution of user-supplied algorithms during unification.

This is joint work with Georges Gonthier, Beta Ziliani and Derek Dreyer.

Michael Norrish

Syntax: Getting Over It Already?

With reference to some of my recent work, I discuss the extent to which syntax is a solved problem.  If it is, what is the natural thing to do next? If it isn't, where do the remaining problems lie? I offer mechanized computability theory as an example of a subject domain that opens up when syntax is easy. On the pessimistic side of things, I describe the issues I see with attempting a mechanization of (co-algebraic) Bohm trees.