default search action

combined dblp search
author search
venue search
publication search

ask others

1. ITP 2010: Edinburgh, UK

Name: dblp XML data dump
Creator: Schloss Dagstuhl - Leibniz Center for Informatics
Published: 1993
License: https://creativecommons.org/publicdomain/zero/1.0/
Keywords: dblp, XML, computer science, scholarly publications, metadata

> Home > Conferences and Workshops > ITP

- view
  authority control:
- export record
  dblp key:
  - conf/itp/2010
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/2010
Matt Kaufmann, Lawrence C. Paulson:
Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings. Lecture Notes in Computer Science 6172, Springer 2010, ISBN 978-3-642-14051-8

Invited Talks

- view
- export record
  dblp key:
  - conf/itp/Klein10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Klein10
Gerwin Klein:
A Formally Verified OS Kernel. Now What? 1-7
- view
- export record
  dblp key:
  - conf/itp/Pierce10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Pierce10
Benjamin C. Pierce:
Proof Assistants as Teaching Assistants: A View from the Trenches. 8

Proof Pearls

- view
- export record
  dblp key:
  - conf/itp/CacheraP10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/CacheraP10
David Cachera, David Pichardie:
A Certified Denotational Abstract Interpreter. 9-24
- view
- export record
  dblp key:
  - conf/itp/CowlesG10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/CowlesG10
John R. Cowles, Ruben Gamboa:
Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure. 25-34
- view
- export record
  dblp key:
  - conf/itp/HuffmanU10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/HuffmanU10
Brian Huffman, Christian Urban:
A New Foundation for Nominal Isabelle. 35-50
- view
- export record
  dblp key:
  - conf/itp/KumarN10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/KumarN10
Ramana Kumar, Michael Norrish:
(Nominal) Unification by Recursive Descent with Triangular Substitutions. 51-66
- view
- export record
  dblp key:
  - conf/itp/VerbeekS10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/VerbeekS10
Freek Verbeek, Julien Schmaltz:
A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks. 67-82

Regular Papers

- view
- export record
  dblp key:
  - conf/itp/ArmandGST10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/ArmandGST10
Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, Laurent Théry:
Extending Coq with Imperative Features and Its Application to SAT Verification. 83-98
- view
- export record
  dblp key:
  - conf/itp/AutexierD10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/AutexierD10
Serge Autexier, Dominik Dietrich:
A Tactic Language for Declarative Proofs. 99-114
- view
- export record
  dblp key:
  - conf/itp/BartheGB10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/BartheGB10
Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin:
Programming Language Techniques for Cryptographic Proofs. 115-130
- view
- export record
  dblp key:
  - conf/itp/BlanchetteN10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/BlanchetteN10
Jasmin Christian Blanchette, Tobias Nipkow:
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. 131-146
- view
- export record
  dblp key:
  - conf/itp/BoldoCFMMW10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/BoldoCFMMW10
Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis:
Formal Proof of a Wave Equation Resolution Scheme: The Method Error. 147-162
- view
- export record
  dblp key:
  - conf/itp/BraibantP10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/BraibantP10
Thomas Braibant, Damien Pous:
An Efficient Coq Tactic for Deciding Kleene Algebras. 163-178
- view
- export record
  dblp key:
  - conf/itp/BohmeW10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/BohmeW10
Sascha Böhme, Tjark Weber:
Fast LCF-Style Proof Reconstruction for Z3. 179-194
- view
- export record
  dblp key:
  - conf/itp/Chargueraud10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Chargueraud10
Arthur Charguéraud:
The Optimal Fixed Point Combinator. 195-210
- view
- export record
  dblp key:
  - conf/itp/DufourdB10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/DufourdB10
Jean-François Dufourd, Yves Bertot:
Formal Study of Plane Delaunay Triangulation. 211-226
- view
- export record
  dblp key:
  - conf/itp/FeltyP10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/FeltyP10
Amy P. Felty, Brigitte Pientka:
Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison. 227-242
- view
- export record
  dblp key:
  - conf/itp/FoxM10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/FoxM10
Anthony C. J. Fox, Magnus O. Myreen:
A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture. 243-258
- view
- export record
  dblp key:
  - conf/itp/GeuversKSW10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/GeuversKSW10
Herman Geuvers, Adam Koprowski, Dan Synek, Eelis van der Weegen:
Automated Machine-Checked Hybrid System Safety Proofs. 259-274
- view
- export record
  dblp key:
  - conf/itp/HendrixKM10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/HendrixKM10
Joe Hendrix, Deepak Kapur, José Meseguer:
Coverset Induction with Partiality and Subsorts: A Powerlist Case Study. 275-290
- view
- export record
  dblp key:
  - conf/itp/JohanssonDB10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/JohanssonDB10
Moa Johansson, Lucas Dixon, Alan Bundy:
Case-Analysis for Rippling and Inductive Proof. 291-306
- view
- export record
  dblp key:
  - conf/itp/KellerW10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/KellerW10
Chantal Keller, Benjamin Werner:
Importing HOL Light into Coq. 307-322
- view
- export record
  dblp key:
  - conf/itp/KraussS10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/KraussS10
Alexander Krauss, Andreas Schropp:
A Mechanized Translation from Higher-Order Logic to Set Theory. 323-338
- view
- export record
  dblp key:
  - conf/itp/LammichL10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/LammichL10
Peter Lammich, Andreas Lochbihler:
The Isabelle Collections Framework. 339-354
- view
- export record
  dblp key:
  - conf/itp/ManoliosV10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/ManoliosV10
Panagiotis Manolios, Daron Vroon:
Interactive Termination Proofs Using Termination Cores. 355-370
- view
- export record
  dblp key:
  - conf/itp/ManskyG10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/ManskyG10
William Mansky, Elsa L. Gunter:
A Framework for Formal Verification of Compiler Optimizations. 371-386
- view
- export record
  dblp key:
  - conf/itp/MhamdiHT10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/MhamdiHT10
Tarek Mhamdi, Osman Hasan, Sofiène Tahar:
On the Formalization of the Lebesgue Integration Theory in HOL. 387-402
- view
- export record
  dblp key:
  - conf/itp/CohenS10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/CohenS10
Ernie Cohen, Bert Schirmer:
From Total Store Order to Sequential Consistency: A Practical Reduction Theorem. 403-418
- view
- export record
  dblp key:
  - conf/itp/Sozeau10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Sozeau10
Matthieu Sozeau:
Equations: A Dependent Pattern-Matching Compiler. 419-434
- view
- export record
  dblp key:
  - conf/itp/SwordsH10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/SwordsH10
Sol Swords, Warren A. Hunt Jr.:
A Mechanically Verified AIG-to-BDD Conversion Algorithm. 435-449
- view
- export record
  dblp key:
  - conf/itp/Walukiewicz-ChrzaszczC10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Walukiewicz-ChrzaszczC10
Daria Walukiewicz-Chrzaszcz, Jacek Chrzaszcz:
Inductive Consequences in the Calculus of Constructions. 450-465
- view
- export record
  dblp key:
  - conf/itp/Weber10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Weber10
Tjark Weber:
Validating QBF Invalidity in HOL4. 466-480

Rough Diamonds

- view
- export record
  dblp key:
  - conf/itp/Howe10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Howe10
Douglas J. Howe:
Higher-Order Abstract Syntax in Isabelle/HOL. 481-484
- view
- export record
  dblp key:
  - conf/itp/Myreen10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/Myreen10
Magnus O. Myreen:
Separation Logic Adapted for Proofs by Rewriting. 485-489
- view
- export record
  dblp key:
  - conf/itp/SpittersW10
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/itp/SpittersW10
Bas Spitters, Eelis van der Weegen:
Developing the Algebraic Hierarchy with Type Classes in Coq. 490-493

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.