LFMTP on Wednesday, August 16th

Session 1 (09:00‑10:30)

09:00‑09:30	Alwen Tiu (Australian National University) A Logic for Reasoning about Generic Judgments This paper presents an extension of a proof system for encoding generic judgments, the logic FOLD-nabla of Miller and Tiu, with an induction principle. The logic FOLD-nabla is itself an extension of intuitionistic logic with fixed points and a ``generic quantifier'', nabla, which is used to reason about the dynamics of bindings in object systems encoded in the logic. A previous attempt to extend FOLD-nabla with an induction principle has been unsuccessful in modeling some behaviours of bindings in inductive specifications. It turns out that this problem can be solved by relaxing some restrictions on nabla, in particular by adding the axiom B <=> nabla x. B, where x is not free in B. We show that by adopting the equivariance principle, the presentation of the extended logic can be much simplified. Cut-elimination for the extended logic is stated, and some applications in reasoning about an object logic and a simply typed lambda-calculus are illustrated.
09:30‑10:00	Ulrich Schoepp (LMU Munich) Modelling Generic Judgements We propose a semantics for the $\nabla$-quantifier of Miller and Tiu. First we consider the case for classical first-order logic. In this case, the interpretation is close to standard Tarski-semantics and completeness can be shown using a standard argument. Then we put our semantics into a broader context by giving a general interpretation of $\nabla$ in categories with binding structure. Since categories with binding structure also encompass nominal logic, we thus show that both $\nabla$-logic and nominal logic can be modelled using the same definition of binding. As a special case of the general semantics in categories with binding structure, we recover Gabbay and Cheney's translation of generic judgements into nominal logic.
10:00‑10:30	Murdoch Gabbay (Heriot-Watt University) Hierarchical nominal rewriting Nominal rewriting introduced a novel method of specifying rewriting on syntax-with-binding. We extend this treatment of rewriting with hierarchy of variables representing increasingly 'meta-level' variables, e.g. in hierarchical nominal rewriting the meta-level unknowns in a rewrite rule, which represent unknown terms, can be "folded into" the syntax itself (and rewritten); to the extent that rewriting can be thought of as a general framework for logic and computation, and nominal rewriting as such a framework with native support for logic and computation in the presence of binders, we can think of hierarchical nominal rewriting as a meta-to-the-omega level theory of logic and computation with binders.

Break (10:30‑11:00)

Session 2 (11:00‑12:30)

11:00‑11:30	Stefan Berghofer (Technische Universität München) Christian Urban (Technical University of Munich) A Head-to-Head Comparison of de Bruijn Indices and Names Often debates about pros and cons of various techniques for formalising lambda-calculi rely on subjective arguments, such as de Bruijn indices are hard to read for humans or nominal approaches come close to the style of reasoning employed in informal proofs. In this paper we will compare a four formalisations based on de Bruijn indices and on names from the nominal logic work, thus providing some hard facts about the pros and cons of these two formalisation techniques. We conclude that the relative merits of the different approaches, as usual, depend on what task one has at hand and which goals one pursues with a formalisation.
11:30‑12:00	Brian Aydemir (Department of Computer and Information Science, University of Pennsylvania) Aaron Bohannon (Department of Computer and Information Science, University of Pennsylvania) Stephanie Weirich (Department of Computer and Information Science, University of Pennsylvania) Nominal Reasoning Techniques in Coq We explore an axiomatized nominal approach to variable binding in Coq, using an untyped lambda-calculus as our test case. In our nominal approach, alpha-equality of lambda terms coincides with Coq's built-in equality. Our axiomatization includes a nominal induction principle and functions for calculating free variables and substitution. These axioms are collected in a module signature and proved sound using locally nameless terms as the underlying representation. Our experience so far suggests that it is feasible to work from such axiomatized theories in Coq and that the nominal style of variable binding corresponds closely with paper proofs. We are currently working on proving the soundness of a primitive recursion combinator and developing a method of generating these axioms and their proof of soundness from a grammar describing the syntax of terms and binding.
12:00‑12:30	Jason Hickey (California Institute of Technology) Aleksey Nogin (California Institute of Technology) Xin Yu (California Institute of Technology) Alexei Kopylov (California Institute of Technology) Practical Reflection for Sequent Logics It is well-known that adding reflective reasoning can tremendously increase the power of a proof assistant. In order for this theoretical increase of power to become accessible to users in practice, the proof assistant needs to provide a great deal of infrastructure to support reflective reasoning. In this paper we explore the problem of creating a practical implementation of such a support layer. Our implementation takes a specification of a logical theory (which is identical to how it would be specified if we simply intended to reason within this logical theory, instead of reflecting it) and automatically generates the necessary definitions, lemmas, and proofs that are needed to enable the reflected meta-reasoning in the provided theory. One of the key features of our approach is that the structure of a logic is preserved when it is reflected. In particular, all variables, including meta-variables, are preserved in the reflected representation. This also allows the preservation of proof automation---there is a structure-preserving one-to-one map from proof steps in the original logic to proof step in the reflected logic. To enable reasoning about terms with sequent context variables, we develop a principle for context induction, called teleportation. This work is fully implemented in the MetaPRL theorem prover.

Lunch break (12:30‑14:00)

Invited Talk (14:00‑15:00)

14:00‑15:00

Gordon Plotkin (University of Edinburgh) An Algebraic Framework for Logics and Type Theories It seems a natural principle to seek logical frameworks that are as simple and as weak as possible while still enabling direct natural representations of a wide variety of formalisms. We present an algebraic framework, which can be considered an extension of multi-sorted equational logic with abstraction and dependent types, but with no ability to form compound types (= sorts) and thereby no lambda-abstraction. Abstraction enables the representation of binding mechanisms; dependent types enables, for example, the representation of the proofs of a formula; and it seems that no other representational mechanisms are necessary. We present the system as a combination of two simpler subsystems: one with only parameterisation and one with only dependent sorts. The closest related previous work is the PAL+ system of Z. Luo which also supplies mechanisms for parameterisation and dependency and avoids lambda abstraction; our system is, perhaps, somewhat simpler.

Session 3 (15:00‑15:30)

15:00‑15:30

Andrew Appel (Princeton University) Xavier Leroy (INRIA Rocquencourt) A List-machine Benchmark for Mechanized Metatheory We propose a benchmark to compare theorem-proving systems on their ability to express proofs of compiler correctness. In contrast to the first POPLmark, we emphasize the connection of proofs to compiler implementations, and we point out that much can be done without binders or alpha-conversion. We propose specific criteria for evaluating the utility of mechanized metatheory systems; we have constructed solutions in both Coq and Twelf metatheory, and we draw conclusions about those two systems in particular.

Break (15:30‑16:00)

Session 4 (16:00‑17:30)

16:00‑16:30	Kevin Donnelly (Boston University) Hongwei Xi (Boston University) A Formalization of Strong Normalization for Simply-Typed Lambda-Calculus and System F We formalize in the logical framework ATS/LF a proof based on Tait's method that establishes the simply-typed lambda-calculus being strongly normalizing. In this formalization, we employ higher-order abstract syntax to encode the simply-typed lambda-terms and an inductive datatype to encode the reducibility predicate in Tait's method. The resulting proof is particularly simple and clean when compared to previously formalized ones. In addition, we mention briefly how a proof based on Girard's method can be formalized in a similar fashion that establishes System F being strongly normalizing.
16:30‑17:00	Chad E. Brown (Universitaet des Saarlandes) Encoding Functional Relations in Scunak We describe how a set-theoretic foundation for mathematics can be encoded in the new system Scunak. We then discuss an encoding of the construction of functions as functional relations in untyped set theory. Using the dependent type theory of Scunak, we can define object level application and lambda abstraction operators (in the spirit of higher-order abstract syntax) mediating between functions in the (meta-level) type theory and (object-level) functional relations. The encoding has also been exported to Automath and Twelf.
17:00‑17:30	Mircea Dan Hernest (INRIA - Ecole Polytechnique) Synthesis of moduli of uniform continuity by the Monotone Dialectica Interpretation in the proof-system MinLog We extract on the computer a number of moduli of uniform continuity for the first few elements of a sequence of closed terms *t* of Goedel's *T* of type (Nat=>Nat)=>(Nat=>Nat). The generic solution may then be quickly inferred by the human. The automated synthesis of such moduli proceeds from a proof of the hereditarily extensional equality (~) of *t* to itself, hence a proof in a weakly extensional variant of Berger-Buchholz-Schwichtenberg's system *Z* of *t* (~)_{(Nat=>Nat)=>(Nat=>Nat)} *t*. We use a machine implementation in Schwichtenberg's MinLog proof-system of a non-literal adaptation to Natural Deduction of Kohlenbach's monotone functional interpretation. This novel variant of Monotone Dialectica produces terms in NbE-normal form by means of a recurrent form of partial normalization. Such partial evaluation is strictly necessary.