Email Gateway (Aug 22 2022 at 15:25): Email Gateway (Aug 22 2022 at 15:25):From: Amy Felty <afelty@eecs.uottawa.ca>
CALL FOR PAPERS
The 7th ACM SIGPLAN International Conference
on Certified Programs and Proofs (CPP 2018)
co-located with POPL 2018
in cooperation with ACM SIGLOG
http://popl18.sigplan.org/track/CPP-2018
8-9 January, 2018, Los Angeles, USA
Certified Programs and Proofs (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.
Important dates
- Abstract submission deadline: Fri 6 Oct 2017
- Full paper submission deadline: Wed 11 Oct 2017
- Notification: Tue 14 Nov 2017
- Camera-ready deadline: Fri 24 Nov 2017
- Conference dates: Mon 8 - Tue 9 Jan 2018
Topics of interest
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=cpp2018
Submitted papers must be formatted following the ACM SIGPLAN
Proceedings format using the sigplanconf format (not the acmart
format), using 10 point font for the main text (not the default 9pt
font).
http://www.sigplan.org/Resources/Author/
Submitted papers should not exceed 12 pages, including tables and
figures, but excluding bibliography. Shorter papers are welcome and
will be given equal consideration.
Abstracts must be submitted by October 6, 2017 (AOE). The deadline for
full papers is October 11, 2017 (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.
Program Committee
Reynald Affeldt (AIST, Japan)
June Andronick (Data61, CSIRO and UNSW, Australia), co-chair
Lennart Beringer (Princeton University, USA)
Jasmin Blanchette (Vrije Universiteit Amsterdam, Netherlands)
Sandrine Blazy (University of Rennes 1, France)
Sylvie Boldo (Inria and Université Paris-Saclay, France)
James Cheney (University of Edinburgh, UK)
Amy Felty (University of Ottawa, Canada), co-chair
Elsa Gunter (University of Illinois, USA)
Reiner Hähnle (Technical University Darmstadt, Germany)
Marieke Huisman (University of Twente, Netherlands)
Warren A. Hunt, Jr. (University of Texas Austin, USA)
Rustan Leino (Microsoft Research, USA)
Assia Mahboubi (Inria, France)
Alberto Momigliano (Università degli Studi di Milano, Italy)
Magnus Myreen (Chalmers University of Technology, Sweden)
Vivek Nigam (Federal University of Paraíba, Brazil / Fortiss, Germany)
Tobias Nipkow (Technical University Munich, Germany)
Gert Smolka (Saarland University, Germany)
Bas Spitters (Aarhus University, Denmark)
Pierre-Yves Strub (École Polytechnique, France)
Laurent Théry (Inria, France)
Josef Urban (Czech Technical University in Prague, Czech Republic)
Viktor Vafeiadis (MPI-SWS, Germany)
Stephanie Weirich (University of Pennsylvania, USA)
Last updated: Apr 16 2024 at 08:18 UTC