


default search action
Archive of Formal Proofs, Volume 2015
Volume 2015, 2015
- Johannes Hölzl:

Verification of the UpDown Scheme. - Lawrence C. Paulson:

Finite Automata in Hereditarily Finite Set Theory. - Jose Divasón, Jesús Aransay:

QR Decomposition. - Jose Divasón, Jesús Aransay:

Echelon Form. - Joachim Breitner:

The Safety of Call Arity. - Ognjen Maric, Christoph Sprenger

:
Consensus Refined. - Andreas Lochbihler, Tobias Nipkow:

Trie. - Peter Gammie:

Concurrent IMP. - Peter Gammie, Tony Hosking, Kai Engelhardt:

Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO. - Victor B. F. Gomes, Georg Struth:

Residuated Lattices. - Marco B. Caminati, Manfred Kerber, Christoph Lange, Colin Rowat:

VCG - Combinatorial Vickrey-Clarke-Groves Auctions. - Christian Sternagel, René Thiemann:

Deriving class instances for datatypes. - Johannes Hölzl, Andreas Lochbihler, Dmitriy Traytel:

A Zoo of Probabilistic Systems. - Dmitriy Traytel:

Derivatives of Logical Formulas. - Tobias Nipkow:

Parameterized Dynamic Tables. - Pasquale Noce:

Reasoning about Lists via List Interleaving. - Pasquale Noce:

The Ipurge Unwinding Theorem for CSP Noninterference Security. - Pasquale Noce:

The Generic Unwinding Theorem for CSP Noninterference Security. - Hitoshi Furusawa, Georg Struth:

Binary Multirelations. - Lukas Bulwahn:

Derangements Formula. - Jose Divasón, Jesús Aransay:

Hermite Normal Form. - Manuel Eberl:

The Akra-Bazzi theorem and the Master theorem. - Manuel Eberl:

Landau Symbols. - Lars Noschinski:

Generating Cases from Labeled Subgoals. - Kirstin Peters, Rob J. van Glabbeek:

Analysing and Comparing Encodability Criteria for Process Calculi. - Jeremy Sylvestre:

Representations of Finite Groups. - Pasquale Noce:

The Inductive Unwinding Theorem for CSP Noninterference Security. - Bertram Felgenhauer:

Decreasing Diagrams II. - René Thiemann, Akihisa Yamada:

Matrices, Jordan Normal Forms, and Spectral Radius Theory. - Salomon Sickert:

Converting Linear Temporal Logic to Deterministic (Generalised) Rabin Automata. - Frédéric Tuong, Burkhart Wolff:

A Meta-Model for the Isabelle API. - Christoph Dittmann:

Positional Determinacy of Parity Games. - Lukas Bulwahn:

Euler's Partition Theorem. - Alexander Bentkamp:

Latin Square. - Lukas Bulwahn:

Cardinality of Set Partitions. - René Thiemann, Akihisa Yamada:

Algebraic Numbers in Isabelle/HOL. - Peter Gammie, Andreas Lochbihler:

The Stern-Brocot Tree. - Andreas Lochbihler, Joshua Schneider:

Applicative Lifting. - Manuel Eberl:

Descartes' Rule of Signs. - Manuel Eberl:

The Divergence of the Prime Harmonic Series. - Manuel Eberl:

Basic Geometric Properties of Triangles. - Manuel Eberl:

Liouville numbers.

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.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














