Archive of Formal Proofs, Volume 2012

Volume 2012, 2012

• Johannes Hölzl, Tobias Nipkow:
  Markov Models. , (Formal proof development)
  
• Peter Lammich:
  Refinement for Monadic Programs. , (Formal proof development)
  
• Benedikt Nordhoff, Peter Lammich:
  Dijkstra's Shortest Path Algorithm. , (Formal proof development)
  
• Lars Noschinski:
  A Probabilistic Proof of the Girth-Chromatic Number Theorem. , (Formal proof development)
  
• René Thiemann:
  Executable Transitive Closures. , (Formal proof development)
  
• Rachid Guerraoui, Viktor Kuncak, Giuliano Losa:
  Abortable Linearizable Modules. , (Formal proof development)
  
• Christian Sternagel:
  Well-Quasi-Orders.
  
• Fabian Immler, Johannes Hölzl:
  Ordinary Differential Equations.
  
• Giampaolo Bella:
  Inductive Study of Confidentiality.
  
• Stephan Merz:
  Stuttering Equivalence.
  
• Gerwin Klein, Rafal Kolanski, Andrew Boyton:
  Separation Algebra.
  
• Abderrahmane Feliachi, Burkhart Wolff, Marie-Claude Gaudel:
  Isabelle/Circus.
  
• Jesper Bengtson:
  Psi-calculi in Isabelle.
  
• Jesper Bengtson:
  The pi-calculus in nominal logic.
  
• Jesper Bengtson:
  CCS in nominal logic.
  
• Brian Huffman:
  Type Constructor Classes and Monad Transformers.
  
• Peter Gammie:
  Logical Relations for PCF.
  
• Henri Debrat, Stephan Merz:
  Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model.
  
• Ralph Romanos, Lawrence C. Paulson:
  Proving the Impossibility of Trisecting an Angle and Doubling the Cube.
  
• René Thiemann:
  Generating linear orders for datatypes.
  
• Andrei Popescu, Johannes Hölzl:
  Possibilistic Noninterference.
  
• Jeremy Avigad, Stefan Hetzl:
  Bondy's Theorem.
  
• T. J. M. Makarios:
  The independence of Tarski's Euclidean axiom.
  
• Peter Lammich, Rene Meis:
  A Separation Logic Framework for Imperative HOL.
  

Last update Sun May 26 06:16:27 2013 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page