[Agda] CFP: Certified Programs and Proofs

[Shin-Cheng Mu]

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

                        Kenting, 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 will
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