@article(Armando:2002yd, author = "A. Armando and M. Rusinowitch and S. Stratulat", year = "2002", title = "Incorporating Decision Procedures in Implicit Induction", journal = "J. Symb. Comput.", volume = "34", number = "4", pages = "241--258", doi = "10.1006/jsco.2002.0549", ) @inproceedings(Barthe:2003hv, author = "G. Barthe and S. Stratulat", year = "2003", title = "Validation of the {J}ava{C}ard Platform with Implicit Induction Techniques", editor = "R. Nieuwenhuis", booktitle = "RTA", series = "Lecture Notes in Computer Science", volume = "2706", publisher = "Springer", pages = "337--351", doi = "10.1007/3-540-44881-0\kern .08em\vbox {\hrule width.35em height.6pt}\kern .08em24", ) @article(Bouhoula:1995wl, author = "A. Bouhoula and E. Kounalis and M. Rusinowitch", year = "1995", title = "Automated Mathematical Induction", journal = "Journal of Logic and Computation", volume = "5", number = "5", pages = "631--668", doi = "10.1093/logcom/5.5.631", ) @incollection(Boulton:2000zr, author = "R. Boulton and K. Slind", year = "2000", title = "Automatic Derivation and Application of Induction Schemes for Mutually Recursive Functions", editor = "J. Lloyd and V. Dahl and U. Furbach and M. Kerber and K.-K. Lau and C. Palamidessi and L. Pereira and Y. Sagiv and P. Stuckey", booktitle = "Computational Logic --- CL 2000", series = "Lecture Notes in Computer Science", volume = "1861", publisher = "Springer Berlin / Heidelberg", pages = "629--643", doi = "10.1007/3-540-44957-4\kern .08em\vbox {\hrule width.35em height.6pt}\kern .08em42", ) @book(Boyer:1988ve, author = "R. S. Boyer and J S. Moore", year = "1988", title = "A computational logic handbook", publisher = "Academic Press Professional", ) @inproceedings(Boyer:1988hb, author = "R. S. Boyer and J S. Moore", year = "1988", title = "{Integrating decision procedures into heuristic theorem provers: a case study of linear arithmetic}", booktitle = "{Machine Intelligence}", publisher = "Oxford University Press, Inc. New York, NY, USA", pages = "83--124", ) @article(Burstall:1969pj, author = "R. M. Burstall", year = "1969", title = "{Proving properties of programs by structural induction}", journal = "The Computer Journal", volume = "12", pages = "41--48", doi = "10.1093/comjnl/12.1.41", ) @article(Contejean:2007kb, author = "E. Contejean and P. Courtieu and J. Forest and O. Pons and X. Urbain", year = "2007", title = "Certification of Automated Termination Proofs", journal = "Frontiers of Combining Systems", pages = "148--162", doi = "10.1007/978-3-540-74621-8\kern .08em\vbox {\hrule width.35em height.6pt}\kern .08em10", ) @techreport(Courant:1996gd, author = "J. Courant", year = "1996", title = "Proof reconstruction", type = "Research Report", number = "RR96-26", institution = "LIP", note = "Preliminary version", ) @inproceedings(Delahaye:2000vn, author = "D. Delahaye", year = "2000", title = "A Tactic Language for the System {C}oq", editor = "M. Parigot and A. Voronkov", booktitle = "Logic for Programming and Automated Reasoning (LPAR)", series = "Lecture Notes in Computer Science (LNCS)", volume = "1955", publisher = "Springer", address = "Reunion Island (France)", pages = "85--95", doi = "10.1007/3-540-44404-1\kern .08em\vbox {\hrule width.35em height.6pt}\kern .08em7", ) @article(Gramlich:2005pf, author = "B. Gramlich", year = "2005", title = "Strategic Issues, Problems and Challenges in Inductive Theorem Proving", journal = "Electronic Notes in Theoretical Computer Science", volume = "125", number = "2", pages = "5--43", doi = "10.1016/j.entcs.2005.01.006", ) @incollection(Kapur:1996qw, author = "D. Kapur and M. Subramaniam", year = "1996", title = "Automating induction over mutually recursive functions", booktitle = "Algebraic Methodology and Software Technology", series = "LNCS", volume = "1101", publisher = "Springer", pages = "117--131", doi = "10.1007/BFb0014311", ) @inproceedings(knuth1970swp, author = "D.E. Knuth and P.B. Bendix", year = "1970", title = "{Simple word problems in universal algebras}", booktitle = "Computational Problems in Abstract Algebra", pages = "263--297", ) @manual(ocaml, author = "X. Leroy and D. Doligez and A. Frisch and J. Garrigue and D. R{\'e}my and J. Vouillon", title = "The {O}bjective {C}aml system - release 3.12. Documentation and user's manual", organization = "INRIA", ) @inproceedings(Musser:1980aq, author = "D. R. Musser", year = "1980", title = "On Proving Inductive Properties of Abstract Data Types", booktitle = "POPL", pages = "154--162", doi = "10.1145/567446.567461", ) @article(Protzen:1994ci, author = "M. Protzen", year = "1994", title = "Lazy generation of induction hypotheses", journal = "Automated Deduction ---CADE-12", pages = "42--56", doi = "10.1007/3-540-58156-1\kern .08em\vbox {\hrule width.35em height.6pt}\kern .08em4", ) @article(Rusinowitch:2003ak, author = "M. Rusinowitch and S. Stratulat and F. Klay", year = "2003", title = "Mechanical Verification of an Ideal Incremental {ABR} Conformance Algorithm", journal = "J. Autom. Reasoning", volume = "30", number = "2", pages = "53--177", doi = "10.1023/A:1023251327012", ) @manual(Shankar:2001zr, author = "N. Shankar and S. Owre and J. M. Rushby and D. W. J. Stringer-Calvert", year = "2001", title = "{PVS} prover guide - version 2.4", organization = "SRI International", ) @article(Stratulat:2001wo, author = "S. Stratulat", year = "2001", title = "A General Framework to Build Contextual Cover Set Induction Provers", journal = "J. Symb. Comput.", volume = "32", number = "4", pages = "403--445", doi = "10.1006/jsco.2000.0469", ) @inproceedings(Stratulat:2010vn, author = "S. Stratulat", year = "2010", title = "Integrating Implicit Induction Proofs into Certified Proof Environments", booktitle = "Integrated Formal Methods", series = "Lecture Notes in Computer Science", volume = "6396", pages = "320--335", doi = "10.1007/978-3-642-16265-7\kern .08em\vbox {\hrule width.35em height.6pt}\kern .08em23", ) @inproceedings(Stratulat:2012uq, author = "S. Stratulat", year = "2012", title = "A Unified View of Induction Reasoning for First-Order Logic", editor = "A. Voronkov", booktitle = "Turing-100 (The Alan Turing Centenary Conference)", series = "EPiC Series", volume = "10", publisher = "EasyChair", pages = "326--352", ) @inproceedings(Stratulat:2011kx, author = "S. Stratulat and V. Demange", year = "2011", title = "Automated Certification of Implicit Induction Proofs", booktitle = "CPP'2011 (First International Conference on Certified Programs and Proofs)", series = "Lecture Notes Computer Science", volume = "7086", publisher = "Springer-Verlag", pages = "37--53", doi = "10.1007/978-3-642-25379-9\kern .08em\vbox {\hrule width.35em height.6pt}\kern .08em5", ) @unpublished(coq, author = "The Coq Development Team", year = "2009", title = "The {C}oq Reference Manual - version 8.2", url = "http://coq.inria.fr/doc", ) @inproceedings(Voicu:2009vn, author = "R. Voicu and M. Li", year = "2009", title = "Descente {I}nfinie Proofs in {C}oq", booktitle = "The 1st Coq Workshop", pages = "12 pages", ) @article(Wirth:2004rb, author = "C.-P. Wirth", year = "2004", title = "Descente Infinie + {D}eduction", journal = "Logic Journal of the IGPL", volume = "12", number = "1", pages = "1--96", doi = "10.1093/jigpal/12.1.1", )