[TYPES/announce] 2nd CFP: Certified Programs and Proofs 2016

[Adam Chlipala]

The 5th ACM SIGPLAN Conference on
Certified Programs and Proofs (CPP 2016)
in cooperation with ACM SIGLOG

Saint Petersburg, Florida, USA
January 18-19, 2016

http://people.csail.mit.edu/adamc/cpp16/
Co-located with POPL 2016 (http://conf.researchr.org/home/POPL-2016)

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 2016 is the fifth in the CPP conference series and will be co-located
with POPL 2016 in Saint Petersburg, Florida from 18-19 January 2016.

Important dates
---------------

Abstract submission:    7 October 2015, anywhere on Earth (11:59 pm, UTC-12)
Full paper submission: 12 October 2015, anywhere on Earth (11:59 pm, UTC-12)
Notification:          18 November 2015
Final versions due:     4 December 2015
Conference dates:   18-19 January 2016

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=cpp2016

Abstracts must be submitted by the deadline given above.
The deadline for full papers falls one week later, and authors
have the option to withdraw their papers during the window between the
two.

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. If the submission reports on a
computer-checked formalization, code, or the results of a computation,
a link to the relevant data should be provided. 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.

AUTHORS TAKE NOTE: The official publication date is the date the
proceedings are made available in the ACM Digital Library. This date
may be up to two weeks prior to the first day of your conference. The
official publication date affects the deadline for any patent filings
related to published work. (For those rare conferences whose
proceedings are published in the ACM Digital Library after the
conference is over, the official publication date remains the first
day of the conference.)

Program Committee
-----------------

Jeremy Avigad (co-chair), Carnegie Mellon University, US
Sandrine Blazy, Université de Rennes 1, France
Adam Chlipala (co-chair), Massachusetts Institute of Technology, US
Thierry Coquand, Chalmers University of Technology, Sweden
John Harrison, Intel, US
Chris Hawblitzel, Microsoft Research, Redmond, US
Cătălin Hriţcu, INRIA Paris-Rocquencourt, France
Brian Huffman, Galois, Inc., US
Laura Kovács, Chalmers University of Technology, Sweden
Peter Lammich, Technische Universität München, Germany
Hongjin Liang, University of Science and Technology of China, China
Dan Licata, Wesleyan University, US
Panagiotis Manolios, Northeastern University, US
Dale Miller, INRIA Saclay and LIX, France
Dominic Mulligan, Cambridge University, UK
Lawrence Paulson, Cambridge University, UK
Andrei Popescu, Middlesex University London, UK
Claudio Sacerdoti Coen, University of Bologna, Italy
Zachary Tatlock, University of Washington, US
Cesare Tinelli, University of Iowa, US