Computation-as-deduction in Abella: work in progress

Authors: Kaustuv Chaudhuri, Ulysse Gérard and Dale Miller

Paper Information

Title:Computation-as-deduction in Abella: work in progress
Authors:Kaustuv Chaudhuri, Ulysse Gérard and Dale Miller
Proceedings:LFMTP Regular papers
Editors: Giselle Reis and Frédéric Blanqui
Keywords:computation and deduction, Abella, functional and relational specifications

ABSTRACT. The Abella theorem prover is based on a logic in which relations, and not functions, are defined by induction (and coinduction). Of course, many relations do, in fact, define functions and there is real value in separating functional computation (marked by determinism) from more general deduction (marked by nondeterminism and backtracking). Recent work on focused proof systems for the logic underlying Abella is used in this paper to motivate the design of various extensions to the Abella system. With these extensions to the system (which do not extend the logic), it is possible to fully automate functional computations within the relational setting as soon as a proof is provided that a given relation does, in fact, capture a total function. In this way, we can use Abella to compute functions on data structures that contain bindings.

Talk:Jul 07 12:00 (Session 26H: Verification and Testing)