Computation-as-deduction in Abella: work in progress

Kaustuv Chaudhuri 1 Ulysse Gérard 1 Dale Miller 1
1 PARSIFAL - Proof search and reasoning with logic specifications
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
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 even when data structures contain bindings.
Complete list of metadatas

Cited literature [12 references]  Display  Hide  Download

https://hal.inria.fr/hal-01806154
Contributor : Ulysse Gérard <>
Submitted on : Friday, June 1, 2018 - 4:38:00 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:29 PM
Long-term archiving on : Sunday, September 2, 2018 - 3:36:23 PM

File

paper.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01806154, version 1

Citation

Kaustuv Chaudhuri, Ulysse Gérard, Dale Miller. Computation-as-deduction in Abella: work in progress. 13th international Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Jul 2018, Oxford, United Kingdom. ⟨hal-01806154⟩

Share

Metrics

Record views

328

Files downloads

60