Fwd: [[Agda] MCS: Formal Proofs for Mathematics and Computer Science [Call for Papers]]

[Dan Licata]

----- Forwarded message from Laurent Th�ry <Lauren...@inria.fr> -----

From: Laurent Th�ry <Lauren...@inria.fr>
To: ag...@lists.chalmers.se
Subject: [Agda] MCS: Formal Proofs for Mathematics and Computer Science
[Call for Papers]
Date: Mon, 06 May 2013 01:48:51 +0200

MCS Special Issue:
Formal Proofs for Mathematics and Computer Science
<http://www-sop.inria.fr/marelle/MCS-FP-2013/>

CALL FOR PAPERS

We invite submission of papers on Proof Formalization
for possible publication in this Mathematics in Computer
Science (MCS) special issue.

Deadlines:

Deadline for paper submission: August 31, 2013
Notification of acceptance/rejection: December 15, 2013
Publication of the special issue: Early 2014

Scope:

In recent years, the use of Interactive Theorem Provers
for the formalization of mathematical proofs has seen
impressive advances:

- In mathematics, the Flyspeck project and the formal
verification of Feit-Thompson theorem indicate that
formal proofs may play an active role in the development
of new mathematics.

- In computer science, the CompCert and L4.verified
projects indicate that non-trivial systems like compilers
and operating systems can be fully verified.

Still, much more progress is needed in order to make
the use of this new technology ubiquitous. The aim of
this special issue is to bring together high quality
contributions which present recent advances in the use
of formal proofs and new perspectives on the technology
of interactive theorem proving.

Submission guidelines:

Papers should be submitted as a pdf. While there is no
strict page limit, papers are expected to be approximately
20 pages long. The LaTeX "mathincs" class should be used,
according to the guidelines at
<http://www.springer.com/birkhauser/mathematics/journal/11786>.
Papers should either be accompanied by a formalization,
a library for an interactive theorem prover, or an
implemented system. Submission is preferably through
EasyChair at
<https://www.easychair.org/conferences/?conf=mcsfp2013>.

Editors of the Special Issue:

Laurent Th�ry, INRIA Sophia Antipolis
email:<Lauren...@inria.fr>

Freek Wiedijk, Radboud University Nijmegen
email:<fr...@cs.ru.nl>

_______________________________________________
Agda mailing list
Ag...@lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda

----- End forwarded message -----

[Andrej Bauer]

Are you suggesting that we take over the special issue? :-)

We could:

1. HoTT library in Coq

2. HoTT library in Agda

3, 4, ..., n: proofs of homotopy-theoretic theorems

On Mon, May 6, 2013 at 7:42 PM, Dan Licata <d...@cs.cmu.edu> wrote:

----- Forwarded message from Laurent Théry <Lauren...@inria.fr> -----

  Laurent Théry, INRIA Sophia Antipolis

  email:<Lauren...@inria.fr>

  Freek Wiedijk, Radboud University Nijmegen
  email:<fr...@cs.ru.nl>

_______________________________________________
Agda mailing list
Ag...@lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda

----- End forwarded message -----

--
You received this message because you are subscribed to the Google Groups "IAS Univalent Foundations" group.
To unsubscribe from this group and stop receiving emails from it, send an email to univalent-founda...@googlegroups.com.
To post to this group, send email to univalent-...@googlegroups.com.
Visit this group at http://groups.google.com/group/univalent-foundations?hl=en.
For more options, visit https://groups.google.com/groups/opt_out.

[Peter LeFanu Lumsdaine]

On Tue, May 7, 2013 at 4:12 AM, Andrej Bauer <andrej...@andrej.com> wrote:

Are you suggesting that we take over the special issue? :-)

No, I think *you* are suggesting that :-) 

I agree, though, that this could be a great venue for submitting at least a write-up of the HoTT library/libraries.  Before the end of term, we discussed fixing a schedule for a stable version of the HoTT Coq library; and their submission deadline, Aug 31, seems perhaps quite well-placed to aim our schedule at?  (Do a few of the main contributors have good time for this over the next few months?  I think I do, for one.)

–p.

[Andrej Bauer]

I am in.

[Michael Shulman]

I support the idea, but I can't promise to have a lot of time to help,
especially in August.