[FOM] MSCS special issue on formally verified mathematics

Jeremy Avigad avigad at cmu.edu
Tue Jan 26 04:04:18 EST 2010


Mathematical Structures in Computer Science

Special Issue on

Advances and Perspectives in the Mechanization of Mathematics

Guest Editors: Andrea Asperti and Jeremy Avigad


Call for contributions

Recent advances in automated reasoning and interactive theorem proving 
have made it possible to formalize and mechanically check substantial 
mathematical theorems, such as the prime number theorem, the four color 
theorem, and the Jordan curve theorem. In particular, a number of 
interactive proof assistants have been developed to help users manage 
libraries of definitions and theorems, and fill in the inferential 
details of a mathematical argument. Automated methods are also often 
used to verify calculations that are too long and complex to check by 
hand. As mathematical proofs become more complicated and, increasingly, 
rely on extensive calculation, this gives rise to an exciting 
interaction between traditional methods and computational means of 
verifying mathematical claims.

The present issue is devoted to recent advances and new perspectives in 
this field, including descriptions of formalizations, thoughtful 
reflection on the future of the discipline, novel insights, innovative 
research directions, and critical assessments of the current state of 
the art.


Deadlines

Deadline for submissions: June 28, 2010
Author's notification: September 27, 2010


Submissions:

All papers should be written in pdf and submitted via the EasyChair 
system, accessible at the following address: 
https://www.easychair.org/login.cgi?conf=mscsadvancesandperspectivesint

Authors are invited to write their papers following the mscs 
instructions available in the MSCS guide for contributors downloadable 
here: http://assets.cambridge.org/MSC/MSC_ifc.pdf.

Extended versions of work previously published in conference proceedings 
are eligible for submission but authors should make it clear how their 
submission improves upon the conference publication; in those cases 
where Cambridge University Press is not the publisher of the original 
conference proceedings, authors should take care to avoid infringing 
that publisher's copyright. Authors who wish to discuss potential 
submissions are encouraged to contact the guest editors.

Papers should not be longer than 35 pages; shorter papers are obviously 
welcome.

------------------------------------------------------------
All information can be found at the following web page:
http://www.cs.unibo.it/~asperti/mscs


-- Andrea Asperti & Jeremy Avigad


More information about the FOM mailing list