### Skapa referens, olika format (klipp och klistra)

**Harvard**

Bove, A., Dybjer, P. och Sicard-Ramírez, A. (2012) *Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs*.

** BibTeX **

@conference{

Bove2012,

author={Bove, Ana and Dybjer, Peter and Sicard-Ramírez, Andrés},

title={Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs},

booktitle={Lecture Notes in Computer Science. 15th International Conference on Foundations of Software Science and Computational Structures, Tallinn, 24 March - 1 April 2012},

isbn={978-3-642-28728-2},

pages={104-118},

abstract={ We propose a new approach to the computer-assisted verification of
functional programs. We work in first order theories of functional
programs which are obtained by extending Aczel's first order theory
of combinatory formal arithmetic with positive inductive and
coinductive predicates. Rather than building a special purpose
system we implement our theories in Agda, a proof assistant for
dependent type theory which can be used as a generic theorem
prover. Agda provides support for interactive reasoning by encoding
first order theories using the formulae-as-types principle. Further
support is provided by off-the-shelf automatic theorem provers for
first order logic which can be called by a program which translates
Agda representations of first order formulae into the TPTP language
understood by the provers. We show some examples where we combine
interactive and automatic reasoning, covering both proof by
induction and coinduction.},

year={2012},

}

** RefWorks **

RT Conference Proceedings

SR Electronic

ID 159212

A1 Bove, Ana

A1 Dybjer, Peter

A1 Sicard-Ramírez, Andrés

T1 Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs

YR 2012

T2 Lecture Notes in Computer Science. 15th International Conference on Foundations of Software Science and Computational Structures, Tallinn, 24 March - 1 April 2012

SN 978-3-642-28728-2

SP 104

OP 118

AB We propose a new approach to the computer-assisted verification of
functional programs. We work in first order theories of functional
programs which are obtained by extending Aczel's first order theory
of combinatory formal arithmetic with positive inductive and
coinductive predicates. Rather than building a special purpose
system we implement our theories in Agda, a proof assistant for
dependent type theory which can be used as a generic theorem
prover. Agda provides support for interactive reasoning by encoding
first order theories using the formulae-as-types principle. Further
support is provided by off-the-shelf automatic theorem provers for
first order logic which can be called by a program which translates
Agda representations of first order formulae into the TPTP language
understood by the provers. We show some examples where we combine
interactive and automatic reasoning, covering both proof by
induction and coinduction.

LA eng

DO 10.1007/978-3-642-28729-9_7

LK http://dx.doi.org/10.1007/978-3-642-28729-9_7

OL 30