The journal encourages submission of papers describing significant, automated or semi-automated formalization efforts in any area, including classical mathematics, constructive mathematics, formal algorithms, and program verification. The emphasis of the journal is on proof techniques and methodologies and their impact on the formalization process.
In particular, the journal provides a forum for comparing alternative approaches, enhancing reusability of solutions and offering a clear view of the current state of the field.
ISSN: 1972-5787
Vol 2, No 1 (2009)
Table of Contents
Articles
| Formalization of the Integral Calculus in the PVS Theorem Prover |
Abstract
PDF
|
|
Ricky Wayne Butler |
1 - 26 |
| Computing with Classical Real Numbers |
Abstract
PDF
|
|
Cezary Kaliszyk, Russell O'Connor |
27-39 |
| A New Look at Generalized Rewriting in Type Theory |
Abstract
PDF
|
|
Matthieu Sozeau |
41-62 |
| A formalized proof of Dirichlet's theorem on primes in arithmetic progression |
Abstract
PDF
|
|
John Harrison |
63-83 |
©
Copyright 2007 - This journal is maintained by
CIB
Centro Inter-Bibliotecario. Legal registration pending
