Case analysis of higher-order data

LFMTP 2008 (Pittsburgh, June 2008)

Jana Dunfield and Brigitte Pientka

Abstract

We discuss coverage checking for data that is dependently typed and is defined using higher-order abstract syntax. Unlike previous work on coverage checking that required objects to be closed, we consider open data objects, i.e. objects that may depend on some context. Our work may therefore provide insights into coverage checking in Twelf, and serve as a basis for coverage checking in functional languages such as Delphin and Beluga. More generally, our work is a foundation for proofs by case analysis in systems that reason about higher-order abstract syntax.

Online version (includes appendix) (June 2008)

BibTeX entry

@InProceedings{Dunfield08:coverage,
    author    = {Jana Dunfield and Brigitte Pientka},
    title     = {Case analysis of higher-order data},
    booktitle = {Int'l Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'08)},
    OPTpages  = {},
    month     = jun,
    year      = {2008},
    OPTeditor = {},
    series    = {Electronic Notes in Theoretical Computer Science (ENTCS)},
    publisher = {Elsevier}
}

all papers * related papers

J. Dunfield