1. ITP 2010: Edinburgh, UK

Invited Talks

• Gerwin Klein:
  A Formally Verified OS Kernel. Now What? 1-7
  
• Benjamin C. Pierce:
  Proof Assistants as Teaching Assistants: A View from the Trenches. 8
  

Proof Pearls

• David Cachera, David Pichardie:
  A Certified Denotational Abstract Interpreter. 9-24
  
• John R. Cowles, Ruben Gamboa:
  Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure. 25-34
  
• Brian Huffman, Christian Urban:
  A New Foundation for Nominal Isabelle. 35-50
  
• Ramana Kumar, Michael Norrish:
  (Nominal) Unification by Recursive Descent with Triangular Substitutions. 51-66
  
• Freek Verbeek, Julien Schmaltz:
  A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks. 67-82
  

Regular Papers

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

Rough Diamonds

• Douglas J. Howe:
  Higher-Order Abstract Syntax in Isabelle/HOL. 481-484
  
• Magnus O. Myreen:
  Separation Logic Adapted for Proofs by Rewriting. 485-489
  
• Bas Spitters, Eelis van der Weegen:
  Developing the Algebraic Hierarchy with Type Classes in Coq. 490-493
  

Last update Fri May 25 08:24:34 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page