![](https://dblp.uni-trier.de/img/logo.ua.320x120.png)
![](https://dblp.uni-trier.de/img/dropdown.dark.16x16.png)
![](https://dblp.uni-trier.de/img/peace.dark.16x16.png)
Остановите войну!
for scientists:
![search dblp search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de/img/search.dark.16x16.png)
default search action
Archive of Formal Proofs, Volume 2019
Volume 2019, 2019
- Ernie Cohen, Norbert Schirmer:
A Reduction Theorem for Store Buffers. - Lars Hupel:
An Algebra for Higher-Order Terms. - Peter Lammich, Simon Wimmer:
IMP2 - Simple Program Verification in Isabelle/HOL. - Ralph Bottesch, Max W. Haslbeck, René Thiemann:
Farkas' Lemma and Motzkin's Transposition Theorem. - Manuel Eberl:
The Inversions of a List. - Simon Foster
, Frank Zeyda, Yakoub Nemouchi
, Pedro Ribeiro, Burkhart Wolff:
Isabelle/UTP: Mechanised Theory Engineering for Unifying Theories of Programming. - Jian Xu, Xingyuan Zhang, Christian Urban, Sebastiaan J. C. Joosten:
Universal Turing Machine. - Daniel Stüwe, Manuel Eberl:
Probabilistic Primality Testing. - Maximilian P. L. Haslbeck, Peter Lammich, Julian Biendarra:
Kruskal's Algorithm for Minimum Spanning Forest. - Manuel Eberl:
Elementary Facts About the Distribution of Primes. - Denis A. Nikiforov:
Safe OCL. - Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, Naijun Zhan:
Quantum Hoare Logic. - Angeliki Koutsoukou-Argyraki, Wenda Li:
The Transcendence of Certain Infinite Series. - Lorenzo Gheri, Andrei Popescu:
A General Theory of Syntax with Bindings. - Safouan Taha, Lina Ye, Burkhart Wolff:
HOL-CSP Version 2.0. - David Aspinall, David Butler:
Multi-Party Computation. - Matthias Brun, Dmitriy Traytel:
Formalization of Generic Authenticated Data Structures. - Benedikt Seidl, Salomon Sickert:
A Compositional and Unified Translation of LTL into ω-Automata. - Martin Rau:
Multidimensional Binary Search Trees. - André Platzer:
Differential Game Logic. - Simon Griebel:
Binary Heaps for IMP2. - Alexander Maletzky:
Gröbner Bases, Macaulay Matrices and Dubé's Degree Bounds. - Alexander Maletzky:
Hilbert's Nullstellensatz. - Ralph Bottesch, Alban Reynaud, René Thiemann:
Linear Inequalities. - Peter Lammich, Tobias Nipkow:
Purely Functional, Simple, and Efficient Implementation of Prim and Dijkstra. - Peter Lammich, Tobias Nipkow:
Priority Search Trees. - Akihisa Yamada, Jérémy Dubut:
Complete Non-Orders and Fixed Points. - Joshua Schneider, Dmitriy Traytel:
Formalization of a Monitoring Algorithm for Metric First-Order Temporal Logic. - Lars Hupel:
A Verified Code Generator from Isabelle/HOL to CakeML. - Asta Halkjær From:
A Sequent Calculus for First-Order Logic. - Peter Zeller:
Szpilrajn Extension Theorem. - Hai Nguyen Van, Frédéric Boulanger, Burkhart Wolff:
A Formal Development of a Polychronous Polytimed Coordination Language. - Giuliano Losa:
Stellar Quorum Systems. - Manuel Eberl:
Selected Problems from the International Mathematical Olympiad 2019. - Maxime Buyse, Jason Jaskolka:
Communicating Concurrent Kleene Algebra for Distributed Systems Specification. - Fabian Immler:
Laplace Transform. - Robert Sachtleben:
Formalisation of an Adaptive State Counting Algorithm. - Clemens Ballarin:
A Case Study in Basic Algebra. - Julian Parsert, Cezary Kaliszyk:
Linear Programming. - Lawrence C. Paulson:
Fourier Series. - Jonathan Julián Huerta y Munive:
Verification Components for Hybrid Systems. - Thibault Dardinier:
Formalization of Multiway-Join Algorithms. - Frédéric Tuong, Burkhart Wolff:
Clean - An Abstract Imperative Programming Language and its Theory. - David Butler, Andreas Lochbihler:
Sigma Protocols and Commitment Schemes. - Angeliki Koutsoukou-Argyraki:
Aristotle's Assertoric Syllogistic. - Peter Lammich, Simon Wimmer:
VerifyThis 2019 - Polished Isabelle Solutions. - Lawrence C. Paulson:
Zermelo Fraenkel Set Theory in Higher-Order Logic. - Rose Bohrer:
Interval Arithmetic on 32-bit Words. - Frédéric Tuong, Burkhart Wolff:
Isabelle/C. - Pasquale Noce:
An Efficient Generalization of Counting Sort for Large, possibly Infinite Key Ranges. - Fabian Immler, Yong Kiam Tan:
The Poincaré-Bendixson Theorem. - Manuel Eberl:
The Irrationality of ζ(3). - Rodrigo Raya, Manuel Eberl:
Gauss Sums and the Pólya-Vinogradov Inequality. - Filip Maric, Danijela Simic:
Complex Geometry. - Danijela Simic, Filip Maric, Pierre Boutry:
Poincaré Disc Model. - Asta Halkjær From:
Formalizing a Seligman-Style Tableau System for Hybrid Logic.
![](https://dblp.uni-trier.de/img/cog.dark.24x24.png)
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.