default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDArchive of Formal Proofs, Volume 2016
Volume 2016, 2016
- Lukas Bulwahn:
Cardinality of Number Partitions. - T. V. H. Prathamesh:
Tensor Product of Matrices. - T. V. H. Prathamesh:
Knot Theory. - Sebastian Ullrich, Denis Lohner:
Verified Construction of Static Single Assignment Form. - René Thiemann, Akihisa Yamada:
Polynomial Factorization. - René Thiemann, Akihisa Yamada:
Polynomial Interpolation. - Maximilian P. L. Haslbeck, Tobias Nipkow:
Analysis of List Update Algorithms. - Salomon Sickert:
Linear Temporal Logic. - Simon Wimmer:
Timed Automata. - Lawrence C. Paulson:
The Cartan Fixed Point Theorems. - Nicolas Peltier:
Propositional Resolution and Prime Implicates Generation. - Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth, Tjark Weber:
Kleene Algebras with Domain. - Pasquale Noce:
Conservation of CSP Noninterference Security under Sequential Composition. - Julius Michaelis, Max W. Haslbeck, Peter Lammich, Lars Hupel:
Algorithms for Reduced Ordered Binary Decision Diagrams. - Maksym Bortin:
A formalisation of the Cocke-Younger-Kasami algorithm. - Mike Stannett, István Németi:
No Faster-Than-Light Observers. - Fabian Immler, Alexander Maletzky:
Gröbner Bases Theory. - Manuel Eberl:
The Incompatibility of SD-Efficiency and SD-Strategy-Proofness. - Lukas Bulwahn:
Spivey's Generalized Recurrence for Bell Numbers. - Manuel Eberl:
Randomised Social Choice Theory. - Andreas Lochbihler:
A Formal Proof of the Max-Flow Min-Cut Theorem for Countable Networks. - Benjamin Bisping, Paul-David Brodmann, Tim Jungnickel, Christina Rickmann, Henning Seidler, Anke Stüber, Arno Wilhelm-Weidner, Kirstin Peters, Uwe Nestmann:
A Constructive Proof for FLP. - Joachim Breitner, Denis Lohner:
The meta theory of the Incredible Proof Machine. - Jose Divasón, Ondrej Kuncar, René Thiemann, Akihisa Yamada:
Perron-Frobenius Theorem for Spectral Radius Analysis. - Fahad Ausaf, Roy Dyckhoff, Christian Urban:
POSIX Lexing with Derivatives of Regular Expressions. - Lukas Bulwahn:
Cardinality of Equivalence Relations. - Christoph Dittmann:
Tree Decomposition. - Joel Beeren, Matthew Fernandez, Xin Gao, Gerwin Klein, Rafal Kolanski, Japheth Lim, Corey Lewis, Daniel Matichuk, Thomas Sewell:
Finite Machine Word Library. - Pasquale Noce:
Conservation of CSP Noninterference Security under Concurrent Composition. - Victor B. F. Gomes, Georg Struth:
Program Construction and Verification Components Based on Kleene Algebra. - Toby C. Murray, Robert Sison, Edward Pierzchalski, Christine Rizkallah:
A Dependent Security Type System for Concurrent Imperative Programs. - Lukas Bulwahn:
Cardinality of Multisets. - Eugene W. Stark:
Category Theory with Adjunctions and Limits. - Toby C. Murray, Robert Sison, Edward Pierzchalski, Christine Rizkallah:
Compositional Security-Preserving Refinement for Concurrent Imperative Programs. - Cornelius Diekmann, Julius Michaelis, Lars Hupel:
IP Addresses. - Anders Schlichtkrull:
The Resolution Calculus for First-Order Logic. - Bertram Felgenhauer, Julian Nagele, Vincent van Oostrom, Christian Sternagel:
The Z Property. - Jeremy Sylvestre:
Chamber Complexes, Coxeter Systems, and Buildings. - Peter Lammich, René Neumann:
A Framework for Verifying Depth-First Search Algorithms. - Joachim Breitner:
Surprise Paradox. - Lukas Bulwahn:
Ptolemy's Theorem. - Peter Lammich:
The Imperative Refinement Framework. - Peter Lammich, S. Reza Sefidgar:
Formalizing the Edmonds-Karp Algorithm. - Romain Aïssat, Frédéric Voisin, Burkhart Wolff:
Infeasible Paths Elimination by Symbolic Execution Techniques: Proof of Correctness and Preservation of Paths. - Cornelius Diekmann, Julius Michaelis, Max W. Haslbeck:
Simple Firewall. - Julius Michaelis, Cornelius Diekmann:
Routing. - Nicolas Peltier:
A Variant of the Superposition Calculus. - Walter Guttmann:
Stone Algebras. - Cornelius Diekmann, Lars Hupel:
Iptables_Semantics. - Fadoua Ghourabi:
Allen's Interval Calculus. - Lukas Bulwahn:
Intersecting Chords Theorem. - Zhe Hou
, David Sanán, Alwen Tiu, Yang Liu:
A formal model for the SPARCv8 ISA and a proof of non-interference for the LEON3 processor. - Quentin Hibon, Lawrence C. Paulson:
Source Coding Theorem. - Julius Michaelis, Cornelius Diekmann:
LOFT - Verified Migration of Linux Firewalls to SDN. - Peter Gammie:
Stable Matching. - Tjark Weber, Lars-Henrik Eriksson, Joachim Parrow, Johannes Borgström, Ramunas Gutkovas:
Modal Logics for Nominal Transition Systems. - Alexander Bentkamp:
Expressiveness of Deep Learning. - Zhe Hou, David Sanán, Alwen Tiu, Rajeev Goré, Ranald Clouston:
Separata: Isabelle tactics for Separation Algebra. - Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah, Joseph Tuong:
COMPLX: A Verification Framework for Concurrent Imperative Programs. - Anders Schlichtkrull, Jørgen Villadsen:
Paraconsistency. - Manuel Eberl:
Catalan Numbers. - Hauke Brinkop, Tobias Nipkow:
Pairing Heap. - Manuel Eberl:
Stirling's formula. - Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand:
Formalization of Recursive Path Orders for Lambda-Free Higher-Order Terms. - Manuel Eberl:
Fisher-Yates shuffle. - Sebastien Gouezel:
Lp spaces. - Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann, Akihisa Yamada:
The Factorization Algorithm of Berlekamp and Zassenhaus. - Jasmin Christian Blanchette, Mathias Fleury, Dmitriy Traytel:
Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals. - Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand:
Formalization of Knuth-Bendix Orders for Lambda-Free Higher-Order Terms. - Tobias Nipkow:
Abstract Interpretation of Annotated Commands. - Yutaka Nagashima:
Proof Strategy Language. - Lukas Bulwahn:
The Twelvefold Way. - Julian Fell, Ian J. Hayes, Andrius Velykis:
Concurrent Refinement Algebra and Rely Quotients.
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.
last updated on 2025-03-01 15:02 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
