Sciweavers

Share
BIRTHDAY
2010
Springer

Programming Inductive Proofs - A New Approach Based on Contextual Types

8 years 5 months ago
Programming Inductive Proofs - A New Approach Based on Contextual Types
In this paper, we present an overview to programming with proofs in the reasoning framework, Beluga. Beluga supports the specification of formal systems given by axioms and inference rules within the logical framework LF. It also supports implementing proofs about formal systems as dependently typed recursive functions. What distinguishes Beluga from other frameworks is that it not only represents binders user-order abstract syntax, but directly supports reasoning with contexts and contextual objects. Contextual types allows us to characterize precisely hypothetical and parametric derivations, i.e. derivations which depend on variables and assumptions, and lead to a direct and elegant implementation of inductive proofs as recursive functions. Because of the intrinsic support for binders and contexts, one can think of the design of Beluga as the most advanced technology for specifying and prototyping formal systems together with their meta-theory.
Brigitte Pientka
Added 06 Dec 2010
Updated 06 Dec 2010
Type Conference
Year 2010
Where BIRTHDAY
Authors Brigitte Pientka
Comments (0)
books