|
|
Archive of
Formal
Proofs
The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments,
mechanically checked in the theorem prover Isabelle. It is organized in the way
of a scientific journal, is indexed by dblp and has an ISSN:
2150-914x. Submissions are refereed. The preferred citation style is available [here]. We encourage companion AFP submissions to conference and journal publications.
This is the development version of the archive, referring to a recent
Isabelle development version. Some entries may not be in a working state, see
the status page for more information.
The main archive is available from the front page.
|
| 2018 |
2018-12-26: A Formal Model of the Document Object Model
Authors:
Achim D. Brucker
and Michael Herzberg
|
2018-12-25: Formalization of Concurrent Revisions
Author:
Roy Overbeek
|
2018-12-21: Verifying Imperative Programs using Auto2
Author:
Bohua Zhan
|
2018-12-17: Constructive Cryptography in HOL
Authors:
Andreas Lochbihler
and S. Reza Sefidgar
|
2018-12-11: Transformer Semantics
Author:
Georg Struth
|
2018-12-11: Quantales
Author:
Georg Struth
|
2018-12-11: Properties of Orderings and Lattices
Author:
Georg Struth
|
2018-11-23: Graph Saturation
Author:
Sebastiaan J. C. Joosten
|
2018-11-23: A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover
Authors:
Anders Schlichtkrull,
Jasmin Christian Blanchette
and Dmitriy Traytel
|
2018-11-20: Auto2 Prover
Author:
Bohua Zhan
|
2018-11-16: Matroids
Author:
Jonas Keinholz
|
2018-11-06: Deriving generic class instances for datatypes
Authors:
Jonas Rädle
and Lars Hupel
|
2018-10-30: Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL
Authors:
David Fuenmayor
and Christoph Benzmüller
|
2018-10-29: Epistemic Logic
Author:
Andreas Halkjær From
|
2018-10-22: Smooth Manifolds
Authors:
Fabian Immler
and Bohua Zhan
|
2018-10-19: Randomised Binary Search Trees
Author:
Manuel Eberl
|
2018-10-19: Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms
Author:
Alexander Bentkamp
|
2018-10-12: Upper Bounding Diameters of State Spaces of Factored Transition Systems
Authors:
Friedrich Kurz
and Mohammad Abdulaziz
|
2018-09-28: The Transcendence of π
Author:
Manuel Eberl
|
2018-09-25: Symmetric Polynomials
Author:
Manuel Eberl
|
2018-09-20: Signature-Based Gröbner Basis Algorithms
Author:
Alexander Maletzky
|
2018-09-19: The Prime Number Theorem
Authors:
Manuel Eberl
and Lawrence C. Paulson
|
2018-09-15: Aggregation Algebras
Author:
Walter Guttmann
|
2018-09-14: Octonions
Author:
Angeliki Koutsoukou-Argyraki
|
2018-09-05: Quaternions
Author:
Lawrence C. Paulson
|
2018-09-02: The Budan-Fourier Theorem and Counting Real Roots with Multiplicity
Author:
Wenda Li
|
2018-08-24: An Incremental Simplex Algorithm with Unsatisfiable Core Generation
Authors:
Filip Marić,
Mirko Spasić
and René Thiemann
|
2018-08-14: Minsky Machines
Author:
Bertram Felgenhauer
|
2018-07-16: Pricing in discrete financial models
Author:
Mnacho Echenim
|
2018-07-04: Von-Neumann-Morgenstern Utility Theorem
Authors:
Julian Parsert
and Cezary Kaliszyk
|
2018-06-23: Pell's Equation
Author:
Manuel Eberl
|
2018-06-14: Projective Geometry
Author:
Anthony Bordg
|
2018-06-14: The Localization of a Commutative Ring
Author:
Anthony Bordg
|
2018-06-05: Partial Order Reduction
Author:
Julian Brunner
|
2018-05-27: Optimal Binary Search Trees
Authors:
Tobias Nipkow
and Dániel Somogyi
|
2018-05-25: Hidden Markov Models
Author:
Simon Wimmer
|
2018-05-24: Probabilistic Timed Automata
Authors:
Simon Wimmer
and Johannes Hölzl
|
2018-05-23: Irrational Rapidly Convergent Series
Authors:
Angeliki Koutsoukou-Argyraki
and Wenda Li
|
2018-05-23: Axiom Systems for Category Theory in Free Logic
Authors:
Christoph Benzmüller
and Dana Scott
|
2018-05-22: Monadification, Memoization and Dynamic Programming
Authors:
Simon Wimmer,
Shuwei Hu
and Tobias Nipkow
|
2018-05-10: OpSets: Sequential Specifications for Replicated Datatypes
Authors:
Martin Kleppmann,
Victor B. F. Gomes,
Dominic P. Mulligan
and Alastair R. Beresford
|
2018-05-07: An Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties
Authors:
Oliver Bračevac,
Richard Gay,
Sylvia Grewe,
Heiko Mantel,
Henning Sudbrock
and Markus Tasch
|
2018-04-29: WebAssembly
Author:
Conrad Watt
|
2018-04-27: VerifyThis 2018 - Polished Isabelle Solutions
Authors:
Peter Lammich
and Simon Wimmer
|
2018-04-24: Bounded Natural Functors with Covariance and Contravariance
Authors:
Andreas Lochbihler
and Joshua Schneider
|
2018-03-22: The Incompatibility of Fishburn-Strategyproofness and Pareto-Efficiency
Authors:
Felix Brandt,
Manuel Eberl,
Christian Saile
and Christian Stricker
|
2018-03-13: Weight-Balanced Trees
Authors:
Tobias Nipkow
and Stefan Dirix
|
2018-03-12: CakeML
Authors:
Lars Hupel
and Yu Zhang
|
2018-03-01: A Theory of Architectural Design Patterns
Author:
Diego Marmsoler
|
2018-02-26: Hoare Logics for Time Bounds
Authors:
Maximilian P. L. Haslbeck
and Tobias Nipkow
|
2018-02-06: Treaps
Authors:
Maximilian Haslbeck,
Manuel Eberl
and Tobias Nipkow
|
2018-02-06: A verified factorization algorithm for integer polynomials with polynomial complexity
Authors:
Jose Divasón,
Sebastiaan Joosten,
René Thiemann
and Akihisa Yamada
|
2018-02-06: First-Order Terms
Authors:
Christian Sternagel
and René Thiemann
|
2018-02-06: The Error Function
Author:
Manuel Eberl
|
2018-02-02: A verified LLL algorithm
Authors:
Ralph Bottesch,
Jose Divasón,
Maximilian Haslbeck,
Sebastiaan Joosten,
René Thiemann
and Akihisa Yamada
|
2018-01-18: Formalization of Bachmair and Ganzinger's Ordered Resolution Prover
Authors:
Anders Schlichtkrull,
Jasmin Christian Blanchette,
Dmitriy Traytel
and Uwe Waldmann
|
2018-01-16: Gromov Hyperbolicity
Author:
Sebastien Gouezel
|
2018-01-11: An Isabelle/HOL formalisation of Green's Theorem
Authors:
Mohammad Abdulaziz
and Lawrence C. Paulson
|
2018-01-08: Taylor Models
Authors:
Christoph Traut
and Fabian Immler
|
| 2017 |
2017-12-22: The Falling Factorial of a Sum
Author:
Lukas Bulwahn
|
2017-12-21: The Median-of-Medians Selection Algorithm
Author:
Manuel Eberl
|
2017-12-21: The Mason–Stothers Theorem
Author:
Manuel Eberl
|
2017-12-21: Dirichlet L-Functions and Dirichlet's Theorem
Author:
Manuel Eberl
|
2017-12-19: Operations on Bounded Natural Functors
Authors:
Jasmin Christian Blanchette,
Andrei Popescu
and Dmitriy Traytel
|
2017-12-18: The string search algorithm by Knuth, Morris and Pratt
Authors:
Fabian Hellauer
and Peter Lammich
|
2017-11-22: Stochastic Matrices and the Perron-Frobenius Theorem
Author:
René Thiemann
|
2017-11-09: The IMAP CmRDT
Authors:
Tim Jungnickel,
Lennart Oldenburg
and Matthias Loibl
|
2017-11-06: Hybrid Multi-Lane Spatial Logic
Author:
Sven Linker
|
2017-10-26: The Kuratowski Closure-Complement Theorem
Authors:
Peter Gammie
and Gianpaolo Gioiosa
|
2017-10-19: Transition Systems and Automata
Author:
Julian Brunner
|
2017-10-19: Büchi Complementation
Author:
Julian Brunner
|
2017-10-17: Evaluate Winding Numbers through Cauchy Indices
Author:
Wenda Li
|
2017-10-17: Count the Number of Complex Roots
Author:
Wenda Li
|
2017-10-14: Homogeneous Linear Diophantine Equations
Authors:
Florian Messner,
Julian Parsert,
Jonas Schöpf
and Christian Sternagel
|
2017-10-12: The Hurwitz and Riemann ζ Functions
Author:
Manuel Eberl
|
2017-10-12: Linear Recurrences
Author:
Manuel Eberl
|
2017-10-12: Dirichlet Series
Author:
Manuel Eberl
|
2017-09-21: Computer-assisted Reconstruction and Assessment of E. J. Lowe's Modal Ontological Argument
Authors:
David Fuenmayor
and Christoph Benzmüller
|
2017-09-17: Representation and Partial Automation of the Principia Logico-Metaphysica in Isabelle/HOL
Author:
Daniel Kirchner
|
2017-09-06: Anselm's God in Isabelle/HOL
Author:
Ben Blumson
|
2017-09-01: Microeconomics and the First Welfare Theorem
Authors:
Julian Parsert
and Cezary Kaliszyk
|
2017-08-20: Root-Balanced Tree
Author:
Tobias Nipkow
|
2017-08-20: Orbit-Stabiliser Theorem with Application to Rotational Symmetries
Author:
Jonas Rädle
|
2017-08-16: The LambdaMu-calculus
Authors:
Cristina Matache,
Victor B. F. Gomes
and Dominic P. Mulligan
|
2017-07-31: Stewart's Theorem and Apollonius' Theorem
Author:
Lukas Bulwahn
|
2017-07-28: Dynamic Architectures
Author:
Diego Marmsoler
|
2017-07-21: Declarative Semantics for Functional Languages
Author:
Jeremy Siek
|
2017-07-15: HOLCF-Prelude
Authors:
Joachim Breitner,
Brian Huffman,
Neil Mitchell
and Christian Sternagel
|
2017-07-13: Minkowski's Theorem
Author:
Manuel Eberl
|
2017-07-09: Verified Metatheory and Type Inference for a Name-Carrying Simply-Typed Lambda Calculus
Author:
Michael Rawson
|
2017-07-07: A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes
Authors:
Victor B. F. Gomes,
Martin Kleppmann,
Dominic P. Mulligan
and Alastair R. Beresford
|
2017-07-06: Stone-Kleene Relation Algebras
Author:
Walter Guttmann
|
2017-06-21: Propositional Proof Systems
Authors:
Julius Michaelis
and Tobias Nipkow
|
2017-06-13: Partial Semigroups and Convolution Algebras
Authors:
Brijesh Dongol,
Victor B. F. Gomes,
Ian J. Hayes
and Georg Struth
|
2017-06-06: Buffon's Needle Problem
Author:
Manuel Eberl
|
2017-06-01: Formalizing Push-Relabel Algorithms
Authors:
Peter Lammich
and S. Reza Sefidgar
|
2017-06-01: Flow Networks and the Min-Cut-Max-Flow Theorem
Authors:
Peter Lammich
and S. Reza Sefidgar
|
2017-05-25: Optics
Authors:
Simon Foster
and Frank Zeyda
|
2017-05-24: Developing Security Protocols by Refinement
Authors:
Christoph Sprenger
and Ivano Somaini
|
2017-05-24: Dictionary Construction
Author:
Lars Hupel
|
2017-05-08: The Floyd-Warshall Algorithm for Shortest Paths
Authors:
Simon Wimmer
and Peter Lammich
|
2017-05-05: Probabilistic while loop
Author:
Andreas Lochbihler
|
2017-05-05: Effect polymorphism in higher-order logic
Author:
Andreas Lochbihler
|
2017-05-05: Monad normalisation
Authors:
Joshua Schneider,
Manuel Eberl
and Andreas Lochbihler
|
2017-05-05: Game-based cryptography in HOL
Authors:
Andreas Lochbihler,
S. Reza Sefidgar
and Bhargav Bhatt
|
2017-05-05: CryptHOL
Author:
Andreas Lochbihler
|
2017-05-04: Monoidal Categories
Author:
Eugene W. Stark
|
2017-05-01: Types, Tableaus and Gödel’s God in Isabelle/HOL
Authors:
David Fuenmayor
and Christoph Benzmüller
|
2017-04-28: Local Lexing
Author:
Steven Obua
|
2017-04-19: Constructor Functions
Author:
Lars Hupel
|
2017-04-18: Lazifying case constants
Author:
Lars Hupel
|
2017-04-06: Subresultants
Authors:
Sebastiaan Joosten,
René Thiemann
and Akihisa Yamada
|
2017-04-04: Expected Shape of Random Binary Search Trees
Author:
Manuel Eberl
|
2017-03-15: The number of comparisons in QuickSort
Author:
Manuel Eberl
|
2017-03-15: Lower bound on comparison-based sorting algorithms
Author:
Manuel Eberl
|
2017-03-10: The Euler–MacLaurin Formula
Author:
Manuel Eberl
|
2017-02-28: The Group Law for Elliptic Curves
Author:
Stefan Berghofer
|
2017-02-26: Menger's Theorem
Author:
Christoph Dittmann
|
2017-02-13: Differential Dynamic Logic
Author:
Brandon Bohrer
|
2017-02-10: Abstract Soundness
Authors:
Jasmin Christian Blanchette,
Andrei Popescu
and Dmitriy Traytel
|
2017-02-07: Stone Relation Algebras
Author:
Walter Guttmann
|
2017-01-31: Refining Authenticated Key Agreement with Strong Adversaries
Authors:
Joseph Lallemand
and Christoph Sprenger
|
2017-01-24: Bernoulli Numbers
Authors:
Lukas Bulwahn
and Manuel Eberl
|
2017-01-17: Minimal Static Single Assignment Form
Authors:
Max Wagner
and Denis Lohner
|
2017-01-17: Bertrand's postulate
Authors:
Julian Biendarra
and Manuel Eberl
|
2017-01-12: The Transcendence of e
Author:
Manuel Eberl
|
2017-01-08: Formal Network Models and Their Application to Firewall Policies
Authors:
Achim D. Brucker,
Lukas Brügger
and Burkhart Wolff
|
2017-01-03: Verification of a Diffie-Hellman Password-based Authentication Protocol by Extending the Inductive Method
Author:
Pasquale Noce
|
2017-01-01: First-Order Logic According to Harrison
Authors:
Alexander Birch Jensen,
Anders Schlichtkrull
and Jørgen Villadsen
|
| 2016 |
2016-12-30: Concurrent Refinement Algebra and Rely Quotients
Authors:
Julian Fell,
Ian J. Hayes
and Andrius Velykis
|
2016-12-29: The Twelvefold Way
Author:
Lukas Bulwahn
|
2016-12-20: Proof Strategy Language
Author:
Yutaka Nagashima
|
2016-12-07: Paraconsistency
Authors:
Anders Schlichtkrull
and Jørgen Villadsen
|
2016-11-29: COMPLX: A Verification Framework for Concurrent Imperative Programs
Authors:
Sidney Amani,
June Andronick,
Maksym Bortin,
Corey Lewis,
Christine Rizkallah
and Joseph Tuong
|
2016-11-23: Abstract Interpretation of Annotated Commands
Author:
Tobias Nipkow
|
2016-11-16: Separata: Isabelle tactics for Separation Algebra
Authors:
Zhe Hou,
David Sanan,
Alwen Tiu,
Rajeev Gore
and Ranald Clouston
|
2016-11-12: Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals
Authors:
Jasmin Christian Blanchette,
Mathias Fleury
and Dmitriy Traytel
|
2016-11-12: Formalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Terms
Authors:
Heiko Becker,
Jasmin Christian Blanchette,
Uwe Waldmann
and Daniel Wand
|
2016-11-10: Expressiveness of Deep Learning
Author:
Alexander Bentkamp
|
2016-10-25: Modal Logics for Nominal Transition Systems
Authors:
Tjark Weber,
Lars-Henrik Eriksson,
Joachim Parrow,
Johannes Borgström
and Ramunas Gutkovas
|
2016-10-24: Stable Matching
Author:
Peter Gammie
|
2016-10-21: LOFT — Verified Migration of Linux Firewalls to SDN
Authors:
Julius Michaelis
and Cornelius Diekmann
|
2016-10-19: Source Coding Theorem
Authors:
Quentin Hibon
and Lawrence C. Paulson
|
2016-10-19: A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor
Authors:
Zhe Hou,
David Sanan,
Alwen Tiu
and Yang Liu
|
2016-10-14: The Factorization Algorithm of Berlekamp and Zassenhaus
Authors:
Jose Divasón,
Sebastiaan Joosten,
René Thiemann
and Akihisa Yamada
|
2016-10-11: Intersecting Chords Theorem
Author:
Lukas Bulwahn
|
2016-10-05: Lp spaces
Author:
Sebastien Gouezel
|
2016-09-30: Fisher–Yates shuffle
Author:
Manuel Eberl
|
2016-09-29: Allen's Interval Calculus
Author:
Fadoua Ghourabi
|
2016-09-23: Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms
Authors:
Jasmin Christian Blanchette,
Uwe Waldmann
and Daniel Wand
|
2016-09-09: Iptables Semantics
Authors:
Cornelius Diekmann
and Lars Hupel
|
2016-09-06: A Variant of the Superposition Calculus
Author:
Nicolas Peltier
|
2016-09-06: Stone Algebras
Author:
Walter Guttmann
|
2016-09-01: Stirling's formula
Author:
Manuel Eberl
|
2016-08-31: Routing
Authors:
Julius Michaelis
and Cornelius Diekmann
|
2016-08-24: Simple Firewall
Authors:
Cornelius Diekmann,
Julius Michaelis
and Maximilian Haslbeck
|
2016-08-18: Infeasible Paths Elimination by Symbolic Execution Techniques: Proof of Correctness and Preservation of Paths
Authors:
Romain Aissat,
Frederic Voisin
and Burkhart Wolff
|
2016-08-12: Formalizing the Edmonds-Karp Algorithm
Authors:
Peter Lammich
and S. Reza Sefidgar
|
2016-08-08: The Imperative Refinement Framework
Author:
Peter Lammich
|
2016-08-07: Ptolemy's Theorem
Author:
Lukas Bulwahn
|
2016-07-17: Surprise Paradox
Author:
Joachim Breitner
|
2016-07-14: Pairing Heap
Authors:
Hauke Brinkop
and Tobias Nipkow
|
2016-07-05: A Framework for Verifying Depth-First Search Algorithms
Authors:
Peter Lammich
and René Neumann
|
2016-07-01: Chamber Complexes, Coxeter Systems, and Buildings
Author:
Jeremy Sylvestre
|
2016-06-30: The Z Property
Authors:
Bertram Felgenhauer,
Julian Nagele,
Vincent van Oostrom
and Christian Sternagel
|
2016-06-30: The Resolution Calculus for First-Order Logic
Author:
Anders Schlichtkrull
|
2016-06-28: IP Addresses
Authors:
Cornelius Diekmann,
Julius Michaelis
and Lars Hupel
|
2016-06-28: Compositional Security-Preserving Refinement for Concurrent Imperative Programs
Authors:
Toby Murray,
Robert Sison,
Edward Pierzchalski
and Christine Rizkallah
|
2016-06-26: Category Theory with Adjunctions and Limits
Author:
Eugene W. Stark
|
2016-06-26: Cardinality of Multisets
Author:
Lukas Bulwahn
|
2016-06-25: A Dependent Security Type System for Concurrent Imperative Programs
Authors:
Toby Murray,
Robert Sison,
Edward Pierzchalski
and Christine Rizkallah
|
2016-06-21: Catalan Numbers
Author:
Manuel Eberl
|
2016-06-18: Program Construction and Verification Components Based on Kleene Algebra
Authors:
Victor B. F. Gomes
and Georg Struth
|
2016-06-13: Conservation of CSP Noninterference Security under Concurrent Composition
Author:
Pasquale Noce
|
2016-06-09: Finite Machine Word Library
Authors:
Joel Beeren,
Matthew Fernandez,
Xin Gao,
Gerwin Klein,
Rafal Kolanski,
Japheth Lim,
Corey Lewis,
Daniel Matichuk
and Thomas Sewell
|
2016-05-31: Tree Decomposition
Author:
Christoph Dittmann
|
2016-05-24: POSIX Lexing with Derivatives of Regular Expressions
Authors:
Fahad Ausaf,
Roy Dyckhoff
and Christian Urban
|
2016-05-24: Cardinality of Equivalence Relations
Author:
Lukas Bulwahn
|
2016-05-20: Perron-Frobenius Theorem for Spectral Radius Analysis
Authors:
Jose Divasón,
Ondřej Kunčar,
René Thiemann
and Akihisa Yamada
|
2016-05-20: The meta theory of the Incredible Proof Machine
Authors:
Joachim Breitner
and Denis Lohner
|
2016-05-18: A Constructive Proof for FLP
Authors:
Benjamin Bisping,
Paul-David Brodmann,
Tim Jungnickel,
Christina Rickmann,
Henning Seidler,
Anke Stüber,
Arno Wilhelm-Weidner,
Kirstin Peters
and Uwe Nestmann
|
2016-05-09: A Formal Proof of the Max-Flow Min-Cut Theorem for Countable Networks
Author:
Andreas Lochbihler
|
2016-05-05: Randomised Social Choice Theory
Author:
Manuel Eberl
|
2016-05-04: The Incompatibility of SD-Efficiency and SD-Strategy-Proofness
Author:
Manuel Eberl
|
2016-05-04: Spivey's Generalized Recurrence for Bell Numbers
Author:
Lukas Bulwahn
|
2016-05-02: Gröbner Bases Theory
Authors:
Fabian Immler
and Alexander Maletzky
|
2016-04-28: No Faster-Than-Light Observers
Authors:
Mike Stannett
and István Németi
|
2016-04-27: Algorithms for Reduced Ordered Binary Decision Diagrams
Authors:
Julius Michaelis,
Maximilian Haslbeck,
Peter Lammich
and Lars Hupel
|
2016-04-27: A formalisation of the Cocke-Younger-Kasami algorithm
Author:
Maksym Bortin
|
2016-04-26: Conservation of CSP Noninterference Security under Sequential Composition
Author:
Pasquale Noce
|
2016-04-12: Kleene Algebras with Domain
Authors:
Victor B. F. Gomes,
Walter Guttmann,
Peter Höfner,
Georg Struth
and Tjark Weber
|
2016-03-11: Propositional Resolution and Prime Implicates Generation
Author:
Nicolas Peltier
|
2016-03-08: Timed Automata
Author:
Simon Wimmer
|
2016-03-08: The Cartan Fixed Point Theorems
Author:
Lawrence C. Paulson
|
2016-03-01: Linear Temporal Logic
Author:
Salomon Sickert
|
2016-02-17: Analysis of List Update Algorithms
Authors:
Maximilian P.L. Haslbeck
and Tobias Nipkow
|
2016-02-05: Verified Construction of Static Single Assignment Form
Authors:
Sebastian Ullrich
and Denis Lohner
|
2016-01-29: Polynomial Interpolation
Authors:
René Thiemann
and Akihisa Yamada
|
2016-01-29: Polynomial Factorization
Authors:
René Thiemann
and Akihisa Yamada
|
2016-01-20: Knot Theory
Author:
T.V.H. Prathamesh
|
2016-01-18: Tensor Product of Matrices
Author:
T.V.H. Prathamesh
|
2016-01-14: Cardinality of Number Partitions
Author:
Lukas Bulwahn
|
| 2014 |
2014-11-28: The Unified Policy Framework (UPF)
Authors:
Achim D. Brucker,
Lukas Brügger
and Burkhart Wolff
|
2014-10-23: Loop freedom of the (untimed) AODV routing protocol
Authors:
Timothy Bourke
and Peter Höfner
|
2014-10-13: Lifting Definition Option
Author:
René Thiemann
|
2014-10-10: Stream Fusion in HOL with Code Generation
Authors:
Andreas Lochbihler
and Alexandra Maximova
|
2014-10-09: A Verified Compiler for Probability Density Functions
Authors:
Manuel Eberl,
Johannes Hölzl
and Tobias Nipkow
|
2014-10-08: Formalization of Refinement Calculus for Reactive Systems
Author:
Viorel Preoteasa
|
2014-10-03: XML
Authors:
Christian Sternagel
and René Thiemann
|
2014-10-03: Certification Monads
Authors:
Christian Sternagel
and René Thiemann
|
2014-09-25: Imperative Insertion Sort
Author:
Christian Sternagel
|
2014-09-19: The Sturm-Tarski Theorem
Author:
Wenda Li
|
2014-09-15: The Cayley-Hamilton Theorem
Authors:
Stephan Adelsberger,
Stefan Hetzl
and Florian Pollak
|
2014-09-09: The Jordan-Hölder Theorem
Author:
Jakob von Raumer
|
2014-09-04: Priority Queues Based on Braun Trees
Author:
Tobias Nipkow
|
2014-09-03: Gauss-Jordan Algorithm and Its Applications
Authors:
Jose Divasón
and Jesús Aransay
|
2014-08-29: Vector Spaces
Author:
Holden Lee
|
2014-08-29: Real-Valued Special Functions: Upper and Lower Bounds
Author:
Lawrence C. Paulson
|
2014-08-13: Skew Heap
Author:
Tobias Nipkow
|
2014-08-12: Splay Tree
Author:
Tobias Nipkow
|
2014-07-29: Haskell's Show Class in Isabelle/HOL
Authors:
Christian Sternagel
and René Thiemann
|
2014-07-18: Formal Specification of a Generic Separation Kernel
Authors:
Freek Verbeek,
Sergey Tverdyshev,
Oto Havle,
Holger Blasum,
Bruno Langenstein,
Werner Stephan,
Yakoub Nemouchi,
Abderrahmane Feliachi,
Burkhart Wolff
and Julien Schmaltz
|
2014-07-13: pGCL for Isabelle
Author:
David Cock
|
2014-07-07: Amortized Complexity Verified
Author:
Tobias Nipkow
|
2014-07-04: Network Security Policy Verification
Author:
Cornelius Diekmann
|
2014-07-03: Pop-Refinement
Author:
Alessandro Coglio
|
2014-06-12: Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
Authors:
Dmitriy Traytel
and Tobias Nipkow
|
2014-06-08: Boolean Expression Checkers
Author:
Tobias Nipkow
|
2014-05-28: Promela Formalization
Author:
René Neumann
|
2014-05-28: Converting Linear-Time Temporal Logic to Generalized Büchi Automata
Authors:
Alexander Schimpf
and Peter Lammich
|
2014-05-28: Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm
Author:
Peter Lammich
|
2014-05-28: A Fully Verified Executable LTL Model Checker
Authors:
Javier Esparza,
Peter Lammich,
René Neumann,
Tobias Nipkow,
Alexander Schimpf
and Jan-Georg Smaus
|
2014-05-28: The CAVA Automata Library
Author:
Peter Lammich
|
2014-05-23: Transitive closure according to Roy-Floyd-Warshall
Author:
Makarius Wenzel
|
2014-05-23: Noninterference Security in Communicating Sequential Processes
Author:
Pasquale Noce
|
2014-05-21: Regular Algebras
Authors:
Simon Foster
and Georg Struth
|
2014-04-28: Formalisation and Analysis of Component Dependencies
Author:
Maria Spichkova
|
2014-04-23: A Formalization of Declassification with WHAT-and-WHERE-Security
Authors:
Sylvia Grewe,
Alexander Lux,
Heiko Mantel
and Jens Sauer
|
2014-04-23: A Formalization of Strong Security
Authors:
Sylvia Grewe,
Alexander Lux,
Heiko Mantel
and Jens Sauer
|
2014-04-23: A Formalization of Assumptions and Guarantees for Compositional Noninterference
Authors:
Sylvia Grewe,
Heiko Mantel
and Daniel Schoepe
|
2014-04-22: Bounded-Deducibility Security
Authors:
Andrei Popescu
and Peter Lammich
|
2014-04-16: A shallow embedding of HyperCTL*
Authors:
Markus N. Rabe,
Peter Lammich
and Andrei Popescu
|
2014-04-16: Abstract Completeness
Authors:
Jasmin Christian Blanchette,
Andrei Popescu
and Dmitriy Traytel
|
2014-04-13: Discrete Summation
Author:
Florian Haftmann
|
2014-04-03: Syntax and semantics of a GPU kernel programming language
Author:
John Wickerson
|
2014-03-11: Probabilistic Noninterference
Authors:
Andrei Popescu
and Johannes Hölzl
|
2014-03-08: Mechanization of the Algebra for Wireless Networks (AWN)
Author:
Timothy Bourke
|
2014-02-18: Mutually Recursive Partial Functions
Author:
René Thiemann
|
2014-02-13: Properties of Random Graphs -- Subgraph Containment
Author:
Lars Hupel
|
2014-02-11: Verification of Selection and Heap Sort Using Locales
Author:
Danijela Petrovic
|
2014-02-07: Affine Arithmetic
Author:
Fabian Immler
|
2014-02-06: Implementing field extensions of the form Q[sqrt(b)]
Author:
René Thiemann
|
2014-01-30: Unified Decision Procedures for Regular Expression Equivalence
Authors:
Tobias Nipkow
and Dmitriy Traytel
|
2014-01-28: Secondary Sylow Theorems
Author:
Jakob von Raumer
|
2014-01-25: Relation Algebra
Authors:
Alasdair Armstrong,
Simon Foster,
Georg Struth
and Tjark Weber
|
2014-01-23: Kleene Algebra with Tests and Demonic Refinement Algebras
Authors:
Alasdair Armstrong,
Victor B. F. Gomes
and Georg Struth
|
2014-01-16: Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5
Authors:
Achim D. Brucker,
Frédéric Tuong
and Burkhart Wolff
|
2014-01-11: Sturm's Theorem
Author:
Manuel Eberl
|
2014-01-11: Compositional Properties of Crypto-Based Components
Author:
Maria Spichkova
|
|