


default search action
Archive of Formal Proofs, Volume 2012
Volume 2012, 2012
- Johannes Hölzl, Tobias Nipkow:
Markov Models. - Peter Lammich:
Refinement for Monadic Programs. - Benedikt Nordhoff, Peter Lammich:
Dijkstra's Shortest Path Algorithm. - Lars Noschinski:
A Probabilistic Proof of the Girth-Chromatic Number Theorem. - René Thiemann:
Executable Transitive Closures. - Rachid Guerraoui, Viktor Kuncak, Giuliano Losa:
Abortable Linearizable Modules. - 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.

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.