@inproceedings{Bove2012,
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.},
author = {Bove, Ana and Dybjer, Peter and Sicard-Ram{\'{i}}rez, Andr{\'{e}}s},
booktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},
doi = {10.1007/978-3-642-28729-9_7},
file = {:Users/jonaprieto/Mendeley/Bove, Dybjer, Sicard-Ram{\'{i}}rez - 2012 - Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs.pdf:pdf},
isbn = {9783642287282},
issn = {03029743},
pages = {104--118},
publisher = {Springer},
title = {{Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs}},
url = {http://link.springer.com/chapter/10.1007/978-3-642-28729-9_7},
volume = {7213 LNCS},
year = {2012}
}

{"_id":"azqr4MTA5RP3Dty4k","bibbaseid":"bove-dybjer-sicardramirez-combininginteractiveandautomaticreasoninginfirstordertheoriesoffunctionalprograms-2012","downloads":0,"creationDate":"2017-09-01T03:35:40.528Z","title":"Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs","author_short":["Bove, A.","Dybjer, P.","Sicard-Ramírez, A."],"year":2012,"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/jonaprieto/athena/master/paper/ref.bib","bibdata":{"bibtype":"inproceedings","type":"inproceedings","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.","author":[{"propositions":[],"lastnames":["Bove"],"firstnames":["Ana"],"suffixes":[]},{"propositions":[],"lastnames":["Dybjer"],"firstnames":["Peter"],"suffixes":[]},{"propositions":[],"lastnames":["Sicard-Ramírez"],"firstnames":["Andrés"],"suffixes":[]}],"booktitle":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)","doi":"10.1007/978-3-642-28729-9_7","file":":Users/jonaprieto/Mendeley/Bove, Dybjer, Sicard-Ramírez - 2012 - Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs.pdf:pdf","isbn":"9783642287282","issn":"03029743","pages":"104--118","publisher":"Springer","title":"Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs","url":"http://link.springer.com/chapter/10.1007/978-3-642-28729-9_7","volume":"7213 LNCS","year":"2012","bibtex":"@inproceedings{Bove2012,\nabstract = {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.},\nauthor = {Bove, Ana and Dybjer, Peter and Sicard-Ram{\\'{i}}rez, Andr{\\'{e}}s},\nbooktitle = {Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)},\ndoi = {10.1007/978-3-642-28729-9_7},\nfile = {:Users/jonaprieto/Mendeley/Bove, Dybjer, Sicard-Ram{\\'{i}}rez - 2012 - Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs.pdf:pdf},\nisbn = {9783642287282},\nissn = {03029743},\npages = {104--118},\npublisher = {Springer},\ntitle = {{Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs}},\nurl = {http://link.springer.com/chapter/10.1007/978-3-642-28729-9_7},\nvolume = {7213 LNCS},\nyear = {2012}\n}\n","author_short":["Bove, A.","Dybjer, P.","Sicard-Ramírez, A."],"key":"Bove2012","id":"Bove2012","bibbaseid":"bove-dybjer-sicardramirez-combininginteractiveandautomaticreasoninginfirstordertheoriesoffunctionalprograms-2012","role":"author","urls":{"Paper":"http://link.springer.com/chapter/10.1007/978-3-642-28729-9_7"},"downloads":0},"search_terms":["combining","interactive","automatic","reasoning","first","order","theories","functional","programs","bove","dybjer","sicard-ramírez"],"keywords":[],"authorIDs":[],"dataSources":["8jafqMAWgB7XP4FTZ"]}