Beluga: a framework for programming and reasoning with deductive systems

IJCAR 2010 (Edinburgh, July 2010)

Brigitte Pientka and Joshua Dunfield

Abstract

Beluga is an environment for programming and reasoning about formal systems given by axioms and inference rules. It implements the logical framework LF for specifying and prototyping formal systems via higher-order abstract syntax. It also supports reasoning: the user implements inductive proofs about formal systems as dependently typed recursive functions. A distinctive feature of Beluga is that it not only represents binders using higher-order abstract syntax, but directly supports reasoning with contexts. Contextual objects represent hypothetical and parametric derivations, leading to compact and elegant proofs. Our test suite includes standard examples such as the Church-Rosser theorem, type uniqueness, proofs about compiler transformations, and preservation and progress for various ML-like languages. We also implemented proofs of structural properties of expressions and paths in expressions. Stating these properties requires nesting of quantifiers and implications, demonstrating the expressive power of Beluga.

Final version (April 2010)

BibTeX entry

@InProceedings{Pientka10:Beluga,
    author    = {Brigitte Pientka and Joshua Dunfield},
    title     = {{Beluga}: A Framework for Programming and Reasoning with Deductive Systems (System Description)},
    booktitle = {Int'l Joint Conference on Automated Reasoning (IJCAR 2010)},
    pages     = {15--21},
    month     = jul,
    year      = {2010}
}
  

all papers * related papers
Joshua Dunfield