Search dblp for Publications

export results for "toc:db/conf/itp/itp2010.bht:"

 download as .bib file

@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}
}
a service of  Schloss Dagstuhl - Leibniz Center for Informatics

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.