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 4, No 1 (2011)
Table of Contents
Articles
| A Formal Proof Of The Riesz Representation Theorem |
PDF
|
|
Anthony Narkawicz |
1-24 |
| Initial Semantics for higher-order typed syntax in Coq |
PDF
|
|
Benedikt Ahrens, Julianna Zsido |
25-69 |
| Formalizing a Proof that e is Transcendental |
PDF
|
|
Jesse Bingham |
71-84 |
| A Proof-Theoretic Account of Primitive Recursion and Primitive Iteration |
PDF
|
|
Luca Chiarabini, Olivier Danvy |
85-109 |
©
Copyright 2011 - Legal registration pending
