Conference Information
CPP 2025: International Conference on Certified Programs and Proofs
https://popl25.sigplan.org/home/CPP-2025Submission Date: |
2024-09-10 |
Notification Date: |
2024-11-19 |
Conference Date: |
2025-01-19 |
Location: |
Denver, Colorado, USA |
Years: |
14 |
Viewed: 9119 Tracked: 3 Attend: 0
Call For Papers
TOPICS OF INTEREST We welcome submissions in research areas related to formal certification of programs and proofs. The following is a non-exhaustive list of topics of interest to CPP: certified or certifying programming, compilation, linking, OS kernels, runtime systems, security monitors, and hardware; certified mathematical libraries and mathematical theorems; proof assistants (e.g, ACL2, Agda, Coq, Dafny, F*, HOL4, HOL Light, Idris, Isabelle, Lean, Mizar, Nuprl, PVS, etc); new languages and tools for certified programming; program analysis, program verification, and program synthesis; program logics, type systems, and semantics for certified code; logics for certifying concurrent and distributed systems; mechanized metatheory, formalized programming language semantics, and logical frameworks; higher-order logics, dependent type theory, proof theory, logical systems, separation logics, and logics for security; verification of correctness and security properties; 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; formal models of computation; mechanized (un)decidability and computational complexity proofs; formally certified methods for induction and coinduction; integration of interactive and automated provers; logical foundations of proof assistants; applications of AI and machine learning to formal verification; user interfaces for proof assistants and theorem provers; teaching mathematics and computer science with proof assistants. Submissions will be reviewed based on the following criteria: Thoroughly discuss the theory or design choices underpinning the formalization. Provide a detailed explanation of the formalization decisions, including alternative approaches and reasons for rejecting them. Examine related literature on formalization choices and techniques. Compare the design choices to those made in other libraries. Offer feedback on the features of the computer proof assistant used, noting any that are missing. Draw conclusions that can guide future formalization efforts in the same or other proof assistants.
Last updated by Dou Sun in 2024-10-02
Related Conferences
Short | Full Name | Submission | Conference |
---|---|---|---|
APMediaCast | Asia Pacific Conference on Multimedia and Broadcasting | 2014-12-23 | 2015-04-23 |
ICCIC | International Conference on Computational Intelligence and Computing Research | 2014-11-05 | 2015-12-18 |
ICAEM | International Conference on Advanced Energy Materials | 2023-01-20 | 2023-01-13 |
Euro-Par | European Conference on Parallel and Distributed Computing | 2025-08-25 | |
ICCA | International Conference on Computer Applications | 2013-09-15 | 2013-12-19 |
ICAMCE | International Ionference on Advanced Materials and Clean Energy | 2023-01-20 | 2023-02-17 |
APSEC | Asia-Pacific Software Engineering Conference | 2024-07-06 | 2024-12-03 |
ICACTE | International Conference on Advanced Computer Theory and Engineering | 2020-07-30 | 2020-09-18 |
PRISMS | International Conference on Privacy and Security in Mobile Systems | 2014-02-21 | 2014-05-11 |
MFPS | International Conference on the Mathematical Foundations of Programming Semantics | 2015-04-03 | 2015-06-22 |
Related Journals
CCF | Full Name | Impact Factor | Publisher | ISSN |
---|---|---|---|---|
c | Cybernetics and Systems | Taylor & Francis | 0196-9722 | |
Journal of Object Technology | EtH Zurich | 1660-1769 | ||
Image Processing On Line | IPOL | 2105-1232 | ||
IEEE Transactions on Intelligent Vehicles | 14.00 | IEEE | 2379-8858 | |
c | Journal of Information Security and Applications | 3.800 | Elsevier | 2214-2126 |
IEEE Transactions on Very Large Scale Integration (VLSI) Systems | 2.800 | IEEE | 1063-8210 | |
IEEE Open Journal of Control Systems | IEEE | 2694-085X | ||
Spatial Statistics | 2.100 | Elsevier | 2211-6753 | |
IEEE Transactions on Emerging Topics in Computational Intelligence | 5.300 | IEEE | 2471-285X | |
International Journal on Applications of Graph Theory in Wireless Ad hoc Networks and Sensor Networks | AIRCC | 0975-7260 |
Full Name | Impact Factor | Publisher |
---|---|---|
Cybernetics and Systems | Taylor & Francis | |
Journal of Object Technology | EtH Zurich | |
Image Processing On Line | IPOL | |
IEEE Transactions on Intelligent Vehicles | 14.00 | IEEE |
Journal of Information Security and Applications | 3.800 | Elsevier |
IEEE Transactions on Very Large Scale Integration (VLSI) Systems | 2.800 | IEEE |
IEEE Open Journal of Control Systems | IEEE | |
Spatial Statistics | 2.100 | Elsevier |
IEEE Transactions on Emerging Topics in Computational Intelligence | 5.300 | IEEE |
International Journal on Applications of Graph Theory in Wireless Ad hoc Networks and Sensor Networks | AIRCC |
Recommendation