Special issue on Programming Languages and Mechanized Mathematics Systems
Journal of Automated Reasoning


This special issue is focused on the intersection of programming languages (PL) and mechanized mathematics systems (MMS). The latter category subsumes present-day computer algebra systems (CAS), interactive proof assistants (PA), and automated theorem provers (ATP), all heading towards fully integrated mechanized mathematical assistants that are expected to emerge eventually.

The two subjects of PL and MMS meet in many interesting ways, in particular in the following main topics of this journal issue.

These topics have been addressed in the PLMMS 2007 and PLMMS 2008 workshops (associated with Calculemus). While the journal issue emerges from that community, submission is open to everyone interested in any of these topics!


Manuscripts should not have been previously published in archival journals nor have been submitted to, or be in consideration for, any journal or conference. Significantly revised and enhanced papers published in workshop or conference proceedings are welcome. All submissions will be reviewed according to scholarly standards for scientific journal publications. See also the general JAR submission policies.

We suggest a page limit of approximately 25 pages, using the LaTeX macros provided by Springer. Instead of using the Springer online submission system, please submit papers in PDF through EasyChair.

Important dates

Editors of the special issue