Programming with proofs and explicit contexts

PPDP 2008 (Valencia, Spain, July 2008)

Brigitte Pientka and Joshua Dunfield

Abstract

This paper explores a new point in the design space of functional programming: functional programming with dependently-typed higher-order data structures described in the logical framework LF. This allows us to program with proofs as higher-order data. We present a decidable bidirectional type system that distinguishes between dependently-typed data and computations. To support reasoning about open data, our foundation makes contexts explicit. This provides us with a concise characterization of open data, which is crucial to elegantly describe proofs. In addition, we present an operational semantics for this language based on higher-order pattern matching for dependently typed objects. Based on this development, we prove progress and preservation.

Final version (May 2008)

BibTeX entry

  @InProceedings{Pientka08:DependentBeluga,
    author    = {Brigitte Pientka and Joshua Dunfield},
    title     = {Programming with proofs and explicit contexts},
    booktitle = {Principles and Practice of Declarative Programming (PPDP'08)},
    pages =     {163--173},
    month =     jul,
    year =      {2008},
    publisher = {ACM Press}
  }
  

all papers * related papers
Joshua Dunfield