🏠홈📊트렌드🏆논문👤마이
CS-Pedia
TrendsBest Papers
Best Papers/POPL

POPL Best Papers

ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

37 papers · 2021–2025

← POPL Conference Info

🏆 2025(7)

Distinguished Paper Award
A Primal-Dual Perspective on Program Verification Algorithms
Takeshi TsukadaHiroshi UnnoOded PadonSharon Shoham
formal verificationalgorithmsfixpoint
Distinguished Paper Award
Affect: An Affine Type and Effect System
Orpheas van RooijRobbert Krebbers
type systemseffectsaffine types
Distinguished Paper Award
Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings
Jan van BrüggeJames McKinnaAndrei PopescuDmitriy Traytel
formal methodstype theoryinduction
Distinguished Paper Award
Data Race Freedom à la Mode
Aina Linn GeorgesBenjamin PetersLaila ElbeheiryLeo WhiteStephen DolanRichard A. EisenbergChris CasinghinoFrançois PottierDerek Dreyer
concurrencyrace freedomtype systems
Distinguished Paper Award
Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops
Fabian ZaiserAndrzej MurawskiC.-H. Luke Ong
probabilistic programmingformal methodsloops
Distinguished Paper Award
Relaxed Memory Concurrency Re-executed
Evgenii MoiseenkoMatteo MeluzziInnokentii MeleshchenkoIvan KabashnyiAnton PodkopaevSoham Chakraborty
concurrencymemory modelsformal methods
Distinguished Paper Award
TensorRight: Automated Verification of Tensor Graph Rewrites
Jai AroraSirui LuDevansh JainTianfan XuFarzin HoushmandPhitchaya Mangpo PhothilimthanaMohsen LesaniPraveen NarayananKarthik Srinivasa MurthyRastislav BodíkAmit SabneCharith Mendis
machine learningcompilersformal verificationtensor

🏆 2024(9)

Distinguished Paper Award
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
Neta EladOded PadonSharon Shoham
formal verificationcounterexamplesdeductive reasoning
Distinguished Paper Award
Automatic Parallelism Management
Sam WestrickMatthew FluetMike RaineyUmut A. Acar
parallel computingprogramming languagesscheduling
Distinguished Paper Award
Flan: An Expressive and Efficient Datalog Compiler for Program Analysis
Supun AbeysingheAnxhelo XhebrajTiark Rompf
compilersdatalogprogram analysis
Distinguished Paper Award
Implementation and Synthesis of Math Library Functions
Ian BriggsYash LadPavel Panchekha
numerical computingprogram synthesisfloating point
Distinguished Paper Award
Modular Denotational Semantics for Effects with Guarded Interaction Trees
Daniel FruminAmin TimanyLars Birkedal
formal semanticseffectsinteraction trees
Distinguished Paper Award
Nominal Recursors as Epi-Recursors
Andrei Popescu
type theoryformal methodsrecursion
Distinguished Paper Award
Parametric Subtyping for Structural Parametric Polymorphism
Henry DeYoungAndreia MordidoFrank PfenningAnkush Das
type systemssubtypingpolymorphism
Distinguished Paper Award
Soundly Handling Linearity
Wenhao TangDaniel HillerströmSam LindleyJ. Garrett Morris
type systemslinear typeseffects
Distinguished Paper Award
Total Type Error Localization and Recovery with Holes
Eric ZhaoRaef MaroofAnand DukkipatiAndrew BlinnZhiyi PanCyrus Omar
type systemserror recoveryprogramming tools

🏆 2023(7)

Distinguished Paper Award
ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs
Alexander K. LewMathieu HuotSam StatonVikash K. Mansinghka
probabilistic programmingautomatic differentiationmachine learning
Distinguished Paper Award
Admissible Types-to-PERs Relativization in Higher-Order Logic
Andrei PopescuDmitriy Traytel
type theoryformal methodshigher-order logic
Distinguished Paper Award
DimSum: A Decentralized Approach to Multi-language Semantics and Verification
Michael SammlerSimon SpiesYoungju SongEmanuele D'OsualdoRobbert KrebbersDeepak GargDerek Dreyer
formal methodsmulti-languageverification
Distinguished Paper Award
Dynamic Race Detection with O(1) Samples
Mosaad Al ThokairMinjian ZhangUmang MathurMahesh Viswanathan
concurrencyrace detectionprogram analysis
Distinguished Paper Award
Higher-Order Leak and Deadlock Free Locks
Jules JacobsStephanie Balzer
concurrencytype systemsformal methods
Distinguished Paper Award
Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification
Hiroshi UnnoTachio TerauchiYu GuEric Koskinen
formal verificationtemporal logicfixpoint
Distinguished Paper Award
SSA Translation Is an Abstract Interpretation
Matthieu Lemerre
compilersabstract interpretationssa

🏆 2022(7)

Distinguished Paper Award
Bottom-Up Synthesis of Recursive Functional Programs using Angelic Execution
Anders MiltnerAdrian Trejo NuñezAna BrendelSwarat ChaudhuriIşıl Dillig
program synthesisfunctional programmingrecursion
Distinguished Paper Award
Formal Metatheory of Second-Order Abstract Syntax
Marcelo FioreDmitrij Szamozvancev
formal methodstype theoryabstract syntax
Distinguished Paper Award
Learning Formulas in Finite Variable Logics
Paul KrogmeierP. Madhusudan
formal methodsmachine learninglogic
Distinguished Paper Award
Observational Equality: Now for Good
Loïc PujetNicolas Tabareau
type theoryequalitydependent types
Distinguished Paper Award
One Polynomial Approximation to Produce Correctly Rounded Results of an Elementary Function for Multiple Representations and Rounding Modes
Jay P. LimSantosh Nagarakatte
numerical computingfloating pointcorrectness
Distinguished Paper Award
Pirouette: Higher-Order Typed Functional Choreographies
Andrew K. HirschDeepak Garg
type systemschoreographiesfunctional programming
Distinguished Paper Award
Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations
Lennard GäherMichael SammlerSimon SpiesRalf JungHoang-Hai DangRobbert KrebbersJeehoon KangDerek Dreyer
concurrencyseparation logicprogram optimizationformal methods

🏆 2021(7)

Distinguished Paper Award
A Pre-Expectation Calculus for Probabilistic Sensitivity
Alejandro AguirreGilles BartheJustin HsuBenjamin Lucien KaminskiJoost-Pieter KatoenChristoph Matheja
probabilistic programmingformal methodssensitivity analysis
Distinguished Paper Award
A Verified Optimizer for Quantum Circuits
Kesha HietalaRobert RandShih-Han HungXiaodi WuMichael Hicks
quantum computingcompilersformal verification
Distinguished Paper Award
An Abstract Interpretation for SPMD Divergence on Reducible Control Flow Graphs
Julian RosemannSimon MollSebastian Hack
abstract interpretationcompilersgpu
Distinguished Paper Award
Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
Marco VassenaCraig DisselkoenKlaus von GleissenthallSunjay CauligiRami Gökhan KıcıRanjit JhalaDean TullsenDeian Stefan
securityspeculative executionprogram analysiscryptography
Distinguished Paper Award
Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory Programs
Pascal BaumannRupak MajumdarRamanathan S. ThinniyamGeorg Zetzsche
concurrencyformal verificationliveness
Distinguished Paper Award
Provably Space Efficient Parallel Functional Programming
Jatin AroraSam WestrickUmut A. Acar
parallel computingfunctional programmingspace efficiency
Distinguished Paper Award
egg: Fast and Extensible Equality Saturation
Max WillseyChandrakana NandiYisu Remy WangOliver FlattZachary TatlockPavel Panchekha
compilersequality saturationprogram optimization

CS-Pedia — 한국 CS 연구자를 위한 학회 통합 플랫폼

데이터 출처: DBLP (CC0), OpenAlex (CC0), Semantic Scholar, aideadlin.es (MIT), 한국연구재단, 한국정보과학회, jeffhuang.com

제출 전 데드라인·학회 일정은 공식 웹사이트에서 반드시 확인하세요.

소개·개인정보 처리방침·이용약관·문의