10:30 | Dan Licata and Robert Harper A Monadic Formalization of ML5 ML5 is a programming language for spatially distributed computing, based on a Curry-Howard correspondence with the modal logic S5. Despite being designed by a correspondence with S5 modal logic, the ML5 programming language differs from the logic in several ways. In this paper, we explain these discrepancies between ML5 and S5 by translating ML5 into a slightly different logic: intuitionistic S5 extended with a lax modality that encapsulates effectful computations in a monad. This translation both explains the existing ML5 design and suggests some simplifications and generalizations. We have formalized our translation within the Agda proof assistant. Rather than formalizing lax S5 as a proof theory, we \emph{embed} it as a universe within the the dependently typed host language, with the universe elimination given by implementing the modal logic's Kripke semantics. This representation technique saves us the work of defining a proof theory for the logic and proving it correct, and additionally allows us to inherit the equational theory of the meta-language, which can be exploited in proving that the semantics validates the operational semantics of ML5. |

11:00 | Herman Geuvers, Robbert Krebbers, James McKinna and Freek Wiedijk Pure Type Systems without Explicit Contexts We present an approach to type theory in which the typing judgments do not have explicit contexts. Instead of judgments of the shape "Gamma |- A : B", our systems just have judgments of the shape "A : B". An essential feature of our systems is that already in pseudo-terms we distinguish the free from the bound variables. Specifically we give the rules of the "Pure Type System" class of type theories in this style. We prove that the type judgments of these systems corresponds in a natural way with the judgments of the traditionally formulated Pure Type Systems. I.e., our systems have exactly the same well-typed terms as traditional presentations of type theory. Our system can be seen as a type theory in which all type judgments share an identical, infinite, typing context that has infinitely many variables for each possible type. For this reason we call our system "Gamma infinity". This name means to suggest that our type judgment "A : B" should be read as "Gamma_infinity |- A : B", with a fixed infinite type context called "Gamma_infinity". |

11:30 | Florian Rabe Representing Isabelle in LF LF has been designed and successfully used as a meta-logical framework to represent and reason about object logics. Here we give a representation of the Isabelle logical framework in LF using the recently introduced module system for LF. The major novelty of our approach is that we can naturally represent the advanced Isabelle features of type classes and locales. Our representation of type classes relies on a feature so far lacking in the LF module system: structure variables and abstraction over them. While conservative over the present system in terms of expressivity, this feature is needed for a representation of type classes that preserves the modular structure. Therefore, we also design the necessary extension of the LF module system. |

12:00 | Andreas Abel and Brigitte Pientka Explicit substitutions for contextual type theory In this paper, we present an explicit substitution calculus which distinguishes between ordinary bound variables and meta-variables. Its typing discipline is derived from contextual modal type theory. We first present a dependently typed lambda calculus with explicit substitutions for ordinary variables and explicit meta-substitutions for meta-variables. We then present a weak head normalization procedure which performs both substitutions lazily and in a single pass thereby combining substitution walks for the two different classes of variables. Finally, we prove normalization which entails decidability of bidirectional type checking. As an important application, we illustrate how the presented calculus can serve as a foundation for implementing the Beluga language which supports programming and reasoning with formal systems specified in the logical framework LF. |

14:00 | Anders Schack-Nielsen and Carsten Schuermann Pattern Unification for the Lambda Calculus with Linear and Affine Types We define the pattern fragment for higher-order unification problems in linear and affine type theory and give a deterministic unification algorithm that computes most general unifiers. |

14:30 | Maribel Fernandez and Murdoch Gabbay Closed nominal rewriting and efficiently computable nominal algebra equality We analyse the relationship between nominal algebra and nominal rewriting, giving a new and concise presentation of equational deduction in nominal theories. With some new results, we characterise a subclass of equational theories for which nominal rewriting provides a complete procedure to check nominal algebra equality. This subclass includes specifications of lambda-calculus and first-order logic. |

15:30 | John Boyland Generating Bijections between HOAS and the Natural Numbers A provably correct bijection between higher-order abstract syntax (HOAS) and the natural numbers enables one to define a ``not equals'' relationship between terms and also to have an adequate encoding of sets of terms. Since creating such bijections is tedious and error-prone, we have created a ``bijection generator'' that generates such bijections automatically together with proofs of correctness, all in the context of Twelf. |

16:00 | Chung-chieh Shan (Rutgers, The State University of New Jersey) Typed metaprogramming with effects Metaprogramming is a popular and effective way to reconcile modularity with efficiency in software. For example, a modular metaprogram for the Fourier transform can generate a variety of implementations optimized for different problem sizes, number representations, and processor architectures. Metaprogramming is also a widespread phenomenon in human language, especially when agents ascribe beliefs to each other. For example, people quote fragments from each other’s utterances in order to curate meanings from each other’s minds. In both settings, it is natural to extend the metalanguage with side effects, in particular delimited control effects. This extension lets metaprograms take advantage of the fact that the binding context of the object language often follows the evaluation context of the metalanguage. Such a combination of metaprogramming and effects provides a benchmark problem for mechanized metatheory. To assure that object expressions stay well-formed, we impose a type system on metaprograms that incorporates two ideas from the literature: answer types, which track delimited control effects, and environment classifiers, which track object variable references. Unlike previous systems, this system lets effects reach beyond binders, so it supports loop-invariant code motion and inverse quantifier scope. |

17:00 | Frank Pfenning (Carnegie Mellon University) The Practice and Promise of Substructural Frameworks Logical frameworks are based on the premise that fundamental concepts and constructions in the definition of logics and programming languages should be directly supported in the framework. For LF, these include variable binding, substitution, as well as parametric and hypothetical judgments. Absent are intrinsic notions of state, consumable resource, or concurrency, which appear to be similarly fundamental. Integrating these into logical frameworks has led to the development of substructural frameworks such as LLF (linear), RLF (relevant), OLF (ordered), CLF (concurrent) and HLF (hybrid). A promising related specification technique for programming languages is substructural operational semantics (SSOS). We illustrate this technique and the logical framework features that support it through several sample programming constructs. We also sketch our current approach to analyzing such specifications, which has been the most challenging part in the development of the next generation of logical frameworks. [Joint work with Jason Reed and Rob Simmons] |