Stop the war!
Остановите войну!
for scientists:
default search action
Search dblp for Publications
export results for "toc:db/conf/itp/itp2010.bht:"
@inproceedings{DBLP:conf/itp/ArmandGST10, author = {Micha{\"{e}}l Armand and Benjamin Gr{\'{e}}goire and Arnaud Spiwack and Laurent Th{\'{e}}ry}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {Extending Coq with Imperative Features and Its Application to {SAT} Verification}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {83--98}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_8}, doi = {10.1007/978-3-642-14052-5\_8}, timestamp = {Tue, 14 May 2019 10:00:37 +0200}, biburl = {https://dblp.org/rec/conf/itp/ArmandGST10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/AutexierD10, author = {Serge Autexier and Dominik Dietrich}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {A Tactic Language for Declarative Proofs}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {99--114}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_9}, doi = {10.1007/978-3-642-14052-5\_9}, timestamp = {Sat, 09 Apr 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/AutexierD10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/BartheGB10, author = {Gilles Barthe and Benjamin Gr{\'{e}}goire and Santiago Zanella B{\'{e}}guelin}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {Programming Language Techniques for Cryptographic Proofs}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {115--130}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_10}, doi = {10.1007/978-3-642-14052-5\_10}, timestamp = {Sun, 25 Oct 2020 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/BartheGB10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/BlanchetteN10, author = {Jasmin Christian Blanchette and Tobias Nipkow}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {Nitpick: {A} Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {131--146}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_11}, doi = {10.1007/978-3-642-14052-5\_11}, timestamp = {Wed, 25 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/BlanchetteN10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/BohmeW10, author = {Sascha B{\"{o}}hme and Tjark Weber}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {Fast LCF-Style Proof Reconstruction for {Z3}}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {179--194}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_14}, doi = {10.1007/978-3-642-14052-5\_14}, timestamp = {Sun, 21 May 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/BohmeW10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/BoldoCFMMW10, author = {Sylvie Boldo and Fran{\c{c}}ois Cl{\'{e}}ment and Jean{-}Christophe Filli{\^{a}}tre and Micaela Mayero and Guillaume Melquiond and Pierre Weis}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {Formal Proof of a Wave Equation Resolution Scheme: The Method Error}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {147--162}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_12}, doi = {10.1007/978-3-642-14052-5\_12}, timestamp = {Sat, 19 Oct 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/BoldoCFMMW10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/BraibantP10, author = {Thomas Braibant and Damien Pous}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {An Efficient Coq Tactic for Deciding Kleene Algebras}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {163--178}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_13}, doi = {10.1007/978-3-642-14052-5\_13}, timestamp = {Thu, 15 Jun 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/BraibantP10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/CacheraP10, author = {David Cachera and David Pichardie}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {A Certified Denotational Abstract Interpreter}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {9--24}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_3}, doi = {10.1007/978-3-642-14052-5\_3}, timestamp = {Sun, 21 May 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/CacheraP10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/Chargueraud10, author = {Arthur Chargu{\'{e}}raud}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {The Optimal Fixed Point Combinator}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {195--210}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_15}, doi = {10.1007/978-3-642-14052-5\_15}, timestamp = {Sun, 21 May 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/Chargueraud10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/CohenS10, author = {Ernie Cohen and Bert Schirmer}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {From Total Store Order to Sequential Consistency: {A} Practical Reduction Theorem}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {403--418}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_28}, doi = {10.1007/978-3-642-14052-5\_28}, timestamp = {Sun, 21 May 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/CohenS10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/CowlesG10, author = {John R. Cowles and Ruben Gamboa}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {25--34}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_4}, doi = {10.1007/978-3-642-14052-5\_4}, timestamp = {Sun, 21 May 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/CowlesG10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/DufourdB10, author = {Jean{-}Fran{\c{c}}ois Dufourd and Yves Bertot}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {Formal Study of Plane Delaunay Triangulation}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {211--226}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_16}, doi = {10.1007/978-3-642-14052-5\_16}, timestamp = {Sun, 21 May 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/DufourdB10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/FeltyP10, author = {Amy P. Felty and Brigitte Pientka}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {Reasoning with Higher-Order Abstract Syntax and Contexts: {A} Comparison}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {227--242}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_17}, doi = {10.1007/978-3-642-14052-5\_17}, timestamp = {Sun, 21 May 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/FeltyP10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/FoxM10, author = {Anthony C. J. Fox and Magnus O. Myreen}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {243--258}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_18}, doi = {10.1007/978-3-642-14052-5\_18}, timestamp = {Sun, 21 May 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/FoxM10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/GeuversKSW10, author = {Herman Geuvers and Adam Koprowski and Dan Synek and Eelis van der Weegen}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {Automated Machine-Checked Hybrid System Safety Proofs}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {259--274}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_19}, doi = {10.1007/978-3-642-14052-5\_19}, timestamp = {Sun, 21 May 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/GeuversKSW10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/HendrixKM10, author = {Joe Hendrix and Deepak Kapur and Jos{\'{e}} Meseguer}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {Coverset Induction with Partiality and Subsorts: {A} Powerlist Case Study}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {275--290}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_20}, doi = {10.1007/978-3-642-14052-5\_20}, timestamp = {Wed, 20 Sep 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/HendrixKM10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/Howe10, author = {Douglas J. Howe}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {Higher-Order Abstract Syntax in Isabelle/HOL}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {481--484}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_33}, doi = {10.1007/978-3-642-14052-5\_33}, timestamp = {Sun, 21 May 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/Howe10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/HuffmanU10, author = {Brian Huffman and Christian Urban}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {A New Foundation for Nominal Isabelle}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {35--50}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_5}, doi = {10.1007/978-3-642-14052-5\_5}, timestamp = {Sun, 21 May 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/HuffmanU10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/JohanssonDB10, author = {Moa Johansson and Lucas Dixon and Alan Bundy}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {Case-Analysis for Rippling and Inductive Proof}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {291--306}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_21}, doi = {10.1007/978-3-642-14052-5\_21}, timestamp = {Sun, 21 May 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/JohanssonDB10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/KellerW10, author = {Chantal Keller and Benjamin Werner}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {Importing {HOL} Light into Coq}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {307--322}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_22}, doi = {10.1007/978-3-642-14052-5\_22}, timestamp = {Sun, 21 May 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/KellerW10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/Klein10, author = {Gerwin Klein}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {A Formally Verified {OS} Kernel. Now What?}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {1--7}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_1}, doi = {10.1007/978-3-642-14052-5\_1}, timestamp = {Fri, 02 Nov 2018 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/itp/Klein10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/KraussS10, author = {Alexander Krauss and Andreas Schropp}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {A Mechanized Translation from Higher-Order Logic to Set Theory}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {323--338}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_23}, doi = {10.1007/978-3-642-14052-5\_23}, timestamp = {Mon, 26 Feb 2024 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/itp/KraussS10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/KumarN10, author = {Ramana Kumar and Michael Norrish}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {(Nominal) Unification by Recursive Descent with Triangular Substitutions}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {51--66}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_6}, doi = {10.1007/978-3-642-14052-5\_6}, timestamp = {Sun, 21 May 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/KumarN10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/LammichL10, author = {Peter Lammich and Andreas Lochbihler}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {The Isabelle Collections Framework}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {339--354}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_24}, doi = {10.1007/978-3-642-14052-5\_24}, timestamp = {Sat, 16 Sep 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/LammichL10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/ManoliosV10, author = {Panagiotis Manolios and Daron Vroon}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {Interactive Termination Proofs Using Termination Cores}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {355--370}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_25}, doi = {10.1007/978-3-642-14052-5\_25}, timestamp = {Tue, 21 Mar 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/itp/ManoliosV10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/ManskyG10, author = {William Mansky and Elsa L. Gunter}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {A Framework for Formal Verification of Compiler Optimizations}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {371--386}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_26}, doi = {10.1007/978-3-642-14052-5\_26}, timestamp = {Sun, 21 May 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/ManskyG10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/MhamdiHT10, author = {Tarek Mhamdi and Osman Hasan and Sofi{\`{e}}ne Tahar}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {On the Formalization of the Lebesgue Integration Theory in {HOL}}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {387--402}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_27}, doi = {10.1007/978-3-642-14052-5\_27}, timestamp = {Fri, 09 Apr 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/MhamdiHT10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/Myreen10, author = {Magnus O. Myreen}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {Separation Logic Adapted for Proofs by Rewriting}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {485--489}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_34}, doi = {10.1007/978-3-642-14052-5\_34}, timestamp = {Sun, 21 May 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/Myreen10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/Pierce10, author = {Benjamin C. Pierce}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {Proof Assistants as Teaching Assistants: {A} View from the Trenches}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {8}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_2}, doi = {10.1007/978-3-642-14052-5\_2}, timestamp = {Sun, 21 May 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/Pierce10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/Sozeau10, author = {Matthieu Sozeau}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {Equations: {A} Dependent Pattern-Matching Compiler}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {419--434}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_29}, doi = {10.1007/978-3-642-14052-5\_29}, timestamp = {Sun, 21 May 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/Sozeau10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/SpittersW10, author = {Bas Spitters and Eelis van der Weegen}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {Developing the Algebraic Hierarchy with Type Classes in Coq}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {490--493}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_35}, doi = {10.1007/978-3-642-14052-5\_35}, timestamp = {Thu, 15 Jun 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/SpittersW10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/SwordsH10, author = {Sol Swords and Warren A. Hunt Jr.}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {A Mechanically Verified AIG-to-BDD Conversion Algorithm}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {435--449}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_30}, doi = {10.1007/978-3-642-14052-5\_30}, timestamp = {Sun, 02 Oct 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/SwordsH10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/VerbeekS10, author = {Freek Verbeek and Julien Schmaltz}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {67--82}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_7}, doi = {10.1007/978-3-642-14052-5\_7}, timestamp = {Sun, 21 May 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/VerbeekS10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/Walukiewicz-ChrzaszczC10, author = {Daria Walukiewicz{-}Chrzaszcz and Jacek Chrzaszcz}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {Inductive Consequences in the Calculus of Constructions}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {450--465}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_31}, doi = {10.1007/978-3-642-14052-5\_31}, timestamp = {Sun, 21 May 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/Walukiewicz-ChrzaszczC10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/itp/Weber10, author = {Tjark Weber}, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {Validating {QBF} Invalidity in {HOL4}}, booktitle = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, pages = {466--480}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5\_32}, doi = {10.1007/978-3-642-14052-5\_32}, timestamp = {Sun, 21 May 2017 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/Weber10.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/itp/2010, editor = {Matt Kaufmann and Lawrence C. Paulson}, title = {Interactive Theorem Proving, First International Conference, {ITP} 2010, Edinburgh, UK, July 11-14, 2010. Proceedings}, series = {Lecture Notes in Computer Science}, volume = {6172}, publisher = {Springer}, year = {2010}, url = {https://doi.org/10.1007/978-3-642-14052-5}, doi = {10.1007/978-3-642-14052-5}, isbn = {978-3-642-14051-8}, timestamp = {Tue, 14 May 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/conf/itp/2010.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.