Wednesday, July 9, 2014

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).

Tuesday, July 1, 2014

PhD opportunities at the University of Birmingham

My university, the University of Birmingham, is looking for applicants to the CS PhD program. I'm putting our advertisement on my blog, in case you (or your students, if you're a professor) are looking for a graduate program -- well, we're looking for students! We have an imminent funding deadline -- please contact us immediately if you are interested!

We invite applications for PhD study at the University of Birmingham.

We are a group of (mostly) theoretical computer scientists who explore fundamental concepts in computation and programming language semantics. This often involves profound and surprising connections between different areas of computer science and mathematics. From category theory to lambda-calculus and computational effects, from topology to constructive mathematics, from game semantics to program compilation, this is a diverse field of research that continues to provide new insight and underlying structure.

  • See our webpage, with links to individual researchers, here:

  • Information about PhD applications may be found here:

  • If you are considering applying, please contact any of us. We will be very happy to discuss the opportunities available.
    • Martin Escardo (topology, computation with infinite objects, constructive mathematics, intuitionistic type theory)
    • Dan Ghica (game semantics, heterogeneous computing, model checking)
    • Achim Jung (mathematical structures in the foundations of computing: logic, topology, order)
    • Neel Krishnaswami (type theory, verification, substructural logic, interactive computation)
    • Paul Levy (denotational semantics, lambda-calculus with effects, nondeterminism, category theory, game semantics)
    • Uday Reddy (semantics of state, separation logic)
    • Eike Ritter (security protocol verification)
    • Hayo Thielecke (abstract machines, concurrent and functional programming, software security)
    • Steve Vickers (constructive mathematics and topology, category theory and toposes)