POPL 2017
Sun 15 - Sat 21 January 2017

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.

Follow this link for more information about the CPP series.

CPP 2017 is co-located with POPL 2017, in Paris, France. Registration and accommodation information will mostly be available on that site.

Dates
You're viewing the program in a time zone which is different from your device's time zone - change time zone

Mon 16 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00
Invited TalkCPP at Auditorium
09:00
60m
Talk
Porting the HOL Light Analysis Library: Some Lessons
CPP
Lawrence Paulson University of Cambridge
File Attached

Tue 17 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:00
Invited TalkCPP at Auditorium
09:00
60m
Talk
Mechanized verification of preemptive OS kernels
CPP
Xinyu Feng University of Science and Technology of China
File Attached
10:30 - 12:00
Verified programming toolsCPP at Auditorium
10:30
30m
Talk
Verified compilation of CakeML to multiple machine-code targets
CPP
Anthony Fox University of Cambridge, UK, Magnus O. Myreen Chalmers University of Technology, Sweden, Yong Kiam Tan IHPC at A*STAR, Singapore, Ramana Kumar
11:00
30m
Talk
COMPLX: a verification framework for concurrent imperative programs
CPP
Sidney Amani UNSW, Australia, June Andronick Data61,CSIRO (formerly NICTA) and UNSW, Maksym Bortin , Corey Lewis , Christine Rizkallah University of Pennsylvania, USA, Joseph Tuong
11:30
30m
Talk
Verifying dynamic race detection
CPP
William Mansky University of Pennsylvania, Yuanfeng Peng University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Joseph Devietti University of Pennsylvania

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 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. 2016
Notification November 16, 2016
Conference dates January 16–17, 2016

Program committee

Accepted Papers

Title
A Coq Formal Proof of the Lax–Milgram theorem
CPP
A Formalization of the Berlekamp-Zassenhaus Factorization Algorithm
CPP
A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations
CPP
Automatic Cyclic Termination Proofs for Recursive Procedures in Separation Logic
CPP
BliStrTune: Hierarchical Invention of Theorem Proving Strategies
CPP
COMPLX: a verification framework for concurrent imperative programs
CPP
Equivalence of System F and λ2 in Coq based on context morphism lemmas
CPP
Formal foundations of 3D geometry for modeling robot manipulators
CPP
Formalising Real Numbers in Homotopy Type Theory
CPP
Formalization of Karp-Miller Tree Construction on Petri Nets
CPP
Formally verified differential dynamic logic
CPP
Lifting proof-relevant unification to higher dimensions
CPP
Markov Processes in Isabelle/HOL
CPP
DOI Pre-print File Attached
The HoTT library: a formalization of homotopy type theory in Coq
CPP
Pre-print
The Next 700 Syntactical models of type theory
CPP
Type-and-scope safe programs and their proofs
CPP
Verified compilation of CakeML to multiple machine-code targets
CPP
Verifying a hash table and its iterators in higher-order separation logic
CPP
Verifying dynamic race detection
CPP

The proceedings for this conference are available at the following address

http://www.sigplan.org/OpenTOC/cpp17.html