Invited Talks

  • Ana Bove, Chalmers University
    10 Years of Partiality and General Recursion
    Abstract
  • Matthieu Sozeau, Harvard University
    Elaborations in Type Theory
    Abstract

Contributed Talks

  • Andreas Abel,
      Parametric Dependent Function Types
  • Edwin Brady,
      Practical, efficient programming with dependent types
  • James Caldwell,
      Extracting Monadic Programs form Proofs,
    (joint work with Josef Pohl)
  • Adam Chlipala,
      Generating Pieces of Web Applications with Type-Level Programming
  • Nils Anders Danielsson,
      TBA
  • Larry Diehl,
      Unit & integration test composition via lemmas
  • Makoto Hamana,
      Another Initial Algebra Semantics of Inductive Families for Programming
  • Hugo Herbelin,
      A sequent calculus presentation of the Calculus of Inductive Constructions
    (joint work with Jeffrey Sarnat, Vincent Siles), abstract
  • Cezar Ionescu,
      Using dependent types in models of climate change impacts
    abstract
  • Karim Kariso,
      Integrating Agda and Automated Theorem Proving Techniques
    (joint work with Anton Setzer)
  • Dan Licata,
      Security-Typed Programming within Dependently Typed Programming
    (joint work with Jamie Morgenstern)
  • Ulf Norell,
      TBA
  • Brigitte Pientka,
      Type reconstruction in dependently typed programming
    , abstract
  • Carsten Schuermann,
      The HOL-Nuprl connection in Delphin,
    (joint work with Adam Poswolsky), abstract
  • Anton Setzer,
      Coalgebras in dependent type theory
  • Antonis Stampoulis,
      VeriML: Type-safe computation of logical terms inside a language with effects,
    abstract
  • Tarmo Uustalu,
      Safely navigable datastructures with cycles and sharing",
    (joint work with Varmo Vene, deriving from a collaboration with Makoto Hamana).
  • Sean Wilson,
      Supporting Dependently Typed Functional Programming with Proof Automation and Testing,
    abstract