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.
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.