Invited Talks

• 
  Bart Jacobs: JavaCard Program Verification. 1-3
• 
  Steven D. Johnson: View from the Fringe of the Fringe (Joint with CHARME 2001). 4
• 
  Natarajan Shankar: Using Decision Procedures with a Higher-Order Logic. 5-26

Regular Contributions

• 
  Andrew Adams, Martin Dunstan, Hanne Gottliebsen, Tom Kelsey, Ursula Martin, Sam Owre: Computer Algebra Meets Automated Theorem Proving: Integrating Maple and PVS. 27-42
• 
  R. D. Arthan: An Irrational Construction of R from Z. 43-58
• 
  Andrea Asperti, Luca Padovani, Claudio Sacerdoti Coen, Irene Schena: HELM and the Semantic Math-Web. 59-74
• 
  Gertrud Bauer, Markus Wenzel: Calculational Reasoning Revisited (An Isabelle/Isar Experience). 75-90
• 
  Giampaolo Bella, Lawrence C. Paulson: Mechanical Proofs about a Non-repudiation Protocol. 91-104
• 
  Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu: Proving Hybrid Protocols Correct. 105-120
• 
  Ana Bove, Venanzio Capretta: Nested General Recursion and Partiality in Type Theory. 121-135
• 
  Mario Cáccamo, Glynn Winskel: A Higher-Order Calculus for Categories. 136-153
• 
  Venanzio Capretta: Certifying the Fast Fourier Transform with Coq. 154-168
• 
  Marc Daumas, Laurence Rideau, Laurent Théry: A Generic Library for Floating-Point Numbers and Its Application to Exact Computing. 169-184
• 
  Louise A. Dennis, Alan Smaill: Ordinal Arithmetic: A Case Study for Rippling in a Higher Order Domain. 185-200
• 
  Matt Fairtlough, Michael Mendler, Xiaochun Cheng: Abstraction and Refinement in Higher Order Logic. 201-216
• 
  Simon J. Gay: A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL. 217-232
• 
  Steffen Helke, Florian Kammüller: Representing Hierarchical Automata in Interactive Theorem Provers. 233-248
• 
  David Hemer, Ian J. Hayes, Paul A. Strooper: Refinement Calculus for Logic Programming in Isabelle/HOL. 249-264
• 
  Joe Hurd: Predicate Subtyping with Predicate Sets. 265-280
• 
  Pertti Kellomäki: A Structural Embedding of Ocsid in PVS. 281-296
• 
  Inmaculada Medina-Bulo, Francisco Palomo-Lozano, José A. Alonso-Jiménez: A Certified Polynomial-Based Decision Procedure for Propositional Logic. 297-312
• 
  J. Strother Moore: Finite Set Theory in ACL2. 313-328
• 
  Pavel Naumov, Mark-Oliver Stehr, José Meseguer: The HOL/NuPRL Proof Translator (A Practical Approach to Formal Interoperability). 329-345
• 
  David Pichardie, Yves Bertot: Formalizing Convex Hull Algorithms. 346-361
• 
  Xavier Rival, Jean Goubault-Larrecq: Experiments with Finite Tree Automata in Coq. 362-377
• 
  Freek Wiedijk: Mizar Light for HOL Light. 378-394

last updated on Mon May 20 02:41:41 2013 by the dblp team
data released under the ODC-BY 1.0 license
see also our legal information page