Sciweavers

Share
CADE
2010
Springer

Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)

11 years 2 months ago
Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
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 er-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 repbinders 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 po...
Brigitte Pientka, Joshua Dunfield
Added 08 Nov 2010
Updated 08 Nov 2010
Type Conference
Year 2010
Where CADE
Authors Brigitte Pientka, Joshua Dunfield
Comments (0)
books