[TYPES/announce] Call for Papers: Certified Programs and Proofs (CPP) 2015

[Alwen Tiu]

The 4th ACM SIGPLAN Conference on
Certified Programs and Proofs (CPP 2015)

Mumbai, India, 12 - 14 January 2015

http://cpp2015.inria.fr

Co-located with POPL 2015 (http://popl.mpi-sws.org/2015/)


Call for Papers
===========

CPP is an 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.

CPP 2015 is the fourth in the CPP conference series and will be co-located
with POPL 2015 in Mumbai from 12 - 14 January 2015.

Important dates
------------------------
Abstract submission:     3 October 2014, anywhere on Earth (11:59 pm,
UTC-12)
Full paper submission:    10 October 2014, anywhere on Earth (11:59 pm,
UTC-12)
Notification:         29 November 2014
Camera-ready deadline:    15 December 2014
Conference dates:    12 - 14 January 2015


Scope
----------
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;
- teaching mathematics and computer science with proof assistants.


Submission instructions
-----------------------------------
Submitted papers should not exceed 12 pages in the ACM SIGPLAN
Proceedings format. Shorter papers are welcome and will be given equal
consideration. The proceedings of the conference will be published
by the ACM. Templates for ACM SIGPLAN format can be found on the
ACM SIGPLAN website:

http://www.sigplan.org/Resources/Author.

Papers should be submitted in PDF format, through the EasyChair
submission page:

https://www.easychair.org/conferences/?conf=cpp2015

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.


Program Committee
-----------------------------
Andreas Abel, Chalmers and Gothenburg University, Sweden
June Andronick, NICTA and UNSW, Sydney, Australia
Nick Benton, Microsoft Research, Cambridge, UK
Lennart Beringer, Princeton University, USA
James Brotherston. University College London, UK
Kaustuv Chaudhuri, Inria, Saclay, France
Amy Felty, University of Ottawa, Canada
Chung-Kil Hur , Seoul National University, Korea
Naoki Kobayashi, University of Tokyo, Japan
Xavier Leroy (co-chair), Inria, Paris-Rocquencourt, France
Leonardo de Moura , Microsoft Research, Redmond, USA
Magnus Myreen , University of Cambridge, UK
Vivek Nigam, Federal University of Paraíba, Brasil
Tobias Nipkow, Technische Universität München. Germany
Christine Paulin-Mohring, Université Paris-Sud, France
Natarajan Raja, Tata Institute of Fundamental Research, Mumbai, India
Gert Smolka, Saarland University, Germany
Alwen Tiu (co-chair), Nanyang Technological University, Singapore
Stephanie Weirich , University of Pennsylvania, USA
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20140717/d5a6fb84/attachment.html>