CPP 2017: The 6th ACM SIGPLAN Conference on Certified Programs and Proofs
Paris, France, January 16 - 17, 2017 (co-located with POPL'17)
http://cpp2017.mpi-sws.org/
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.
We welcome submissions in research areas related to formal certification of
programs and proofs. The following is a suggested list of topics of interests
to CPP. This is a non-exhaustive list and should be read as a guideline rather
than a requirement.
- 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 guidelines
Papers should be submitted in PDF format through the EasyChair submission page
at
https://easychair.org/conferences/?conf=cpp2017.
Submitted papers must be formatted following the ACM SIGPLAN Proceedings format
(seehttp://www.sigplan.org/Resources/Author/) using **10 point** font for the
main text (not the default 9pt font).
Papers should should not exceed **12 pages** including all tables, figures, and
bibliography. Shorter papers are very welcome and will be given equal
consideration.
Abstracts must be submitted by October 5, 2016 (AOE). The deadline for full
papers is October 12, 2016 (AOE), and authors have the option to withdraw their
papers during the window between the two.
Submissions must be written in English and provide sufficient detail to allow
the program committee to assess the merits of the paper. They 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. 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.
Whenever appropriate, the submission should come along with a formal
development, using whatever prover, e.g., Agda, Coq, Dafny, Elf, HOL,
HOL-Light, Isabelle, Lean, Matita, Mizar, NQTHM, PVS, Vampire, etc. Such formal
developments must be submitted together with the paper as auxiliary material,
and will be taken into account during the reviewing process.
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 welcome. One author of each accepted paper
is expected to present it at the conference.
For any questions about the formatting or submission of papers, please consult
the PC chairs.
Important Dates
Abstract submission: October 5, 2016
Full paper submission: October 12, 2016
Notification: November 16, 2016
Conference dates: January 16-17, 2017
Program Committee
Reynald Affeldt, AIST, Japan
Thorsten Altenkirch, University of Nottingham, UK
Jesús Aransay, Universidad de La Rioja, Spain
Andrea Asperti, University of Bologna, Italy
Clark Barrett, New York University, USA
Yves Bertot, INRIA, France (co-chair)
Nikolaj Bjorner, Microsoft Research, USA
Ana Bove, Chalmers University of Technology & University of Gothenburg, Sweden
Delphine Demange, IRISA / University of Rennes 1, France
Marieke Huisman, University of Twente, Netherlands
Reiner Hähnle, Technische Universität Darmstadt, Germany
Cezary Kaliszyk, University of Innsbruck, Austria
Robbert Krebbers, Aarhus University, Denmark
Ondřej Kunčar, Technische Universität München, Germany
Mohsen Lesani, MIT, USA
Assia Mahboubi, INRIA, France
Michael Norrish, Data61, Australia
Vincent Rahli, University of Luxembourg, Luxembourg
Tom Ridge, University of Leicester, UK
Viktor Vafeiadis, MPI-SWS, Germany (co-chair)
Freek Verbeek, Open University of the Netherlands, Netherlands
Steve Zdancewic, University of Pennsylvania, USA
------------------------------------------------------------------------------
Find and fix application performance issues faster with Applications Manager
Applications Manager provides deep performance insights into multiple tiers of
your business applications. It resolves application problems quickly and
reduces your MTTR. Get your free trial!
https://ad.doubleclick.net/ddm/clk/302982198;130105516;z
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
