Two Drafts on Dependent Types

I have two new draft papers to publicize. The first is a paper with Pierre Pradic and Nick Benton:

• Integrating Linear and Dependent Types, Neelakantan R. Krishnaswami, Pierre Pradic, Nick Benton. The technical report with proofs is also available.

  In this paper, we show how to integrate linear types with type dependency, by extending the linear/non-linear calculus of Benton to support type dependency.

  Next, we give an application of this calculus by giving a proof-theoretic account of imperative programming, which requires extending the calculus with computationally irrelevant quantification, proof irrelevance, and a monad of computations. We show the soundness of our theory by giving a realizability model in the style of Nuprl, which permits us to validate not only the β-laws for each type, but also the η-laws.

  These extensions permit us to decompose Hoare triples into a collection of simpler type-theoretic connectives, yielding a rich equational theory for dependently-typed higher-order imperative programs. Furthermore, both the type theory and its model are relatively simple, even when all of the extensions are considered.

Sometimes, it seems like every problem in programming languages research can be solved by either linear types, or dependent types. So why not combine them, and see what happens?

• Mtac: A Monad for Typed Tactic Programming in Coq, Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis.

  A website with Coq source and tutorial is available.

  Effective support for custom proof automation is essential for large-scale interactive proof development. However, existing languages for automation via tactics either (a) provide no way to specify the behavior of tactics within the base logic of the accompanying theorem prover, or (b) rely on advanced type-theoretic machinery that is not easily integrated into established theorem provers.

  We present Mtac, a lightweight but powerful extension to Coq that supports dependently-typed tactic programming. Mtac tactics have access to all the features of ordinary Coq programming, as well as a new set of typed tactical primitives. We avoid the need to touch the trusted kernel typechecker of Coq by encapsulating uses of these new tactical primitives in a monad, and instrumenting Coq so that it executes monadic tactics during type inference.

Since I'm not the main author of this paper, I feel free to say this is really good! Mtac manages to strike a really amazing balance of simplicity, cleanliness, and power. It's really the first tactic language that I want to implement (rather than grudgingly accepting the necessity of implementing).