*CPP 2027: *16th International Conference on Certified Programs and Proofs January 11 - 12, 2027 Mexico City, Mexico (Co-located with POPL 2027) https://popl27.sigplan.org/home/CPP-2027 Abstract Submission Deadline: September 3, 2026 AoE Paper Submission Deadline: September 10, 2026 AoE Author notifications: November 10, 2026 CPP 2027 Conference: January 11-12, 2027 CPP 2027 is an international conference on practical and theoretical topics in all areas that consider formal verification and certification as an essential paradigm for their work. CPP spans areas of computer science, mathematics, logic, and education. CPP 2027 is sponsored by ACM SIGPLAN, in cooperation with ACM SIGLOG. CPP 2027 will be held on January 11–12, 2027, co-located with POPL 2027 in Mexico City, Mexico. CPP 2027 welcomes contributions from all members of the community. It is primarily an in-person event, and at least one author of every accepted paper is expected to attend in person. The organizers aim to support remote participation, with talks recorded and streamed online depending on AV support from the POPL 2027 organizers. *List of Topics* We welcome submissions in research areas related to formal certification of programs and proofs. Topics of interest include, but are not limited to, the following: * 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, Dafny, F*, HOL4, HOL Light, Idris, Isabelle, Lean, Mizar, Nuprl, PVS, Rocq, 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 *Conference Co-Chairs* * Sophie Tourret (Inria) * Yannick Zakowski (Inria) *Programme Committee Co-Chairs* * Cyril Cohen (Inria) * Nikhil Swamy (Microsoft Research) *Programme Committee* Aart Middeldorp [University of Innsbruck] Abhishek Singh [IIIT Hyderabad] Anders Mörtberg [Stockholm University] Andrej Bauer [University of Ljubljana] Anne Baanen [Mathlib Initiative] Ariel Kellison [Code Metal] Assia Mahboubi [Inria, VU Amsterdam] Chantal Keller [Université Paris-Saclay] Chelsea Edmonds [University of Western Australia] Christine Rizkallah [University of Melbourne] Cyril Cohen [Inria] (co-chair) Denis Firsov [Tallinn University of Technology] Derek Dreyer [MPI-SWS] Dmitriy Traytel [University of Copenhagen] Dominik Kirst [Inria] Holger Thies [Kyoto University] Ian Shillito [University of Melbourne] Jannis Limperg [Axiom Math] Jonas Kastberg Hinrichsen [Aalborg University] Julie Cailler [University of Lorraine, CNRS, Inria, LORIA] Julien Narboux [Université Paris Cité] Kathrin Stark [Heriot-Watt University] Kaustuv Chaudhuri [Inria Saclay, École Polytechnique] Kenji Maillard [Inria, University of Nantes] Lauren M. White [NASA] Lawrence C. Paulson [University of Cambridge] María Inés de Frutos-Fernández [University of Bonn] Martin Bodin [Inria] Matthieu Sozeau [Inria] Mauricio Ayala-Rincón [University of Brasília, Federal University of Goiás] Nada Amin [Harvard University] Nikhil Swamy [Microsoft Research] (co-chair) Patricia Johann [Appalachian State University] Qinxiang Cao [Shanghai Jiao Tong University] René Thiemann [University of Innsbruck] Reynald Affeldt [AIST] Sébastien Gouëzel [Université de Rennes] Simon Oddershede Gregersen [CISPA Helmholtz Center for Information Security] Sophie Morel [CNRS] Stefan Zetsche [AWS] Stéphane Graham-Lengrand [SRI] Tobias Nipkow [TU Munich] Viktor Vafeiadis [MPI-SWS] Xavier Allamigeon [Inria, École polytechnique] Yann Herklotz [EPFL] Yannick Forster [Inria] Yao Li [Portland State] Yonghyun Kim [MPI-SP] *Submission link:* https://popl27.sigplan.org/home/CPP-2027#Call-for-Papers *Author notifications*: November 10, 2026 -Regards. Abhishek Singh Software Engineering Research Centre IIIT Hyderabad. Home Page <https://sites.google.com/view/abhishek-singh/home> <http://www.tcs.tifr.res.in/people/students>