diff --git a/web/about.html b/web/about.html --- a/web/about.html +++ b/web/about.html @@ -1,144 +1,144 @@
|
Archive of Formal Proofs
|
|
Citing Entries
|
|
Download the Archive
|
|
Loop freedom of the (untimed) AODV routing protocol
|
|
AVL Trees
|
|
Mechanization of the Algebra for Wireless Networks (AWN)
|
|
Abortable Linearizable Modules
|
|
Abstract Interpretation of Annotated Commands
|
|
Abstract Hoare Logics
|
|
Abstract Rewriting
|
|
Abstract Completeness
|
|
Abstract Soundness
|
|
Formalisation of an Adaptive State Counting Algorithm
|
|
Affine Arithmetic
|
|
Aggregation Algebras
|
|
The Akra-Bazzi theorem and the Master theorem
|
|
Algebraic Numbers in Isabelle/HOL
|
|
Program Construction and Verification Components Based on Kleene Algebra
|
|
Allen's Interval Calculus
|
|
Amortized Complexity Verified
|
|
Anselm's God in Isabelle/HOL
|
|
Applicative Lifting
|
|
Verified Approximation Algorithms
|
|
A Theory of Architectural Design Patterns
|
|
Aristotle's Assertoric Syllogistic
|
|
Arithmetic progressions and relative primes
|
|
Arrow and Gibbard-Satterthwaite
|
|
Auto2 Prover
|
|
Verifying Imperative Programs using Auto2
|
|
AutoFocus Stream Processing for Single-Clocking and Multi-Clocking Semantics
|
|
Automatic Data Refinement
|
|
Axiom Systems for Category Theory in Free Logic
|
|
BDD Normalisation
|
|
Bounded Natural Functors with Covariance and Contravariance
|
|
Operations on Bounded Natural Functors
|
|
Spivey's Generalized Recurrence for Bell Numbers
|
|
The Factorization Algorithm of Berlekamp and Zassenhaus
|
|
Bernoulli Numbers
|
|
Bertrand's postulate
|
|
Bicategories
|
|
Binary Search Trees
|
|
A General Theory of Syntax with Bindings
|
|
Binomial Heaps and Skew Binomial Heaps
|
|
Functional Binomial Queues
|
|
Bondy's Theorem
|
|
Boolean Expression Checkers
|
|
Bounded-Deducibility Security
|
|
Büchi Complementation
|
|
The Budan-Fourier Theorem and Counting Real Roots with Multiplicity
|
|
Buffon's Needle Problem
|
|
Chamber Complexes, Coxeter Systems, and Buildings
|
|
A Bytecode Logic for JML and Types
|
|
Communicating Concurrent Kleene Algebra for Distributed Systems Specification
|
|
The CAVA Automata Library
|
|
A Fully Verified Executable LTL Model Checker
|
|
CCS in nominal logic
|
|
Formal Specification of a Generic Separation Kernel
|
|
A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes
|
|
A formalisation of the Cocke-Younger-Kasami algorithm
|
|
CakeML
|
|
A Verified Code Generator from Isabelle/HOL to CakeML
|
|
The Safety of Call Arity
|
|
Cardinality of Equivalence Relations
|
|
Cardinality of Multisets
|
|
Cardinality of Number Partitions
|
|
Cardinality of Set Partitions
|
|
The Cartan Fixed Point Theorems
|
|
Generating Cases from Labeled Subgoals
|
|
Catalan Numbers
|
|
Category Theory to Yoneda's Lemma
|
|
Category Theory
|
|
Category Theory with Adjunctions and Limits
|
|
Cauchy's Mean Theorem and the Cauchy-Schwarz Inequality
|
|
The Cayley-Hamilton Theorem
|
|
Certification Monads
|
|
Intersecting Chords Theorem
|
|
Isabelle/Circus
|
|
Clean - An Abstract Imperative Programming Language and its Theory
|
|
Instances of Schneider's generalized protocol of clock synchronization
|
|
Closest Pair of Points Algorithms
|
|
An Example of a Cofinitary Group in Isabelle/HOL
|
|
Coinductive
|
|
A Codatatype of Formal Languages
|
|
Collections Framework
|
|
Lower bound on comparison-based sorting algorithms
|
|
Complete Non-Orders and Fixed Points
|
|
Completeness theorem
|
|
Complex Geometry
|
|
COMPLX: A Verification Framework for Concurrent Imperative Programs
|
|
Formalisation and Analysis of Component Dependencies
|
|
Relaxing Safely: Verified On-the-Fly Garbage Collection for x86-TSO
|
|
Concurrent IMP
|
|
Concurrent Refinement Algebra and Rely Quotients
|
|
Formalization of Concurrent Revisions
|
|
Consensus Refined
|
|
Constructive Cryptography in HOL
|
|
Constructor Functions
|
|
Light-weight Containers
|
|
CoreC++
|
|
A Formal Model of the Document Object Model
|
|
Count the Number of Complex Roots
|
|
CryptHOL
|
|
Compositional Properties of Crypto-Based Components
|
|
A Framework for Verifying Depth-First Search Algorithms
|
|
A Fast SAT Solver for Isabelle in Standard ML
|
|
Semantics and Data Refinement of Invariant Based Programs
|
|
Generating linear orders for datatypes
|
|
Declarative Semantics for Functional Languages
|
|
Decreasing Diagrams II
|
|
Decreasing Diagrams
|
|
Expressiveness of Deep Learning
|
|
A Verified Compiler for Probability Density Functions
|
|
Compositional Security-Preserving Refinement for Concurrent Imperative Programs
|
|
A Dependent Security Type System for Concurrent Imperative Programs
|
|
Depth First Search
|
|
Derangements Formula
|
|
Deriving class instances for datatypes
|
|
Descartes' Rule of Signs
|
|
Dictionary Construction
|
|
Differential Dynamic Logic
|
|
Differential Game Logic
|
|
Dijkstra's Shortest Path Algorithm
|
|
Homogeneous Linear Diophantine Equations
|
|
Dirichlet L-Functions and Dirichlet's Theorem
|
|
Dirichlet Series
|
|
Pricing in discrete financial models
|
|
Discrete Summation
|
|
Proving the Correctness of Disk Paxos
|
|
Dynamic Architectures
|
|
Parameterized Dynamic Tables
|
|
The Transcendence of e
|
|
Echelon Form
|
|
Formalizing the Edmonds-Karp Algorithm
|
|
Efficient Mergesort
|
|
The Group Law for Elliptic Curves
|
|
Analysing and Comparing Encodability Criteria for Process Calculi
|
|
Epistemic Logic
|
|
Ergodic Theory
|
|
The Error Function
|
|
The Euler–MacLaurin Formula
|
|
Euler's Partition Theorem
|
|
Example Submission
|
|
Fast Fourier Transform
|
|
A Constructive Proof for FLP
|
|
First-Order Logic According to Fitting
|
|
First-Order Logic According to Harrison
|
|
A Sequent Calculus for First-Order Logic
|
|
Upper Bounding Diameters of State Spaces of Factored Transition Systems
|
|
The Falling Factorial of a Sum
|
|
Farkas' Lemma and Motzkin's Transposition Theorem
|
|
A Theory of Featherweight Java in Isabelle/HOL
|
|
Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5
|
|
Fermat's Last Theorem for Exponents 3 and 4 and the Parametrisation of Pythagorean Triples
|
|
File Refinement
|
|
Code Generation for Functions as Data
|
|
Finger Trees
|
|
Finite Automata in Hereditarily Finite Set Theory
|
|
First-Order Terms
|
|
Microeconomics and the First Welfare Theorem
|
|
The Incompatibility of Fishburn-Strategyproofness and Pareto-Efficiency
|
|
Fisher–Yates shuffle
|
|
Flow Networks and the Min-Cut-Max-Flow Theorem
|
|
The Floyd-Warshall Algorithm for Shortest Paths
|
|
Flyspeck I: Tame Graphs
|
|
Stream Processing Components: Isabelle/HOL Formalisation and Case Studies
|
|
Verified Construction of Static Single Assignment Form
|
|
Derivatives of Logical Formulas
|
|
Fourier Series
|
|
Free Boolean Algebra
|
|
Free Groups
|
|
Fun With Functions
|
|
Fun With Tilings
|
|
Functional Automata
|
|
A Verified Functional Implementation of Bachmair and Ganzinger's Ordered Resolution Prover
|
|
Furstenberg's topology and his proof of the infinitude of primes
|
|
Syntax and semantics of a GPU kernel programming language
|
|
Verified Efficient Implementation of Gabow's Strongly Connected Components Algorithm
|
|
Game-based cryptography in HOL
|
|
Gauss-Jordan Elimination for Matrices Represented as Functions
|
|
Gauss-Jordan Algorithm and Its Applications
|
|
Gauss Sums and the Pólya–Vinogradov Inequality
|
|
Formalization of a Generalized Protocol for Clock Synchronization
|
|
The General Triangle Is Unique
|
|
An Efficient Generalization of Counting Sort for Large, possibly Infinite Key Ranges
|
|
Deriving generic class instances for datatypes
|
|
Formalization of Multiway-Join Algorithms
|
|
Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL
|
|
A Probabilistic Proof of the Girth-Chromatic Number Theorem
|
|
Gödel's God in Isabelle/HOL
|
|
Implementing the Goodstein Function in λ-Calculus
|
|
Verification of the Deutsch-Schorr-Waite Graph Marking Algorithm using Data Refinement
|
|
Graph Saturation
|
|
Graph Theory
|
|
An Isabelle/HOL formalisation of Green's Theorem
|
|
Gröbner Bases Theory
|
|
Gröbner Bases, Macaulay Matrices and Dubé's Degree Bounds
|
|
Gromov Hyperbolicity
|
|
Groups, Rings and Modules
|
|
HOL-CSP Version 2.0
|
|
HOLCF-Prelude
|
|
Backing up Slicing: Verifying the Interprocedural Two-Phase Horwitz-Reps-Binkley Slicer
|
|
Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model
|
|
Hello World
|
|
The Hereditarily Finite Sets
|
|
Hermite Normal Form
|
|
Hidden Markov Models
|
|
An Algebra for Higher-Order Terms
|
|
Hoare Logics for Time Bounds
|
|
Hotel Key Card System
|
|
The Textbook Proof of Huffman's Algorithm
|
|
Formalizing a Seligman-Style Tableau System for Hybrid Logic
|
|
Hybrid Multi-Lane Spatial Logic
|
|
Verification Components for Hybrid Systems
|
|
A shallow embedding of HyperCTL*
|
|
A Formal Model of IEEE Floating Point Arithmetic
|
|
The IMAP CmRDT
|
|
Selected Problems from the International Mathematical Olympiad 2019
|
|
IMP2 – Simple Program Verification in Isabelle/HOL
|
|
Binary Heaps for IMP2
|
|
IP Addresses
|
|
Imperative Insertion Sort
|
|
Proving the Impossibility of Trisecting an Angle and Doubling the Cube
|
|
Gödel's Incompleteness Theorems
|
|
The meta theory of the Incredible Proof Machine
|
|
Inductive Study of Confidentiality
|
|
Infeasible Paths Elimination by Symbolic Execution Techniques: Proof of Correctness and Preservation of Paths
|
|
Information Flow Noninterference via Slicing
|
|
Inter-Procedural Information Flow Noninterference via Slicing
|
|
Integration theory and random variables
|
|
Interval Arithmetic on 32-bit Words
|
|
Iptables Semantics
|
|
Irrational Rapidly Convergent Series
|
|
Isabelle/C
|
|
A Meta-Model for the Isabelle API
|
|
A Case Study in Basic Algebra
|
|
Jinja is not Java
|
|
Jinja with Threads
|
|
Jive Data and Store Model
|
|
The Jordan-Hölder Theorem
|
|
Matrices, Jordan Normal Forms, and Spectral Radius Theory
|
|
Kleene Algebras with Domain
|
|
Kleene Algebra with Tests and Demonic Refinement Algebras
|
|
Knowledge-based programs
|
|
Multidimensional Binary Search Trees
|
|
Refining Authenticated Key Agreement with Strong Adversaries
|
|
Kleene Algebra
|
|
Knot Theory
|
|
The string search algorithm by Knuth, Morris and Pratt
|
|
The Königsberg Bridge Problem and the Friendship Theorem
|
|
Kruskal's Algorithm for Minimum Spanning Forest
|
|
The Kuratowski Closure-Complement Theorem
|
|
A verified LLL algorithm
|
|
A verified factorization algorithm for integer polynomials with polynomial complexity
|
|
LOFT — Verified Migration of Linux Firewalls to SDN
|
|
Linear Temporal Logic
|
|
A Compositional and Unified Translation of LTL into ω-Automata
|
|
Converting Linear Temporal Logic to Deterministic (Generalized) Rabin Automata
|
|
Converting Linear-Time Temporal Logic to Generalized Büchi Automata
|
|
Strong Normalization of Moggis's Computational Metalanguage
|
|
Formalization of Generic Authenticated Data Structures
|
|
The LambdaMu-calculus
|
|
Formalization of the Embedding Path Order for Lambda-Free Higher-Order Terms
|
|
Formalization of Knuth–Bendix Orders for Lambda-Free Higher-Order Terms
|
|
Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms
|
|
Landau Symbols
|
|
Laplace Transform
|
|
Latin Square
|
|
Lattice Properties
|
|
The Correctness of Launchbury's Natural Semantics for Lazy Evaluation
|
|
Lazy Lists II
|
|
Lazifying case constants
|
|
Lehmer's Theorem
|
|
Lifting Definition Option
|
|
Lightweight Java
|
|
Quantifier Elimination for Linear Arithmetic
|
|
Linear Inequalities
|
|
Linear Programming
|
|
Linear Recurrences
|
|
Liouville numbers
|
|
List Index
|
|
Infinite Lists
|
|
Reasoning about Lists via List Interleaving
|
|
The Inversions of a List
|
|
Analysis of List Update Algorithms
|
|
Local Lexing
|
|
The Localization of a Commutative Ring
|
|
Locally Nameless Sigma Calculus
|
|
Computer-assisted Reconstruction and Assessment of E. J. Lowe's Modal Ontological Argument
|
|
Lower Semicontinuous Functions
|
|
Lp spaces
|
|
A Formal Proof of the Max-Flow Min-Cut Theorem for Countable Networks
|
|
Formalization of an Optimized Monitoring Algorithm for Metric First-Order Dynamic Logic with Aggregations
|
|
Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic
|
|
Decision Procedures for MSO on Words Based on Derivatives of Regular Expressions
|
|
Markov Models
|
|
Hall's Marriage Theorem
|
|
The Mason–Stothers Theorem
|
|
Executable Matrix Operations on Matrices of Arbitrary Dimensions
|
|
Tensor Product of Matrices
|
|
Matroids
|
|
Maximum Cardinality Matching
|
|
The Median-of-Medians Selection Algorithm
|
|
Menger's Theorem
|
|
Mersenne primes and the Lucas–Lehmer test
|
|
Mini ML
|
|
Minimal Static Single Assignment Form
|
|
Minkowski's Theorem
|
|
Minsky Machines
|
|
Modal Logics for Nominal Transition Systems
|
|
An Isabelle/HOL Formalization of the Modular Assembly Kit for Security Properties
|
|
Monadification, Memoization and Dynamic Programming
|
|
Monad normalisation
|
|
Algebra of Monotonic Boolean Transformers
|
|
Monoidal Categories
|
|
Effect polymorphism in higher-order logic
|
|
Much Ado About Two
|
|
Multi-Party Computation
|
|
Binary Multirelations
|
|
The Myhill-Nerode Theorem Based on Regular Expressions
|
|
Verified Metatheory and Type Inference for a Name-Carrying Simply-Typed Lambda Calculus
|
|
Interval Temporal Logic on Natural Numbers
|
|
Native Word
|
|
Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals
|
|
Network Security Policy Verification
|
|
Von-Neumann-Morgenstern Utility Theorem
|
|
No Faster-Than-Light Observers
|
|
Nominal 2
|
|
Noninterference Security in Communicating Sequential Processes
|
|
Conservation of CSP Noninterference Security under Concurrent Composition
|
|
The Generic Unwinding Theorem for CSP Noninterference Security
|
|
The Inductive Unwinding Theorem for CSP Noninterference Security
|
|
The Ipurge Unwinding Theorem for CSP Noninterference Security
|
|
Conservation of CSP Noninterference Security under Sequential Composition
|
|
Normalization by Evaluation
|
|
Hilbert's Nullstellensatz
|
|
Octonions
|
|
OpSets: Sequential Specifications for Replicated Datatypes
|
|
Open Induction
|
|
Optics
|
|
Optimal Binary Search Trees
|
|
Orbit-Stabiliser Theorem with Application to Rotational Symmetries
|
|
Properties of Orderings and Lattices
|
|
Formalization of Bachmair and Ganzinger's Ordered Resolution Prover
|
|
Countable Ordinals
|
|
Ordinals and Cardinals
|
|
Ordinary Differential Equations
|
|
Logical Relations for PCF
|
|
Representation and Partial Automation of the Principia Logico-Metaphysica in Isabelle/HOL
|
|
POPLmark Challenge Via de Bruijn Indices
|
|
Partial Semigroups and Convolution Algebras
|
|
Pairing Heap
|
|
Paraconsistency
|
|
Positional Determinacy of Parity Games
|
|
Mutually Recursive Partial Functions
|
|
Partial Order Reduction
|
|
Verification of a Diffie-Hellman Password-based Authentication Protocol by Extending the Inductive Method
|
|
Pell's Equation
|
|
Perfect Number Theorem
|
|
Perron-Frobenius Theorem for Spectral Radius Analysis
|
|
The pi-calculus in nominal logic
|
|
The Transcendence of π
|
|
Planarity Certificates
|
|
The Poincaré-Bendixson Theorem
|
|
Poincaré Disc Model
|
|
Polynomial Factorization
|
|
Polynomial Interpolation
|
|
Executable Multivariate Polynomials
|
|
Pop-Refinement
|
|
POSIX Lexing with Derivatives of Regular Expressions
|
|
Possibilistic Noninterference
|
|
Pratt's Primality Certificates
|
|
Formalizing the Logic-Automaton Connection
|
|
Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra
|
|
Elementary Facts About the Distribution of Primes
|
|
The Divergence of the Prime Harmonic Series
|
|
The Prime Number Theorem
|
|
Priority Queues Based on Braun Trees
|
|
Priority Search Trees
|
|
Probabilistic Noninterference
|
|
Probabilistic Primality Testing
|
|
A Zoo of Probabilistic Systems
|
|
Probabilistic Timed Automata
|
|
Probabilistic while loop
|
|
Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors
|
|
Projective Geometry
|
|
Promela Formalization
|
|
Proof Strategy Language
|
|
Propositional Resolution and Prime Implicates Generation
|
|
Propositional Proof Systems
|
|
Formalizing Push-Relabel Algorithms
|
|
Pseudo Hoops
|
|
Psi-calculi in Isabelle
|
|
Ptolemy's Theorem
|
|
Quantum Hoare Logic
|
|
QR Decomposition
|
|
Quantales
|
|
Quaternions
|
|
The number of comparisons in QuickSort
|
|
RIPEMD-160
|
|
Algorithms for Reduced Ordered Binary Decision Diagrams
|
|
SHA1, RSA, PSS and more
|
|
Ramsey's theorem, infinitary version
|
|
Expected Shape of Random Binary Search Trees
|
|
Properties of Random Graphs -- Subgraph Containment
|
|
Randomised Binary Search Trees
|
|
Randomised Social Choice Theory
|
|
Rank-Nullity Theorem in Linear Algebra
|
|
Implementing field extensions of the form Q[sqrt(b)]
|
|
Recursion Theory I
|
|
The Imperative Refinement Framework
|
|
Refinement for Monadic Programs
|
|
Formalization of Refinement Calculus for Reactive Systems
|
|
Unified Decision Procedures for Regular Expression Equivalence
|
|
Regular Sets and Expressions
|
|
Regular Algebras
|
|
Relation Algebra
|
|
An Under-Approximate Relational Logic
|
|
Representations of Finite Groups
|
|
Residuated Lattices
|
|
The Resolution Calculus for First-Order Logic
|
|
The Z Property
|
|
Ribbon Proofs
|
|
A Complete Proof of the Robbins Conjecture
|
|
Root-Balanced Tree
|
|
Routing
|
|
Transitive closure according to Roy-Floyd-Warshall
|
|
Formal Verification of Modern SAT Solvers
|
|
The Incompatibility of SD-Efficiency and SD-Strategy-Proofness
|
|
Secure information flow and program logics
|
|
A Formalization of Assumptions and Guarantees for Compositional Noninterference
|
|
A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor
|
|
Safe OCL
|
|
A Comprehensive Framework for Saturation Theorem Proving
|
|
Secondary Sylow Theorems
|
|
Developing Security Protocols by Refinement
|
|
Verification of Selection and Heap Sort Using Locales
|
|
Some classical results in Social Choice Theory
|
|
Separata: Isabelle tactics for Separation Algebra
|
|
Separation Algebra
|
|
A Separation Logic Framework for Imperative HOL
|
|
Invertibility in Sequent Calculi
|
|
Shivers' Control Flow Analysis
|
|
An Axiomatic Characterization of the Single-Source Shortest Path Problem
|
|
Haskell's Show Class in Isabelle/HOL
|
|
Sigma Protocols and Commitment Schemes
|
|
Signature-Based Gröbner Basis Algorithms
|
|
A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment
|
|
Simple Firewall
|
|
An Incremental Simplex Algorithm with Unsatisfiable Core Generation
|
|
Skew Heap
|
|
Skip Lists
|
|
Towards Certified Slicing
|
|
Formalization of an Algorithm for Greedily Computing Associative Aggregations on Sliding Windows
|
|
Smooth Manifolds
|
|
Sound and Complete Sort Encodings for First-Order Logic
|
|
Source Coding Theorem
|
|
Real-Valued Special Functions: Upper and Lower Bounds
|
|
Splay Tree
|
|
Computing N-th Roots using the Babylonian Method
|
|
Stable Matching
|
|
Formalizing Statecharts using Hierarchical Automata
|
|
Stellar Quorum Systems
|
|
The Stern-Brocot Tree
|
|
Stewart's Theorem and Apollonius' Theorem
|
|
Stirling's formula
|
|
Stochastic Matrices and the Perron-Frobenius Theorem
|
|
Stone Algebras
|
|
Stone-Kleene Relation Algebras
|
|
Stone Relation Algebras
|
|
A Reduction Theorem for Store Buffers
|
|
Stream Fusion
|
|
Stream Fusion in HOL with Code Generation
|
|
A Formalization of Strong Security
|
|
Sturm's Theorem
|
|
The Sturm-Tarski Theorem
|
|
Stuttering Equivalence
|
|
Subresultants
|
|
A Hierarchy of Algebras for Boolean Subsets
|
|
Sums of Two and Four Squares
|
|
A Variant of the Superposition Calculus
|
|
Surprise Paradox
|
|
Symmetric Polynomials
|
|
Szpilrajn Extension Theorem
|
|
A Formal Development of a Polychronous Polytimed Coordination Language
|
|
A Definitional Encoding of TLA* in Isabelle/HOL
|
|
A General Method for the Proof of Theorems on Tail-recursive Functions
|
|
The independence of Tarski's Euclidean axiom
|
|
Taylor Models
|
|
Timed Automata
|
|
Topology
|
|
The Tortoise and Hare Algorithm
|
|
The Transcendence of Certain Infinite Series
|
|
Transformer Semantics
|
|
Transition Systems and Automata
|
|
Executable Transitive Closures
|
|
Executable Transitive Closures of Finite Relations
|
|
Treaps
|
|
Tree Automata
|
|
Tree Decomposition
|
|
Basic Geometric Properties of Triangles
|
|
Trie
|
|
The Twelvefold Way
|
|
Type Constructor Classes and Monad Transformers
|
|
Types, Tableaus and Gödel’s God in Isabelle/HOL
|
|
The Unified Policy Framework (UPF)
|
|
Formal Network Models and Their Application to Firewall Policies
|
|
Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming
|
|
Universal Turing Machine
|
|
Verification of the UpDown Scheme
|
|
Fundamental Properties of Valuation Theory and Hensel's Lemma
|
|
Vector Spaces
|
|
A Generic Framework for Verified Compilers
|
|
A Mechanically Verified, Efficient, Sound and Complete Theorem Prover For First Order Logic
|
|
VerifyThis 2018 - Polished Isabelle Solutions
|
|
VerifyThis 2019 -- Polished Isabelle Solutions
|
|
VCG - Combinatorial Vickrey-Clarke-Groves Auctions
|
|
A Correctness Proof for the Volpano/Smith Security Typing System
|
|
A Formalization of Declassification with WHAT-and-WHERE-Security
|
|
Strong Eventual Consistency of the Collaborative Editing Framework WOOT
|
|
WebAssembly
|
|
Weight-Balanced Trees
|
|
Well-Quasi-Orders
|
|
Evaluate Winding Numbers through Cauchy Indices
|
|
Finite Machine Word Library
|
|
The Worker/Wrapper Transformation
|
|
XML
|
|
Zermelo Fraenkel Set Theory in Higher-Order Logic
|
|
The Irrationality of ζ(3)
|
|
The Hurwitz and Riemann ζ Functions
|
|
pGCL for Isabelle
|
|
Archive of Formal Proofs
|
|
Search the Archive
Use Google to search the archive. It will look in entry descriptions as well as in the Isabelle theories and PDF proof documents.
Google may take some time to index new pages. Very new Submissions might be missed. |
|
Statistics
|
|
Submission Guidelines
|
|
Index by Topic
|
|
Updating Entries
|
|
Referring to AFP Entries
|