# LFMTP on Wednesday, July 14th

10:25‑10:30 Opening
Location: AT 2.12
 10:25 Marino Miculan Welcome
10:30‑12:30 Formalizations
Chair: Amy Felty
Location: AT 2.12
14:00‑15:00 Implementations
Chair: Andy Pitts
Location: AT 2.12
 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‑17:00 HOAS and Invited Speaker 1
Chair: Carsten Schuermann
Location: AT 2.12
 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‑18:00 Invited speaker 2
Chair: Marino Miculan
Location: AT 2.12
 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]
18:00‑18:10 Closing
Location: AT 2.12
 18:00 Marino Miculan Closing