Research Papers
Full papers on theoretical and experimental aspects of programming languages and systems, submitted to POPL with double-blind review.
Software Eng/CORE A*
POPL 2027
ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
POPL 2027 is the annual ACM SIGPLAN Symposium on Principles of Programming Languages, serving as a forum for theoretical and experimental research on programming languages and systems. It covers foundational aspects of design, analysis, implementation, and application of programming languages, and is co-located with several specialized workshops and conferences such as CPP and VMCAI.
Key deadlines
Verified September 9, 2026Full paper
July 10, 2026
AoE
Conference timeline
Submission and decisions
Full paperKey deadline
July 10, 2026 · AoE
Paper fit
Contribution paths
A strong submission should clearly identify its contribution and evaluate it appropriately.
CPP Papers
Papers on formal verification and certification, submitted to CPP 2027 with lightweight double-blind review, up to 12 pages excluding bibliography and appendices.
Workshop Proposals
Proposals for one-day workshops co-located with POPL, including description, format, organizers, and plans for remote participation.
Tutorial Proposals
Proposals for 1.5- or 3-hour tutorials on topics relevant to the POPL community, including objectives, target audience, and prerequisite knowledge.
Student Research Competition Submissions
Submissions from students presenting research work, evaluated for the POPL Student Research Competition.
Artifact Submissions
Supplementary artifacts (code, data, proofs) accompanying accepted POPL or CPP papers, submitted for evaluation.
Research areas in scope
01
CPP 2027 (Certified Programs and Proofs)
certified or certifying programming, compilation, linking, OS kernels, runtime systems, security monitors, and hardwarecertified mathematical libraries and mathematical theoremsproof assistants (e.g., ACL2, Agda, Dafny, F*, HOL4, HOL Light, Idris, Isabelle, Lean, Mizar, Nuprl, PVS, Rocq)new languages and tools for certified programmingprogram analysis, program verification, and program synthesisprogram logics, type systems, and semantics for certified codelogics for certifying concurrent and distributed systemsmechanized metatheory, formalized programming language semantics, and logical frameworkshigher-order logics, dependent type theory, proof theory, logical systems, separation logics, and logics for securityverification of correctness and security propertiescertificates for decision procedures (linear algebra, polynomial systems, SAT, SMT, unification)certificates for semi-decision procedures (equality, first-order logic, higher-order unification)certificates for program terminationformal models of computationmechanized (un)decidability and computational complexity proofsformally certified methods for induction and coinductionintegration of interactive and automated proverslogical foundations of proof assistantsapplications of AI and machine learning to formal verificationuser interfaces for proof assistants and theorem proversteaching mathematics and computer science with proof assistants
02
Workshops
FPBT: Future of Property-based TestingFRIDA: Formal Reasoning in Distributed AlgorithmsLAFI: Languages for InferencePAgE: Principles Of Agentic EngineeringPEPM: Partial Evaluation and Program ManipulationPLanQC: Programming Languages for Quantum ComputingPLMW @ POPL: PL Mentoring WorkshopPriSC: Principles of Secure CompilationRocqPL: Rocq for Programming LanguagesTPSA: Theory and Practice of Static AnalysisWAVE: Workshop on Auto-active Verification
Policies worth checking twice
- POPL employs full double-blind reviewing.
- CPP employs a lightweight double-blind reviewing process: author names and institutions must be omitted, and references to own work must be in third person.
- Papers must not exceed 12 pages (excluding bibliography and clearly marked appendices) for CPP submissions.
- Submissions must follow the ACM SIGPLAN Proceedings format using the acmart style with the sigplan option.
- Concurrent submissions to other conferences, journals, or workshops with proceedings are not allowed.
- Authors must adhere to the ACM Policy on Authorship, including the use of AI tools, which must not plagiarize, misrepresent, or falsify content, and the resulting work must be an accurate representation of the authors' intellectual contributions.
- Authors are responsible for the veracity and correctness of all material, including AI-generated content.
- At least one author of every accepted CPP paper is expected to attend in person.
Official sources
Compiled from the official call for papers. The organizers’ pages remain authoritative.
Official conference siteTutorialsWorkshops and Co-located EventsCPP Certified Programs and ProofsPEPM Partial Evaluation and Program ManipulationPLanQC Programming Languages for Quantum Computing
Last verified September 9, 2026