| 9:30-10:00 | Coffee, hanging out, chatting ... |
| 10:00-10:45 | David August, Princeton |
| 10:45-11:30 | Brian Aydemir, UPenn |
| 11:30-12 | Yitzhak Mandelbaum, AT&T |
| 12-1:15 | Lunch |
| 1:15-1:30 | Business: Organizing the next NJPLS |
| 1:30-2:15 | Jeffrey Siskind, Purdue |
| 2:15-3pm | Adriana Compagnoni, Stevens |
| 3-3:30 | Short Talks (5-10min each) |
Given the complexity of the metatheoretic reasoning involved with current programming languages and their type systems, techniques for mechanical formalization and checking of the metatheory have received much recent attention. In previous work, we advocated a combination of locally nameless representation and cofinite quantification as a lightweight style for carrying out such formalizations in the Coq proof assistant. As part of the presentation of that methodology, we described a number of operations associated with variable binding and listed a number of properties, called ``infrastructure lemmas,'' about those operations that needed to be shown. The proofs of these infrastructure lemmas are generally straightforward, given a specification of the binding structure of the language.
In this work, we present LNgen, a prototype tool for automatically generating these definitions, lemmas, and proofs from Ott-like language specifications. Furthermore, the tool also generates a recursion scheme for defining functions over syntax, which was not available in our previous work. We also show the soundness and completeness of our tool's output. For untyped lambda terms, we prove the adequacy of our representation with respect to a fully concrete representation, and we argue that the representation is complete--- that we generate the right set of lemmas---with respect to Gordon and Melham's ``Five Axioms of Alpha-Conversion.'' Finally, we claim that our recursion scheme is simpler to work with than either Gordon and Melham's recursion scheme or the recursion scheme of Nominal Logic.
Type theories with higher-order subtyping or singleton types are examples of systems where computation rules for variables are affected by type information in the context. A complication for these systems is that bounds declared in the context do not interact well with the logical relation proof of completeness or termination.
This paper proposes a natural modification to the type syntax for F-omega-sub , adding a variable’s bound to the variable type constructor, thereby separating the com- putational behavior of the variable from the context. In the algorithm that compares whether two types are in the subtyping relation, a variable may become its bound using the rule of Promotion. Traditionally, the bound of a variable is recorded in the context, so the subtyping relation depends on the context, creating meta-theoretic complications that are not essential to the subtyping problem but introduced by the occurrence of the bound in the context. By taking the bound out of the con- text and placing it in the variable, the need for ad hoc results about the context disappears. The algorithm for subtyping in F-omega-sub can then be given on types without context or kind information. As a con- sequence, the metatheory follows the general approach for type systems without computational information in the context, including a simple logical relation defini- tion without Kripke-style indexing by context. Com- pleteness and correctness, anti-symmetry, transitivity elimination and termination of the algorithm are all proved. Finally, this new presentation of the system is shown to be equivalent to the traditional presentation without bounds on the variable type constructor.
It is extremely useful to be able to take derivatives of functions expressed as computer programs to support function optimization and approximation, parameter estimation, machine learning, and ultimately computational science and engineering design. The established discipline of Automatic Differentiation (AD) has largely focussed on imperative languages, where it is most efficiently implemented as a source-to-source transformation performed by a preprocessor. This talk will present a novel formulation of AD for functional programs expressed in the lambda calculus. A key novel aspect of our formulation is that AD is performed by higher-order functions that reflectively transform closure bodies. Our methods exhibit an important closure property that prior AD formulations lack: the ability to transform the entire space of input programs, including those produced by the AD transformations themselves. This is crucial for solving the kinds of nested optimizations that arise in domains such as game theory and automatic control. Furthermore, since the input and output of our transformations is the lambda calculus, efficient implementation is facilitated by novel extensions of standard compilation techniques. We exhibit a novel "almost" union-free polyvariant flow-analysis algorithm, formulated as abstract interpretation, that partially evaluates calls to the AD operators, migrating reflective source-to-source transformation to compile time. This yields code with run-time performance that exceeds the best existing AD implementations for imperative languages by a factor of two and outperforms all AD implementations for functional languages by two to three orders of magnitude.
AD has traditionally been applied to purely numeric programs written in imperative languages like Fortran. Our novel methods can be applied to mixed symbolic-numeric programs written in functional languages. This is useful for developing complex stochastic models such as is done in the emerging field of probabilistic programming. We demonstrate how our methods support this enterprise by constructing evaluators for two different probabilistic programming languages, one based on Scheme and one based on Prolog, and using both forward-mode and reverse-mode variants of our AD methods to take the gradients of such evaluators executing probabilistic programs in their respective target languages in order to perform gradient-based maximum-likelihood estimation of the distribution parameters of the free random variables in those programs. We demonstrate that for this domain our methods yield performance that exceeds straightforward implementation of AD in functional languages by many orders of magnitude.
Joint work with Barak A. Pearlmutter.
The Yakker project aims to improve the security and robustness of externally-facing software. In particular, Yakker focuses on protecting software from malicious or erroneous inputs and outputs through grammar-style specifications. The Yakker project has a number of components, including a system for extracting grammars from RFCs and generating parsing- and printing-related libraries and tools from those grammars; a language for specifying grammar- refinement rules which can be used both for crafting malicious inputs (e.g., for penetration testing) and for protecting against them (e.g. intrusion detection); a general-purpose context-sensitive grammar specification language; and a parsing virtual machine for improving the portability and modularity of parser/printer generators.
In this talk, I will review why today's software needs input/output protection and will provide a brief synopsis of each component of the Yakker project.