[TYPES/announce] New conference - Certified Programs and Proofs

[bywang at iis.sinica.edu.tw]

Dear colleagues,

Certified Programs and Proofs (CPP) is a new international conference
dedicated to the development of certified software and proofs. The
conference is intended to be a forum for both theorists and
practitioners to exchange ideas about certification used in computer
science, mathematics, and education.

Please read the manifesto (followed by CFP) for our visions. For more
information, please go to the CPP web site at http://formes.asia/cpp/.

Best regards,

Bow-Yaw

Academia Sinica, INRIA, and Tsinghua University

***********************************************************************

                         CPP Manifesto

In this manifesto, we advocate for the creation of a new international
conference in the area of formal methods and programming languages,
named Certified Programs and Proofs (CPP).  Certification here means
formal, mechanized verification of some sort, preferably with
production of independently checkable certificates. CPP would target
any research promoting formal development of certified software and
proofs, that is:

- the development of certified or certifying programs;
- the development of certified mathematical theories;
- the development of new languages and tools for certified programming;
- new program logics, type systems, and semantics for certified code;
- new automated or interactive tools and provers for certification;
- results assessed by an original open source formal development;
- original teaching material based on a proof assistant.

Software today is still developed without precise specification.
A developer often starts the programming task with a rather informal
specification. After careful engineering, the developer delivers a
program that may not fully satisfy the specification.  Extensive
testing and debugging may shrink the gap between the two, but there is
no assurance that the program accurately follows the specification.
Such inaccuracy may not always be significant, but when a developer
links a large number of such modules together, these ``noises'' may
multiply, leading to a system that nobody can understand and
manage. System software built this way often contains hard-to-find
``zero-day vulnerabilities'' that become easy targets for the
Stuxnet-like attacks. CPP aims to promote the development of new
languages and tools for building certified programs and for making
programming precise.

Certified software consists of an executable program plus a formal
proof that the software is free of bugs with respect to a particular
dependability claim. With certified software, the dependability of a
software system is measured by the actual formal claim that it is able
to certify. Because the claim comes with a mechanized proof, the
dependability can be checked independently and automatically in an
extremely reliable way. The formal dependability claim can range from
making almost no guarantee, to simple type safety property, or all the
way to deep liveness, security, and correctness properties. It
provides a great metric for comparing different techniques and
building steady progress in constructing dependable software.

The conventional wisdom is that certified software will never be
practical because any real software must also rely on the underlying
runtime system which is too low-level and complex to be verifiable. In
recent years, however, there have been many advances in the theory and
engineering of mechanized proof systems applied to verification of
low-level code, including proof-carrying code, certified assembly
programming, local reasoning and separation logic, certified linking
of heterogeneous components, certified protocols, certified garbage
collectors, certified or certifying compilation, and certified
OS-kernels.  CPP intends to be a driving force that would facilitate
the rapid development of this exciting new area, and be a natural
international forum for such work.

The recent development in several areas of modern mathematics requires
mathematical proofs containing enormous computation that cannot be
verified by mathematicians in a whole lifetime. Such development has
puzzled the mathematical community and prompted some of our colleagues
in mathematics and computer science to start developing a new
paradigm, formal mathematics, which requires proofs to be
verified by a reliable theorem prover. As particular examples, such an
effort has been done for the four-color theorem and has started for
the sphere packing problem and the classification of finite groups. We
believe that this emerging paradigm is the beginning of a new era.  No
essential existing theorem in computer science has been considered yet
worth a similar effort, but it could well happen in the very near
future. For example, existing results in security would often benefit
from a formal development allowing to exhibit the essential hypotheses
under which the result really holds. CPP would again be a natural
international forum for this kind of work, either in mathematics or in
computer science, and participate strongly to the emergence of this
paradigm.

On the other hand, there is a recent trend in computer science to
formally prove new results in highly technical subjects such as
computational logic, at least in part. In whichever scientific area,
formal proofs have three major advantages: no assumption can be
missing, as is sometimes the case; the result cannot be disputed by a
wrong counterexample, as it sometimes happens; and more importantly, a
formal development often results in a better understanding of the
proof or program, and hence results in easier and better
implementation. This new trend is becoming strong in computer science
work, but is not recognized yet as it should be by traditional
conferences. CPP would be a natural forum promoting this trend.

There are not many proof assistants around. There should be more,
because progress benefits from competition. On the other hand, there
is much theoretical work that could be implemented in the form of
a proof assistant, but this does not really happen. One reason is that
it is hard to publish a development work, especially when this
requires a long term effort as is the case for a proof assistant. It
is even harder to publish work about libraries which, we know all, are
fundamental to make the success of a proof assistant. CPP would take a
particular attention in publishing, publicizing, and promoting this
kind of work.

Finally, CPP also aims to be a publication arena for innovative
teaching experiences, in computer science or mathematics, using proof
assistants in an essential way. These experiences could be submitted
in an innovative format to be defined.

CPP would be an international conference initially based in
Asia. Formal methods in Asia based on model checking have been boosted
by ATVA. An Asian community in formal methods based on formal proofs
is now emerging, in China, South Korea, Taiwan, and Japan (where the
use of such formal methods is recent despite a strong logical
tradition), but is still very scattered and lacks a forum where
researchers can easily meet on a regular basis. CPP is intended to
nurse such a forum, and help boosting this community in Asia as ATVA
did for the model checking community.

For its start, CPP will join APLAS, to be organized in early December
2011 in Taiwan. Co-locating with APLAS will have the advantage of
having a larger community present for the very first CPP meeting.  In
the long run, we would target a three-year rotating schema among Asia,
Europe, and North America, and favor colocations with other
conferences on each continent.


                         by Jean-Pierre Jouannaud and Zhong Shao
                                   December 15, 2010

***********************************************************************

             The First International Conference on
            Certified Programs and Proofs (CPP 2011)
                 PRELIMINARY CALL FOR PAPERS

                         Taiwan
                   December 7--9, 2011
                  http://formes.asia/cpp

               (co-located with APLAS 2011)


CPP is a new international forum on theoretical and practical topics
in all areas, including computer science, mathematics, and education,
that consider certification as an essential paradigm for their work.
Certification here means formal, mechanized verification of some sort,
preferably with production of independently checkable certificates.
We invite submissions on topics that fit under this rubric.

Suggested, but not exclusive, specific topics of interest for
submissions include: certified or certifying programming, compilation,
linking, OS kernels, runtime systems, and security monitors; program
logics, type systems, and semantics for certified code; certified
decision procedures, mathematical libraries, and mathematical
theorems; proof assistants and proof theory; new languages and tools
for certified programming; program analysis, program verification, and
proof-carrying code; certified secure protocols and transactions;
certificates for decision procedures, including linear algebra,
polynomial systems, SAT, SMT, and unification in algebras of interest;
certificates for semi-decision procedures, including equality,
first-order logic, and higher-order unification; certificates for
program termination; logics for certifying concurrent and distributed
programs; higher-order logics, logical systems, separation logics, and
logics for security; and teaching mathematics and computer science
with proof assistants.

IMPORTANT DATES:

Authors are required to submit a paper title and a short abstract
before submitting the full paper.  The submission should include when
necessary a url where to find the formal development assessing the
essential aspects of the work.  All submissions will be
electronic. All deadlines are at midnight (GMT).

   Abstract Deadline:           Monday, June 13, 2011
   Paper Submission Deadline:   Friday, June 17, 2011
   Author Notification:         Monday, August 29, 2011
   Camera Ready:                Monday, September 19, 2011
   Conference:                  December 7-9, 2011

SUBMISSION INSTRUCTIONS:

Papers should be submitted electronically online via the conference
submission web page at URL:

http://www.easychair.org/conferences/?conf=cpp2011

Acceptable formats are PostScript or PDF, viewable by Ghostview or
Acrobat Reader. Submissions should not exceed 16 pages in LNCS format,
including bibliography and figures.  Submitted papers will be judged
on the basis of significance, relevance, correctness, originality, and
clarity. They should clearly identify what has been accomplished and
why it is significant. The proceedings of the symposium is planned to
be published as a volume in Springer-Verlag's Lecture Notes in
Computer Science series. Submission instructions including Latex
style files are available from the CPP 2011 website.

Each submission must be written in English and provide sufficient
detail to allow the program committee to assess the merits of the
paper.  It should begin with a succinct statement of the issues, a
summary of the main results, and a brief explanation of their
significance and relevance to the conference, all phrased for the
non-specialist.  Technical and formal developments directed to the
specialist should follow.  Whenever appropriate, the submission should
come along with a formal development, using whatever prover, e.g.,
Agda, Coq, Elf, HOL, HOL-Light, Isabelle, Matita, Mizar, NQTHM, PVS,
Vampire, etc. References and comparisons with related work should be
included.  Papers not conforming to the above requirements concerning
format and length may be rejected without further consideration.

The results must be unpublished and not submitted for publication
elsewhere, including the proceedings of other published conferences or
workshops.  The PC chairs should be informed of closely related work
submitted to a conference or journal in advance of
submission. Original formal proofs of known results in mathematics or
computer science are among the targets.  One author of each accepted
paper is expected to present it at the conference.


AWARD FOR BEST PAPER:

An award will be given for the best accepted paper, as judged by the
program committee.  Details concerning eligibility criteria and
procedure for consideration for this award will be posted at the CPP
website.  The committee may decline to make the award or split it
among several papers.


PROGRAM CO-CHAIRS:
  Jean-Pierre Jouannaud   (INRIA and Tsinghua University)
  Zhong Shao              (Yale University)
  Email: cpp2011pc at gmail.com

GENERAL CHAIR:
  Yih-Kuen Tsay           (National Taiwan University)

PROGRAM COMMITTEE:

  Andrea Asperti          (University of Bologna)
  Gilles Barthe           (IMDEA Software Institute)
  Xiao-Shan Gao           (Chinese Academy of Sciences)
  Georges Gonthier        (Microsoft Research Cambridge)
  Chris Hawblitzel        (Microsoft Research Redmond)
  John Harrison           (Intel Corporation)
  Jean-Pierre Jouannaud   (INRIA and Tsinghua University)
  Akash Lal               (Microsoft Research India)
  Xavier Leroy            (INRIA Paris-Rocquencourt)
  Yasuhiko Minamide       (University of Tsukuba)
  Shin-Cheng Mu           (Academia Sinica)
  Michael Norrish         (NICTA)
  Brigitte Pientka        (McGill University)
  Sandip Ray              (University of Texas at Austin)
  Natarajan Shankar       (SRI International)
  Zhong Shao              (Yale University)
  Christian Urban         (TU Munich)
  Viktor Vafeiadis        (Max Planck Institute for Software Systems)
  Stephanie Weirich       (University of Pennsylvania)
  Kwangkeun Yi            (Seoul National University)

PUBLICITY CHAIR:
  Bow-Yaw Wang            (Academia Sinica, INRIA and Tsinhua University)

ORGANIZING COMMITTEE:
  Tyng-Ruey Chuang (chair), Shin-Cheng Mu, Yih-Kuen Tsay
                          (Academia Sinica and National Taiwan University)
  Email: cpp2011oc at gmail.com


----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.