-
Journal of Formalized Reasoning Vol. 13 No. 1 (2020) - Articles
C floating-point proofs layered with VST and Flocq
Abstract PDF -
Journal of Formalized Reasoning Vol. 11 No. 1 (2018) - Articles
Formalization Techniques for Asymptotic Reasoning in Classical Analysis
Abstract PDF -
Journal of Formalized Reasoning Vol. 11 No. 1 (2018) - Articles
A Decision Procedure for Univariate Polynomial Systems Based on Root Counting and Interval Subdivision
Abstract PDF -
Journal of Formalized Reasoning Vol. 12 No. 1 (2019) - Articles
Commutativity Theorems in Groups with Power-like Maps
Abstract PDF -
Journal of Formalized Reasoning Vol. 12 No. 1 (2019) - Articles
A Why3 proof of GMP algorithms
Abstract PDF -
Journal of Formalized Reasoning Vol. 12 No. 1 (2019) - Articles
LF+ in Coq for "fast and loose" reasoning
Abstract PDF -
Journal of Formalized Reasoning Vol. 13 No. 1 (2020) - Errata
Corrigendum: C floating-point proofs layered with VST and Flocq
Abstract PDF -
Journal of Formalized Reasoning Vol. 10 No. 1 (2017) - Articles
Formal Proof of Banach-Tarski Paradox
Abstract PDF -
Journal of Formalized Reasoning Vol. 10 No. 1 (2017) - Articles
A Library for Algorithmic Game Theory in Ssreflect/Coq
Abstract PDF -
Journal of Formalized Reasoning Vol. 11 No. 1 (2018) - Articles
Dependent Types for Extensive Games
Abstract PDF -
Journal of Formalized Reasoning Vol. 9 No. 1 (2016): Special Issue: Twenty Years of the QED Manifesto - QED 20th anniversary
Formalizing Scientifically Applicable Mathematics in a Definitional Framework
Abstract PDF -
Journal of Formalized Reasoning Vol. 2 No. 1 (2009) - Articles
A New Look at Generalized Rewriting in Type Theory
Abstract PDF -
Journal of Formalized Reasoning Vol. 9 No. 1 (2016): Special Issue: Twenty Years of the QED Manifesto - QED 20th anniversary
Proof Auditing Formalised Mathematics
Abstract PDF -
Journal of Formalized Reasoning Vol. 3 No. 1 (2010) - Articles
Sets in Coq, Coq in Sets
Abstract PDF -
Journal of Formalized Reasoning Vol. 3 No. 1 (2010) - Articles
Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure
Abstract PDF -
Journal of Formalized Reasoning Vol. 9 No. 1 (2016): Special Issue: Twenty Years of the QED Manifesto - QED 20th anniversary
Hammering towards QED
Abstract PDF -
Journal of Formalized Reasoning Vol. 3 No. 1 (2010) - Articles
Implementation of Bourbaki's Elements of Mathematics in Coq: Part One, Theory of Sets
Abstract PDF -
Journal of Formalized Reasoning Vol. 4 No. 1 (2011) - Articles
A Formal Proof Of The Riesz Representation Theorem
Abstract PDF -
Journal of Formalized Reasoning Vol. 9 No. 1 (2016): Special Issue: Twenty Years of the QED Manifesto - QED 20th anniversary
Conversion of HOL Light proofs into Metamath
Abstract PDF -
Journal of Formalized Reasoning Vol. 7 No. 2 (2014): Special Issue: User Tutorials 2 - Articles
Abella: A System for Reasoning about Relational Specifications
Abstract PDF -
Journal of Formalized Reasoning Vol. 3 No. 1 (2010) - Articles
Basic first-order model theory in Mizar
Abstract PDF -
Journal of Formalized Reasoning Vol. 3 No. 2 (2010): Special Issue: User Tutorials I - Articles
An Introduction to Programming and Proving with Dependent Types in Coq
Abstract PDF -
Journal of Formalized Reasoning Vol. 3 No. 2 (2010): Special Issue: User Tutorials I - Articles
An introduction to small scale reflection in Coq
Abstract PDF -
Journal of Formalized Reasoning Vol. 3 No. 2 (2010): Special Issue: User Tutorials I - Articles
Mizar in a Nutshell
Abstract PDF -
Journal of Formalized Reasoning Vol. 7 No. 2 (2014): Special Issue: User Tutorials 2 - Articles
Matita Tutorial
Abstract PDF -
Journal of Formalized Reasoning Vol. 4 No. 1 (2011) - Articles
Initial Semantics for higher-order typed syntax in Coq
Abstract PDF -
Journal of Formalized Reasoning Vol. 8 No. 2 (2015): Special Issue - PhD Theses - Ph.D. Thesis
Initiality for Typed Syntax and Semantics
Abstract PDF -
Journal of Formalized Reasoning Vol. 8 No. 1 (2015) - Articles
Verified Representations of Landau's "Grundlagen" in the lambda-delta Family and in the Calculus of Constructions
Abstract PDF -
Journal of Formalized Reasoning Vol. 4 No. 1 (2011) - Articles
A Proof-Theoretic Account of Primitive Recursion and Primitive Iteration
Abstract PDF -
Journal of Formalized Reasoning Vol. 9 No. 2 (2016) - Articles
Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers
Abstract PDF -
Journal of Formalized Reasoning Vol. 4 No. 1 (2011) - Articles
Formalizing a Proof that e is Transcendental
Abstract PDF -
Journal of Formalized Reasoning Vol. 8 No. 1 (2015) - Articles
A formal verification of the theory of parity complexes
Abstract PDF -
Journal of Formalized Reasoning Vol. 5 No. 1 (2012) - Articles
A formal proof of Sasaki-Murao algorithm
Abstract PDF -
Journal of Formalized Reasoning Vol. 5 No. 1 (2012) - Articles
Standardization and Confluence in Pure Lambda-Calculus Formalized for the Matita Theorem Prover
Abstract PDF -
Journal of Formalized Reasoning Vol. 5 No. 1 (2012) - Articles
A proof of Bertrand's postulate
Abstract PDF -
Journal of Formalized Reasoning Vol. 9 No. 2 (2016) - Articles
Formalization of the pumping lemma for context-free languages
Abstract PDF -
Journal of Formalized Reasoning Vol. 6 No. 1 (2013) - Articles
Formal Verification of Language-Based Concurrent Noninterference
Abstract PDF -
Journal of Formalized Reasoning Vol. 9 No. 1 (2016): Special Issue: Twenty Years of the QED Manifesto - QED 20th anniversary
Preface: Twenty Years of the QED Manifesto
Abstract PDF -
Journal of Formalized Reasoning Vol. 6 No. 1 (2013) - Articles
A String of Pearls: Proofs of Fermat's Little Theorem
Abstract PDF -
Journal of Formalized Reasoning Vol. 6 No. 1 (2013) - Articles
Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model
Abstract PDF -
Journal of Formalized Reasoning Vol. 9 No. 2 (2016) - Articles
Lawvere-Tierney sheafification in Homotopy Type Theory
Abstract PDF -
Journal of Formalized Reasoning Vol. 6 No. 1 (2013) - Articles
A Formal Proof of Square Root and Division Elimination in Embedded Programs
Abstract PDF -
Journal of Formalized Reasoning Vol. 10 No. 1 (2017) - Articles
Formalizing Restriction Categories
Abstract PDF -
Journal of Formalized Reasoning Vol. 9 No. 2 (2016) - Articles
Understanding and maintaining tactics graphically OR how we are learning that a diagram can be worth more than 10K LoC
Abstract PDF -
Journal of Formalized Reasoning Vol. 7 No. 1 (2014) - Articles
Certified Kruskal's Tree Theorem
Abstract PDF -
Journal of Formalized Reasoning Vol. 7 No. 1 (2014) - Articles
An Intrinsic Encoding of a Subset of C and its Application to TLS Network Packet Processing
Abstract PDF -
Journal of Formalized Reasoning Vol. 8 No. 1 (2015) - Articles
Formal Proofs for Nonlinear Optimization
Abstract PDF -
Journal of Formalized Reasoning Vol. 10 No. 1 (2017) - Articles
A Formally Proved, Complete Algorithm for Path Resolution with Symbolic Links
Abstract PDF -
Journal of Formalized Reasoning Vol. 7 No. 1 (2014) - Articles
Views of PI: Definition and computation
Abstract PDF -
Journal of Formalized Reasoning Vol. 7 No. 1 (2014) - Articles
Innocuous Double Rounding of Basic Arithmetic Operations
Abstract PDF -
Journal of Formalized Reasoning Vol. 7 No. 1 (2014) - Articles
Relative Monads Formalised
Abstract PDF -
Journal of Formalized Reasoning Vol. 1 No. 1 (2008) - Articles
A Page in Number Theory
Abstract PDF -
Journal of Formalized Reasoning Vol. 1 No. 1 (2008) - Articles
Genetic Algorithms in Coq: Generalization and Formalization of the crossover operator
Abstract PDF -
Journal of Formalized Reasoning Vol. 9 No. 1 (2016): Special Issue: Twenty Years of the QED Manifesto - QED 20th anniversary
Mixing Computations and Proofs
Abstract PDF -
Journal of Formalized Reasoning Vol. 9 No. 1 (2016): Special Issue: Twenty Years of the QED Manifesto - QED 20th anniversary
Now f is continuous (exercise!)
Abstract PDF -
Journal of Formalized Reasoning Vol. 9 No. 1 (2016): Special Issue: Twenty Years of the QED Manifesto - QED 20th anniversary
Theorema 2.0: Computer-Assisted Natural-Style Mathematics
Abstract PDF -
Journal of Formalized Reasoning Vol. 1 No. 1 (2008) - Articles
A constructive and formal proof of Lebesgue’s Dominated Convergence Theorem in the interactive theorem prover Matita
Abstract PDF -
Journal of Formalized Reasoning Vol. 1 No. 1 (2008) - Articles
A Formalization of Newman's and Yokouchi's Lemmas in a Higher-Order Language
Abstract PDF -
Journal of Formalized Reasoning Vol. 9 No. 1 (2016): Special Issue: Twenty Years of the QED Manifesto - QED 20th anniversary
Mathematical Text Processing in EA-style: a Sequent Aspect
Abstract PDF -
Journal of Formalized Reasoning Vol. 2 No. 1 (2009) - Articles
Formalization of the Integral Calculus in the PVS Theorem Prover
Abstract PDF -
Journal of Formalized Reasoning Vol. 8 No. 1 (2015) - Articles
Programming type-safe transformations using higher-order abstract syntax
Abstract PDF -
Journal of Formalized Reasoning Vol. 9 No. 1 (2016): Special Issue: Twenty Years of the QED Manifesto - QED 20th anniversary
QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge
Abstract PDF -
Journal of Formalized Reasoning Vol. 2 No. 1 (2009) - Articles
Computing with Classical Real Numbers
Abstract PDF -
Journal of Formalized Reasoning Vol. 2 No. 1 (2009) - Articles
A formalized proof of Dirichlet's theorem on primes in arithmetic progression
Abstract PDF