bibfile.bib

%% This BibTeX bibliography file was created using BibDesk.
%% http://bibdesk.sourceforge.net/


%% Created for Moa at 2015-02-26 11:06:39 +0000


%% Saved with string encoding Unicode (UTF-8)



@techreport{dixon2007isaplanner,
	Author = {Dixon, Lucas and Johansson, Moa},
	Date-Added = {2015-02-26 11:04:05 +0000},
	Date-Modified = {2015-02-26 11:06:38 +0000},
	Institution = {University of Edinburgh},
	Journal = {DReaM Technical Report (System description)},
	Title = {{IsaPlanner} 2: {A} Proof Planner in {Isabelle}},
	Year = {2007}}

@inproceedings{boogie11why3,
	Abstract = {Why3 is the next generation of the
  Why software verification platform.
  Why3 clearly separates the purely logical
  specification part from generation of verification conditions for programs.
  This article focuses on the former part.
  Why3 comes with a new enhanced language of
  logical specification. It features a rich library of
  proof task transformations that can be chained to produce a suitable
  input for a large set of theorem provers, including SMT solvers,
  TPTP provers, as well as interactive proof assistants.},
	Address = {Wroc\l{}aw, Poland},
	Author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich},
	Booktitle = {Boogie 2011: First International Workshop on Intermediate Verification Languages},
	Date-Added = {2015-02-18 16:03:38 +0000},
	Date-Modified = {2015-02-18 16:03:38 +0000},
	Hal = {http://hal.inria.fr/hal-00790310},
	Keywords = {Why3},
	Month = {August},
	Pages = {53--64},
	Title = {Why3: Shepherd Your Herd of Provers},
	Topics = {team},
	Url = {http://proval.lri.fr/publications/boogie11final.pdf},
	X-Cle-Support = {BOOGIE},
	X-Equipes = {demons PROVAL},
	X-International-Audience = {yes},
	X-Proceedings = {yes},
	X-Support = {article},
	X-Type = {actes_aux},
	Year = 2011,
	Bdsk-Url-1 = {http://proval.lri.fr/publications/boogie11final.pdf}}

@incollection{cite-key,
	Date-Added = {2015-02-18 16:03:11 +0000},
	Date-Modified = {2015-02-18 16:03:11 +0000}}

@incollection{HOWhyML,
	Author = {Martin Clochard and Claude Marche and Andrei Paskevich},
	Booktitle = {Programming Language meets Program Verification},
	Date-Added = {2015-02-18 15:39:04 +0000},
	Date-Modified = {2015-02-18 15:46:26 +0000},
	Publisher = {ACM},
	Title = {Verified Programs with Binders},
	Year = {2014}}

@inproceedings{Why3,
	Author = {Jean-Christophe Filliatre and Andrei Paskevich},
	Booktitle = {ESOP'13 22nd European Symposium on Programming},
	Date-Added = {2015-02-18 09:33:42 +0000},
	Date-Modified = {2015-02-18 09:35:32 +0000},
	Title = {Why3 - {W}here Programs Meet Provers},
	Year = {2013}}

@inproceedings{hipster,
	Author = {Moa Johansson and Dan Ros\'en and Nicholas Smallbone and Koen Claessen},
	Booktitle = {Conference on Intelligent Computer Mathematics},
	Date-Added = {2015-02-17 17:52:58 +0000},
	Date-Modified = {2015-02-17 17:54:54 +0000},
	Title = {Hipster: Integrating Theory Exploration in a Proof Assistant},
	Year = {2014}}

@unpublished{SPASSInduction,
	Author = {Daniel Wand and Christoph Weidenbach},
	Date-Added = {2015-02-17 17:33:48 +0000},
	Date-Modified = {2015-02-17 17:35:24 +0000},
	Note = {https://people.mpi-inf.mpg.de/~dwand/datasup/draft.pdf},
	Title = {Automatic Induction inside Superposition}}

@inproceedings{cvc4,
	Author = {Andrew Reynolds and Viktor Kuncak},
	Booktitle = {Proceedings of VMCAI},
	Date-Added = {2015-02-17 10:43:41 +0000},
	Date-Modified = {2015-02-17 10:45:33 +0000},
	Title = {Induction for {SMT} Solvers},
	Year = {2015}}

@incollection{codegen2,
	Author = {Haftmann, Florian and Nipkow, Tobias},
	Booktitle = {Functional and Logic Programming},
	Editor = {Blume, Matthias and Kobayashi, Naoki and Vidal, Germ{\'a}n},
	Pages = {103-117},
	Publisher = {Springer},
	Series = {LNCS},
	Title = {Code Generation via Higher-Order Rewrite Systems},
	Volume = {6009},
	Year = {2010}}

@misc{blanchettification,
	Author = {Jasmin Christian Blanchette},
	Howpublished = {Personal communication},
	Year = {2013}}

@inproceedings{hipspecCADE,
	Author = {Claessen, Koen and Johansson, Moa and Ros\'en, Dan and Smallbone, Nicholas},
	Booktitle = {Proceedings of the Conference on Automated Deduction (CADE)},
	Pages = {392-406},
	Publisher = {Springer},
	Series = {LNCS},
	Title = {Automating Inductive Proofs using Theory Exploration},
	Volume = {7898},
	Year = {2013}}

@inproceedings{metis,
	Author = {Joe Hurd},
	Booktitle = {Design and Application of Strategies/Tactics in Higher Order Logics (STRATA)},
	Number = {NASA/CP-2003-212448},
	Pages = {56--68},
	Series = {NASA Technical Reports},
	Title = {First-Order Proof Tactics in Higher-Order Logic Theorem Provers},
	Year = {2003}}

@incollection{mash,
	Author = {Kuhlwein, Daniel and Blanchette, Jasmin Christian and Kaliszyk, Cezary and Urban, Josef},
	Booktitle = {Interactive Theorem Proving},
	Pages = {35-50},
	Publisher = {Springer},
	Series = {LNCS},
	Title = {{MaSh}: Machine Learning for {Sledgehammer}},
	Volume = {7998},
	Year = {2013}}

@misc{codegen,
	Author = {Haftmann, Florian and Bulwahn, Lukas},
	Howpublished = {\url{http://isabelle.in.tum.de/doc/codegen.pdf}},
	Title = {Code generation from {Isabelle/HOL} theories},
	Year = {2013}}

@article{sledgehammer,
	Author = {Paulson, Lawrence C and Blanchette, Jasmin Christian},
	Journal = {IWIL-2010},
	Title = {Three years of experience with {Sledgehammer}, a practical link between automatic and interactive theorem provers},
	Year = {2010}}

@article{theorema,
	Author = {Bruno Buchberger and Adrian Creciun and Tudor Jebelean and Laura Kovacs and Temur Kutsia and Koji Nakagawa and Florina Piroi and Nikolaj Popov and Judit Robu and Markus Rosenkranz and Wolfgang Windsteiger},
	Journal = {Journal of Applied Logic},
	Note = {Towards Computer Aided Mathematics},
	Number = {4},
	Pages = {470 - 504},
	Title = {{Theorema}: {Towards} computer-aided mathematical theory exploration},
	Volume = {4},
	Year = {2006}}

@article{buchberger2000theory,
	Author = {Buchberger, Bruno},
	Journal = {Analele Universitatii Din Timisoara, ser. Matematica-Informatica},
	Number = {2},
	Pages = {9--32},
	Title = {Theory exploration with {Theorema}},
	Volume = {38},
	Year = {2000}}

@inproceedings{feat,
	Address = {New York, USA},
	Author = {Dureg{\aa}rd, Jonas and Jansson, Patrik and Wang, Meng},
	Booktitle = {Proceedings of the 2012 Haskell Symposium},
	Numpages = {12},
	Pages = {61--72},
	Publisher = {ACM},
	Series = {Haskell '12},
	Title = {{Feat}: {F}unctional Enumeration of Algebraic Types},
	Year = {2012}}

@misc{hip,
	Author = {Dan Ros\'en},
	Note = {MSc. Thesis, University of Gothenburg},
	Title = {{Proving Equational Haskell Properties using Automated Theorem Provers}},
	Year = {2012}}

@inproceedings{dafny,
	Author = {Leino, K. Rustan},
	Booktitle = {Proceedings of VMCAI},
	Publisher = {Springer},
	Title = {Automating Induction with an {SMT} Solver},
	Year = {2012}}

@inproceedings{Bundy88,
	Author = {Alan Bundy},
	Booktitle = {Proceedings of CADE},
	Pages = {111-120},
	Title = {The Use of Explicit Plans to Guide Inductive Proofs},
	Year = {1988}}

@inproceedings{jasmin-lpar,
	Author = {Jasmin Blanchette and Koen Claessen},
	Booktitle = {Proceedings of LPAR},
	Publisher = {Springer LNCS},
	Title = {Generating Counterexamples for Structural Inductions by Exploiting Nonstandard Models},
	Year = {2010}}

@book{acl2,
	Author = {Kaufmann, Matt and Panagiotis, Manolios and Strother Moore, J},
	Publisher = {Kluwer Academic Publishers},
	Title = {Computer-Aided Reasoning: An Approach},
	Year = {2000}}

@book{isabelle,
	Author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
	Publisher = {Springer},
	Series = {LNCS},
	Title = {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
	Volume = 2283,
	Year = 2002}

@article{isascheme,
	Author = {Montano-Rivas, Omar and McCasland, Roy and Dixon, Lucas and Bundy, Alan},
	Journal = {Expert Systems with Applications},
	Number = {2},
	Numpages = {10},
	Pages = {1637--1646},
	Title = {Scheme-based theorem discovery and concept invention},
	Volume = {39},
	Year = {2012}}

@inproceedings{zeno,
	Author = {Willam Sonnex and Sophia Drossopoulou and Susan Eisenbach},
	Booktitle = {Proceedings of TACAS},
	Pages = {407--421},
	Publisher = {Springer},
	Title = {{Zeno: An automated prover for properties of recursive datatypes}},
	Year = {2012}}

@article{productiveuse,
	Author = {Andrew Ireland and Alan Bundy},
	Journal = {Journal of Automated Reasoning},
	Pages = {79--111},
	Title = {Productive Use of Failure in Inductive Proof},
	Volume = {16},
	Year = {1996}}

@misc{isaplanner2,
	Author = {Lucas Dixon and Moa Johansson},
	Note = {DReaM Technical Report (System description)},
	Title = {Isa{P}lanner 2: A Proof Planner in {I}sabelle},
	Url = {http://dream.inf.ed.ac.uk/projects/isaplanner/docs/isaplanner-v2-07.pdf},
	Year = 2007,
	Bdsk-Url-1 = {http://dream.inf.ed.ac.uk/projects/isaplanner/docs/isaplanner-v2-07.pdf}}

@inproceedings{sortMonotonicity,
	Acmid = {2032283},
	Address = {Berlin, Heidelberg},
	Author = {Koen Claessen and Ann Lilliestr{\"o}m and Nicholas Smallbone},
	Booktitle = {Proceedings of the 23rd international conference on Automated deduction},
	Isbn = {978-3-642-22437-9},
	Location = {Wroc\&\#322;aw, Poland},
	Numpages = {15},
	Pages = {207--221},
	Publisher = {Springer-Verlag},
	Series = {CADE'11},
	Title = {Sort it out with monotonicity: translating between many-sorted and unsorted first-order logic},
	Url = {http://dl.acm.org/citation.cfm?id=2032266.2032283},
	Year = {2011},
	Bdsk-Url-1 = {http://dl.acm.org/citation.cfm?id=2032266.2032283}}

@inproceedings{polyMonotonicity,
	Author = {Jasmin Christian Blanchette and Sascha B{\"o}hme and Nicholas Smallbone},
	Title = {Monotonicity or how to encode polymorphic types safely and efficiently},
	Year = {2011}}

@inproceedings{isaplanner,
	Author = {Dixon, Lucas and Fleuriot, Jacques D.},
	Booktitle = {Proceedings of TPHOLs},
	Pages = {83--98},
	Series = {LNCS},
	Title = {Higher Order Rippling in {IsaPlanner}},
	Volume = {3223},
	Year = {2004}}

@article{isacosy,
	Author = {Johansson, Moa and Dixon, Lucas and Bundy, Alan},
	Journal = {Journal of Automated Reasoning},
	Number = {3},
	Pages = {251-289},
	Title = {Conjecture Synthesis for Inductive Theories},
	Volume = {47},
	Year = {2011}}

@inproceedings{quickcheck,
	Author = {Koen Claessen and John Hughes},
	Bibsource = {DBLP, http://dblp.uni-trier.de},
	Booktitle = {Proceedings of ICFP},
	Ee = {http://doi.acm.org/10.1145/351240.351266},
	Pages = {268-279},
	Title = {Quick{C}heck: a lightweight tool for random testing of {H}askell programs},
	Year = {2000}}

@inproceedings{quickspec,
	Author = {Koen Claessen and Nicholas Smallbone and John Hughes},
	Bibsource = {DBLP, http://dblp.uni-trier.de},
	Booktitle = {Proceedings of TAP},
	Ee = {http://dx.doi.org/10.1007/978-3-642-13977-2_3},
	Pages = {6-21},
	Title = {Quick{S}pec: Guessing Formal Specifications Using Testing},
	Year = {2010}}

@misc{schulzE,
	Author = {Stephan Schulz},
	Title = {E - A Brainiac Theorem Prover},
	Year = {2002}}

@book{rippling,
	Author = {Bundy, Alan and Basin, David and Hutter, Dieter and Ireland, Andrew},
	Publisher = {Cambridge University Press},
	Title = {Rippling: meta-level guidance for mathematical reasoning},
	Year = {2005}}

@inproceedings{IsaPcase,
	Author = {Johansson, Moa and Dixon, Lucas and Bundy, Alan},
	Booktitle = {Proceedings of ITP},
	Pages = {291--306},
	Title = {Case-Analysis for rippling and inductive proof},
	Year = {2010}}

@inproceedings{acl2s,
	Author = {Chamarthi, Harsh Raju and Dillinger, Peter and Manolios, Panagiotis and Vroon, Daron},
	Booktitle = {Proceedings of TACAS},
	Pages = {291--295},
	Title = {The {ACL2 Sedan} theorem proving system},
	Year = {2011}}

@incollection{middleout,
	Author = {Johansson, Moa and Dixon, Lucas and Bundy, Alan},
	Booktitle = {Induction, Verification and Termination Analysis: Festschrift for Christoph Walther},
	Editor = {S. Siegler and N. Wasser},
	Pages = {102--116},
	Publisher = {Springer},
	Series = {LNAI},
	Title = {Lemma Discovery and Middle-Out Reasoning for Automated Inductive Proof},
	Volume = {6463}}

@incollection{mathsaid,
	Author = {McCasland, Roy and Bundy, Alan and Autexier, Serge},
	Booktitle = {From Insight to Proof: Festschrift in Honor of A. Trybulec},
	Editor = {R. Matuszewski and P. Rudnicki},
	Title = {Automated discovery of inductive theorems},
	Year = {2007}}

@article{McCasland2006,
	Author = {Roy L. McCasland and Alan Bundy and Patrick F. Smith},
	Journal = {Electronic Notes in Theoretical Computer Science},
	Number = {1},
	Pages = {21 - 38},
	Title = {Ascertaining Mathematical Theorems},
	Volume = {151},
	Year = {2006}}

@inproceedings{z3,
	Author = {De Moura, Leonardo and Bj{\o}rner, Nikolaj},
	Booktitle = {Proceedings of TACAS},
	Pages = {337--340},
	Publisher = {Springer-Verlag},
	Series = {TACAS'08/ETAPS'08},
	Title = {Z3: an efficient {SMT} solver},
	Year = {2008}}

@inproceedings{acl2ml,
	Author = {Heras, Jonathan and Komendantskaya, Ekaterina and Johansson, Moa and Maclean, Ewen},
	Booktitle = {Proceedings of LPAR},
	Pages = {389-406},
	Publisher = {Springer-Verlag},
	Series = {LNCS},
	Title = {Proof-Pattern Recognition and Lemma Discovery in {ACL2}},
	Volume = {8312},
	Year = {2013}}

@inproceedings{BST10,
   author = {Clark Barrett and Aaron Stump and Cesare Tinelli},
   title = {The {SMT-LIB} Standard -- Version 2.0},
   booktitle = {Proceedings of the 8th International Workshop on
	Satisfiability Modulo Theories (SMT '10)},
   month = jul,
   year = {2010},
   note = {Edinburgh, Scotland},
   url = {http://www.cs.nyu.edu/~barrett/pubs/BST10.pdf}
}

@misc{smtlib25,
   author = {Clark Barrett and Aaron Stump and Cesare Tinelli},
   title = {The {SMT-LIB} Standard -- Version 2.5 (draft)},
   Howpublished = {\url{http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.5-draft.pdf}},
}


@misc{cvc4parPR,
   author = {Fran\c{c}ois Bobot},
   title = {[{RFC}] {A}dd adhoc polymorphism},
   Howpublished = {\url{https://github.com/CVC4/CVC4/pull/51}}
}

@inproceedings{smtlam,
    title = {Extending {SMT-LIB} v2 with $\lambda$-Terms and Polymorphism},
    author = {Richard Bonichon and David D\'{e}harbe and Cl\'{a}udia Tavares},
    pages = {53--62},
    url = {http://ceur-ws.org/Vol-1163#paper-08},
    crossref = {SMT2014},
}



@proceedings{SMT2014,
booktitle = {12th International Workshop on Satisfiability Modulo Theories (SMT)},
title = {Proceedings of the 12th International Workshop on Satisfiability Modulo Theories (SMT)},
year = 2014,
editor = {Philipp R\"{u}mmer and Christoph M. Wintersteiger},
number = 1163,
series = {CEUR Workshop Proceedings},
address = {Aachen},
issn = {1613-0073},
url = {http://ceur-ws.org/Vol-1163},
venue = {Vienna, Austria},
eventdate = {2014-07-17},
}

@misc{tiplang,
   author = {Koen Claessen and Moa Johansson and Dan Ros\'en and Nick Smallbone},
   title = {The {TIP} language},
   Howpublished = {\url{http://tip-org.github.io/format.html}}
   }

@inproceedings{defunc,
 author = {Reynolds, John C.},
 title = {Definitional Interpreters for Higher-order Programming Languages},
 booktitle = {Proceedings of the ACM Annual Conference - Volume 2},
 series = {ACM '72},
 year = {1972},
 location = {Boston, Massachusetts, USA},
 pages = {717--740},
 numpages = {24},
 url = {http://doi.acm.org/10.1145/800194.805852},
 doi = {10.1145/800194.805852},
 acmid = {805852},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {Applicative language, Closure, Continuation, GEDANKEN, Higher-order function, Interpreter, J-operator, LISP, Lambda calculus, Language definition, Order of application, PAL, Programming language, Reference, SECD machine},
}