POPL 2024 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (959)

A Guillermo A. PerezA. Perez, Guillermo University of AntwerpBelgium Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic
Carmine AbateAbate, Carmine Inria Paris Committee Member in Program Committee within the PriSC-track
Parosh Aziz AbdullaAbdulla, Parosh Aziz Uppsala University, SwedenSweden Boosting Constrained Horn Solving by Unsat Core Learning
Supun AbeysingheAbeysinghe, Supun Purdue UniversityUnited States Rhyme: A Data-Centric Expressive Query Language for Nested Data Structures Flan: An Expressive and Efficient Datalog Compiler for Program Analysis
Umut A. AcarAcar, Umut A. Carnegie Mellon UniversityUnited States Automatic Parallelism Management Disentanglement with Futures, State, and Interaction
Nate AckermanAckerman, Nate Harvard University Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets
Arthur AdjedjAdjedj, Arthur ENS Paris Saclay, Université Paris-Saclay Martin-Löf à la Coq
Weronika T. AdrianAdrian, Weronika T. Committee Member in Program Committee within the PADL-track
Alejandro AguirreAguirre, Alejandro Aarhus UniversityDenmark Asynchronous Probabilistic Couplings in Higher-Order Separation Logic Committee Member in Program Committee within the POPL -track
Amal AhmedAhmed, Amal Northeastern University, USAUnited States Towards a Categorical Model of the Lilac Separation Logic All the Binaries Together: A Semantic Approach to Application Binary Interfaces Steering Committee Member in Steering Committee within the PriSC-track
Benedikt AhrensAhrens, Benedikt Delft University of TechnologyNetherlands Univalent Double Categories Displayed Monoidal Categories for the Semantics of Linear Logic PC Member in Program Committee within the CPP-track
Kinan Dak AlbabAlbab, Kinan Dak Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Aws AlbarghouthiAlbarghouthi, Aws University of Wisconsin-MadisonUnited States Committee Member in Program Committee within the POPL -track
Aurore AlcoleiAlcolei, Aurore INRIA RennesFrance Committee Member in Program Committee within the GALOP-track
Jonathan AldrichAldrich, Jonathan Carnegie Mellon UniversityUnited States Gradual Verification for Smart Contracts Sound Gradual Verification with Symbolic Execution
Jade AlglaveAlglave, Jade University College LondonFrance Arm Architecture and Formal Artifacts: Memory Model and Instruction Semantics
Thorsten AltenkirchAltenkirch, Thorsten University of Nottingham Internal parametricity, without an interval
Mario AlvianoAlviano, Mario University of CalabriaItaly Rethinking Answer Set Programming Templates Marketplace Logistic via Answer Set Programming
Nicolas AmatAmat, Nicolas LAAS-CNRSFrance Project and Conquer: Fast Quantifier Elimination for Checking Petri Nets Reachability
Danilo AmendolaAmendola, Danilo Oliveru - Smartly Engineering Marketplace Logistic via Answer Set Programming
Matthew AmyAmy, Matthew Simon Fraser UniversityCanada Committee Member in Program Committee within the PLanQC-track Committee Member in Organizing Committee within the PLanQC-track
Abhishek AnandAnand, Abhishek Cornell UniversityUnited States Modularizing CPU Semantics for Virtualization
Jacob AndreasAndreas, Jacob MIT Effective Sequential Monte Carlo for Language Model Probabilistic Programs
Cezar-Constantin AndriciAndrici, Cezar-Constantin MPI-SPGermany Securing Verified IO Programs Against Unverified Code in F*
Étienne AndréAndré, Étienne Université Sorbonne Paris Nord; LIPN; CNRSFrance Parameterized Verification of Disjunctive Timed Networks
Zhendong AngAng, Zhendong National University of Singapore Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic Predictive Monitoring against Pattern Regular Languages
Carlo AngiuliAngiuli, Carlo Indiana UniversityUnited States Committee Member in Program Committee within the POPL -track
Andrew W. AppelAppel, Andrew W. Princeton University VCFloat2: Floating-point error analysis in Coq VST-A: A Foundationally Sound Annotation Verifier Committee Member in Program Committee within the POPL -track
Jaime AriasArias, Jaime CNRS; LIPN; Université Sorbonne Paris NordFrance Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Joaquín AriasArias, Joaquín Universidad Rey Juan CarlosSpain Automated Interactive Domain-Specific Conversational Agents that Understand Human Dialogs
Jatin AroraArora, Jatin Carnegie Mellon UniversityUnited States Disentanglement with Futures, State, and Interaction
Kazuyuki AsadaAsada, Kazuyuki Tohoku University Enriched Presheaf Model of Quantum FPC
Flavio AscariAscari, Flavio University of Pisa A comparison of program logics for (in)correctness
Robert AtkeyAtkey, Robert University of Strathclyde Polynomial Time and Dependent types PC Member in Program Committee within the CPP-track
Eric AtkinsonAtkinson, Eric Committee Member in Program Committee within the LAFI-track
Lyes AttoucheAttouche, Lyes Université Paris-Dauphine -- PSL Validation of Modern JSON Schema: Formalization and Complexity
Lennart AugustssonAugustsson, Lennart Epic Games Committee Member in Program Committee within the WITS-track
Jeremy AvigadAvigad, Jeremy Carnegie Mellon University, USA PC Member in Program Committee within the CPP-track
Sacha-Élie AyounAyoun, Sacha-Élie Imperial College LondonUnited Kingdom Student Volunteer Co-Chair in Organizing Committee for POPL 2024 Unified Compositional Formal Methods: Exact Separation Logic and the Gillian Platform for Correctness and Incorrectness Reasoning
Jon AytacAytac, Jon Sandia National Laboratories Towards a Categorical Model of the Lilac Separation Logic
Arthur Azevedo de AmorimAzevedo de Amorim, Arthur Rochester Institute of Technology, USAUnited States Pipelines and Beyond: Graph Types for ADTs with Futures
B Mohamed-Amine BaaziziBaazizi, Mohamed-Amine Sorbonne Université Validation of Modern JSON Schema: Formalization and Complexity
Casper Bach PoulsenBach Poulsen, Casper Delft University of TechnologyNetherlands Committee Member in Program Committee within the POPL -track
Michael BackesBackes, Michael Cispa Helmholtz Center for Information Security Lifting Compiler Security Properties to Stronger Attackers: the Speculation Case Secure Composition of SPECTRE Mitigations
Patrick BahrBahr, Patrick IT University of CopenhagenDenmark Asynchronous Reactive Programming with Modal Types in Haskell Committee Member in Program Committee within the PADL-track
Guangdong BaiBai, Guangdong The University of QueenslandAustralia ReLU Hull Approximation
A. R. BalasubramanianBalasubramanian, A. R. Technical University of Munich Reachability in Continuous Pushdown VASS
Teodoro BaldazziBaldazzi, Teodoro Università degli Studi Roma Tre Ontological Reasoning over Shy and Warded Datalog+/- for Streaming-based Architectures
Marcello BalducciniBalduccini, Marcello Saint Joseph's University, USA Committee Member in Program Committee within the PADL-track
Stephanie BalzerBalzer, Stephanie Carnegie Mellon UniversityUnited States DisLog: A Separation Logic for Disentanglement
Rini BanerjeeBanerjee, Rini University of CambridgeUnited Kingdom Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Suguman BansalBansal, Suguman Georgia Institute of Technology, USAUnited States Committee Member in Program Committee within the POPL -track
Jialu BaoBao, Jialu Cornell University Mixture Languages
Yuyan BaoBao, Yuyan Augusta UniversityUnited States Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs
Joachim BardBard, Joachim CISPA Helmholtz Center for Information SecurityGermany Automatic and Incremental Repair for Speculative Information Leaks
Sébastien BardinBardin, Sébastien CEA LIST, University Paris-SaclayFrance Inference of Robust Reachability Constraints
Lara BargmannBargmann, Lara University of Oldenburg A Reachability Logic for a Weak Memory Model with Promises
Shraddha BarkeBarke, Shraddha University of California at San DiegoUnited States Student Volunteer Co-Chair in Organizing Committee for POPL 2024
Clark BarrettBarrett, Clark Stanford UniversityUnited States CLOVER: Closed-Loop Verifiable Code Generation
Gilles BartheBarthe, Gilles MPI-SP; IMDEA Software InstituteGermany Decision and Complexity of Dolev-Yao Hyperproperties
Ezio BartocciBartocci, Ezio Technische Universität WienAustria Committee Member in Program Committee within the VMCAI -track
Osbert BastaniBastani, Osbert University of PennsylvaniaUnited States Optimal Program Synthesis via Abstract Interpretation
Kinjal BasuBasu, Kinjal IBM Automated Interactive Domain-Specific Conversational Agents that Understand Human Dialogs
Mark BattyBatty, Mark University of KentUnited Kingdom Organizing Committee in Organizing Committee within the The Future of Weak Memory-track
Kevin BatzBatz, Kevin RWTH Aachen UniversityGermany Caesar: A Verifier for Probabilistic Programs Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs
Mireia González BedmarBedmar, Mireia González University of Barcelona and Formal Vindications S.L. UTC time, formally verified
Luigi BellomariniBellomarini, Luigi Banca d'Italia Ontological Reasoning over Shy and Warded Datalog+/- for Streaming-based Architectures
Nick BentonBenton, Nick MetaUnited Kingdom Committee Member in Program Committee within the POPL -track
Pascal BergsträßerBergsträßer, Pascal University of Kaiserslautern-LandauGermany Ramsey Quantifiers in Linear Arithmetics
Lennart BeringerBeringer, Lennart Princeton UniversityUnited States Compositional Verification of Concurrent C Programs with Search Structure Templates Steering Committee Member in Steering Committee within the CPP-track
Quentin BerthetBerthet, Quentin Google DeepMind Committee Member in Program Committee within the LAFI-track
Nathalie BertrandBertrand, Nathalie INRIA Rennes Committee Member in Program Committee within the VMCAI -track
Frédéric BessonBesson, Frédéric INRIA A Verified Compiler for Packet Filtering
Siddharth BhatBhat, Siddharth the University of EdinburghUnited Kingdom Guided Equality Saturation
Dariusz BiernackiBiernacki, Dariusz University of WrocławPoland Committee Member in Program Committee within the POPL -track
Lars BirkedalBirkedal, Lars Aarhus UniversityDenmark Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement Modular Denotational Semantics for Effects with Guarded Interaction Trees Asynchronous Probabilistic Couplings in Higher-Order Separation Logic The Essence of Generalized Algebraic Data Types The Logical Essence of Well-Bracketed Control Flow An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic
Tom BiskupBiskup, Tom RWTH Aachen University, Germany Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs
Joydeep BiswasBiswas, Joydeep The University of Texas at Austin Programming-by-Demonstration for Long-Horizon Robot Tasks
Sandrine BlazyBlazy, Sandrine University of RennesFrance PC Chair in Program Committee within the CPP-track PC Chair in Organizing Committee within the CPP-track
Martin BlichaBlicha, Martin Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Andrew BlinnBlinn, Andrew University of MichiganUnited States Total Type Error Localization and Recovery with Holes
Pauline BlohmBlohm, Pauline Uni MünsterGermany Deductive Verification of Parameterized Embedded Systems modeled in SystemC
Laura BocchiBocchi, Laura University of KentUnited Kingdom Committee Member in Program Committee within the PEPM-track
Stefan BodenmüllerBodenmüller, Stefan University of AugsburgGermany A Fully Verified Persistency Library
Mikolaj BojanczykBojanczyk, Mikolaj Warsaw University Polyregular functions on unordered trees of bounded height
Sylvie BoldoBoldo, Sylvie Inria and Université Paris-SaclayFrance Committee Member in Programme Committee within the PROPL-track
Michele BorealeBoreale, Michele Università di FirenzeItaly Guaranteed inference for probabilistic programs: a parallelisable, small-step operational approach
Ana de Almeida BorgesBorges, Ana de Almeida University of Barcelona and Formal Vindications S.L. UTC time, formally verified
Michael BorkowskiBorkowski, Michael University of California, San Diego Mechanizing Refinement Types
Luca BortolussiBortolussi, Luca Department of Mathematics and Geosciences, University of Trieste Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures
Aleksander Boruch-GruszeckiBoruch-Gruszecki, Aleksander EPFLSwitzerland When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism
Ahmed BouajjaniBouajjani, Ahmed IRIF, Université Paris DiderotFrance Committee Member in Program Committee within the POPL -track
Thomas BourgeatBourgeat, Thomas EPFL PC Member in Program Committee within the CPP-track
Matt BowersBowers, Matt Massachusetts Institute of TechnologyUnited States Toward Probabilistic Coarse-to-Fine Program Synthesis
William J. BowmanBowman, William J. University of British ColumbiaCanada Indexed Types for a Statically Safe WebAssembly Committee Member in Program Committee within the PriSC-track
Marius BozgaBozga, Marius CNRS; Université Grenoble AlpesFrance Function synthesis for maximizing model counting
Jonathan Immanuel BrachthäuserBrachthäuser, Jonathan Immanuel University of TübingenGermany Committee Member in Program Committee within the POPL -track
Edwin BradyBrady, Edwin University of St Andrews, UKUnited Kingdom Committee Member in Program Committee within the PEPM-track Committee Member in Program Committee within the WITS-track
Oliver BračevacBračevac, Oliver Galois, Inc.United States Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs
Ian BriggsBriggs, Ian University of Utah Implementation and Synthesis of Math Library Functions
Christopher BrixBrix, Christopher RWTH Aachen University Generation of Verified Assembly Code Using Dafny and Reinforcement Learning
Fraser BrownBrown, Fraser CMU Committee Member in Program Committee within the POPL -track
Lily BrownBrown, Lily RobloxUnited States Towards an Unsound But Complete Type System: Work In Progress on New Non-Strict Mode for Luau
Stefan BrunthalerBrunthaler, Stefan Bundeswehr University MunichGermany Committee Member in Program Committee within the PriSC-track
Laura BrædderBrædder, Laura A formal security analysis of Blockchain voting
Alex Buna-MargineanBuna-Marginean, Alex University of Oxford On Learning Polynomial Recursive Programs
Matteo BusiBusi, Matteo University Ca' Foscari, VeniceItaly When Obfuscations Preserve Cryptographic Constant-Time Committee Member in Program Committee within the PriSC-track Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Joaquim Casals BuñuelBuñuel, Joaquim Casals University of Barcelona and Formal Vindications S.L. UTC time, formally verified
Twain ByrnesByrnes, Twain Carnegie Mellon University, Amazon, AWSUnited States Automatically Enforcing Rust Trait Properties
Lucas BöltzBöltz, Lucas Univerity of KoblenzGermany On the Verification of a Subgraph Construction Algorithm
C Shaowei CaiCai, Shaowei Institute of Software at Chinese Academy of SciencesChina Efficient Local Search for Nonlinear Real Arithmetic
Francesco CalimeriCalimeri, Francesco University of Calabria Forgetting Techniques for Optimizing ASP-based Stream Reasoning
Brian CampbellCampbell, Brian University of Edinburgh Committee Member in Organizing Committee within the POCL-track
Marco CampionCampion, Marco INRIA & École Normale Supérieure \| Université PSLFrance Monotonicity and the Precision of Program Analysis
John Peter CamporaCampora, John Peter Quantinuum Type-based Gradual Typing Performance Optimization
Filip Cano CórdobaCano Córdoba, Filip Technical University of Graz Committee Member in Artifact Evaluation Committee within the VMCAI -track
Qinxiang CaoCao, Qinxiang Shanghai Jiao Tong UniversityChina VST-A: A Foundationally Sound Annotation Verifier
Jacques CaretteCarette, Jacques McMaster UniversityCanada With a Few Square Roots, Quantum Computing is as Easy as Pi Committee Member in Program Committee within the PEPM-track PC Member in Program Committee within the CPP-track
Manuel CarroCarro, Manuel IMDEA Software Institute and T.U. of Madrid (UPM)Spain Committee Member in Program Committee within the PADL-track
Giuseppe CastagnaCastagna, Giuseppe CNRS; Université Paris CitéFrance Polymorphic Type Inference for Dynamic Languages
Ethan CecchettiCecchetti, Ethan University of Wisconsin-MadisonUnited States Computational-Bounded Robust Compilation and Universally Composable Security
Lorenzo CeragioliCeragioli, Lorenzo IMT Lucca, Italy Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-Deterministic Observers
Emmanuel ChaillouxChailloux, Emmanuel UPMC, France Hardware implementation of OCaml using a synchronous functional language
Tej ChajedChajed, Tej UW-MadisonUnited States Co-chair in Program Committee within the CoqPL-track
Soham ChakrabortyChakraborty, Soham TU DelftNetherlands TBC How Hard is Weak-Memory Testing? Committee Member in Program Committee within the POPL -track
Stefanos ChaliasosChaliasos, Stefanos Imperial College LondonUnited Kingdom API-driven Program Synthesis for Testing Static Typing Implementations
Yorgo ChamounChamoun, Yorgo École Polytechnique Internal parametricity, without an interval
Jonathan ChanChan, Jonathan University of PennsylvaniaCanada Internalizing Indistinguishability with Dependent Types
Nicolas ChappeChappe, Nicolas Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Arthur CharguéraudCharguéraud, Arthur InriaFrance Committee Member in Program Committee within the CoqPL-track PC Member in Program Committee within the CPP-track
Nicolas ChataingChataing, Nicolas ENS Paris Unboxed data constructors -- or, how cpp decides a halting problem
Agnishom ChattopadhyayChattopadhyay, Agnishom Rice University Efficient Matching of Regular Expressions with Lookaround Assertions
Chun Yin ChauChau, Chun Yin HKUST When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism
Isha ChaudharyChaudhary, Isha Univ of Illinois Urbana-Champaign Committee Member in Artifact Evaluation Committee within the VMCAI -track
Clément ChavanonChavanon, Clément INRIA A Verified Compiler for Packet Filtering
Qiaochu ChenChen, Qiaochu University of Texas at AustinUnited States Committee Member in Artifact Evaluation Committee within the VMCAI -track
Qiaochu ChenChen, Qiaochu Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Sheng ChenChen, Sheng UL Lafayette Type-based Gradual Typing Performance Optimization
Taolue ChenChen, Taolue University of LondonUnited Kingdom EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis
Yanju ChenChen, Yanju University of California at Santa BarbaraUnited States Committee Member in Artifact Evaluation Committee within the VMCAI -track
Yuqi ChenChen, Yuqi ShanghaiTech University, ChinaChina EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis
Vincent ChevalCheval, Vincent Inria Paris On Learning Polynomial Recursive Programs
Francesco ChiarielloChiariello, Francesco University of Naples Federico II A direct ASP encoding for Declare
David ChisnallChisnall, David MicrosoftUnited Kingdom Committee Member in Program Committee within the PriSC-track
Adam ChlipalaChlipala, Adam Massachusetts Institute of TechnologyUnited States Programme Committee in Program Committee within the Dafny-track Committee Member in Program Committee within the CoqPL-track Committee Member in Steering Committee within the CPP-track
Alessandro CimattiCimatti, Alessandro Fondazione Bruno KesslerItaly Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking
Stefan CiobacaCiobaca, Stefan Alexandru Ioan Cuza University of Iasi Securing Verified IO Programs Against Unverified Code in F*
Pierre ClairambaultClairambault, Pierre CNRS & LIS, Aix-Marseille UniversitéFrance Committee Member in Organising Committee within the GALOP-track Co-chair in Program Committee within the GALOP-track
Michael CoblenzCoblenz, Michael University of California, San DiegoUnited States Committee Member in Programme Committee within the PROPL-track
Jesper CockxCockx, Jesper Delft University of TechnologyNetherlands Committee Member in Program Committee within the PADL-track Co-chair in Program Committee within the WITS-track PC Member in Program Committee within the CPP-track
Joshua M. CohenCohen, Joshua M. Princeton University A Formalization of Core Why3 in Coq
Liron CohenCohen, Liron Ben-Gurion University of the NegevIsrael The Complex(ity) Landscape of Checking Infinite Descent Committee Member in Program Committee within the CoqPL-track
Dario ColazzoColazzo, Dario Université Paris-Dauphine -- PSL Validation of Modern JSON Schema: Formalization and Complexity
Luisa CollodiCollodi, Luisa University of FlorenceItaly Guaranteed inference for probabilistic programs: a parallelisable, small-step operational approach
Youyou CongCong, Youyou Tokyo Institute of TechnologyJapan Committee Member in Program Committee within the PEPM-track Committee Member in Program Committee within the PADL-track
Breandan ConsidineConsidine, Breandan McGill UniversityCanada A Tree Sampler for Bounded Context-Free Languages
Breandan ConsidineConsidine, Breandan McGill UniversityCanada Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Évelyne ContejeanContejean, Évelyne CNRS, ENS Paris-Saclay & Université Paris-Saclay PC Member in Program Committee within the CPP-track
Simon CookseyCooksey, Simon University of KentUnited Kingdom Programmers love mind-bogglingly complicated weak memory models
Stefania CostantiniCostantini, Stefania Dipartimento di Ingegneria e Scienze dell'Informazione eMatematica, Univ. dell'Aquila Committee Member in Program Committee within the PADL-track
Andreea CosteaCostea, Andreea National University of SingaporeSingapore Committee Member in Program Committee within the PriSC-track Committee Member in Program Committee within the PEPM-track
Damien CourousséCouroussé, Damien Univ Grenoble Alpes, CEA, ListFrance Inference of Robust Reachability Constraints
Patrick CousotCousot, Patrick New York University Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
Maria-Nicoleta CraciunCraciun, Maria-Nicoleta University of Oxford A slice sampler for the Indian Buffet Process: expressivity in nonparametric probabilistic programming
Will CrichtonCrichton, Will Brown UniversityUnited States A Core Calculus for Documents
Caroline CronjägerCronjäger, Caroline Vrije Universiteit Amsterdam The Never-Ending Trace: An Under-Approximate Approach to Divergence Bugs
Joseph W. CutlerCutler, Joseph W. University of Pennsylvania Improving the Stability of Type Safety Proofs in Dafny
John CyphertCyphert, John University of Wisconsin-Madison, USA Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis
D Ugo Dal LagoDal Lago, Ugo University of Bologna; InriaItaly On Model-Checking Higher-Order Effectful Programs Invited Speaker in Invited Speakers within the GALOP-track
Silvano DAL ZILIODAL ZILIO, Silvano LAAS-CNRSFrance Project and Conquer: Fast Quantifier Elimination for Checking Petri Nets Reachability
Mila Dalla PredaDalla Preda, Mila University of VeronaItaly Monotonicity and the Precision of Program Analysis
Hoang-Hai DangDang, Hoang-Hai BedRock SystemsGermany Towards Modular Specification and Verification of Concurrent Hypervisor-based Isolation Modularizing CPU Semantics for Virtualization
Hezi DanielDaniel, Hezi Israel Academic College in Ramat Gan Teaching Logic and Set Theory with Dafny
Lesly-Ann DanielDaniel, Lesly-Ann Compiler Support for Control-Flow Linearization Using Architectural Mimicry
Lesly-Ann DanielDaniel, Lesly-Ann CEA ListFrance Committee Member in Program Committee within the PriSC-track
Thibault DardinierDardinier, Thibault ETH ZurichSwitzerland Pulse: Proof-oriented Programming in a Concurrent Separation Logic DSL in F*
Ankush DasDas, Ankush AmazonUnited States Parametric Subtyping for Structural Parametric Polymorphism Committee Member in Program Committee within the POPL -track
Emanuele De AngelisDe Angelis, Emanuele CNR-IASIItaly Committee Member in Program Committee within the VMCAI -track
María Inés de Frutos-Fernándezde Frutos-Fernández, María Inés Universidad Autónoma de Madrid A Formalization of Complete Discrete Valuation Rings and Local Fields
Tom de Jongde Jong, Tom University of NottinghamUnited Kingdom Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Jan de Muijnck-Hughesde Muijnck-Hughes, Jan University of StrathclydeUnited Kingdom Colouring Flags with Dafny & Idris
Coen De RooverDe Roover, Coen Vrije Universiteit BrusselBelgium Committee Member in Program Committee within the VMCAI -track
Pierpaolo DeganoDegano, Pierpaolo University of Pisa and IMT School for Advanced Studies Lucca When Obfuscations Preserve Cryptographic Constant-Time
Benjamin DelawareDelaware, Benjamin Purdue UniversityUnited States Type-Based Incorrectness Reasoning
Haowei DengDeng, Haowei University of Maryland at College ParkUnited States A Case for Synthesis of Recursive Quantum Unitary Programs
Yuxin DengDeng, Yuxin East China Normal UniversityChina Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
Farzaneh DerakhshanDerakhshan, Farzaneh Illinois Institute of TechnologyUnited States Committee Member in Program Committee within the PriSC-track
John DerrickDerrick, John A Fully Verified Persistency Library
Jyotirmoy DeshmukhDeshmukh, Jyotirmoy University of Southern California Committee Member in Program Committee within the VMCAI -track
Dominique DevrieseDevriese, Dominique KU LeuvenBelgium Secure Calling Conventions for CHERI Capability Machines in Practice (Work in Progress) Internal and Observational Parametricity for Cubical Agda Steering Committee Member in Steering Committee within the PriSC-track Committee Member in Program Committee within the POPL -track
Henry DeYoungDeYoung, Henry CMU Parametric Subtyping for Structural Parametric Polymorphism
Akshay Dhonthi Ramesh BabuDhonthi Ramesh Babu, Akshay Audi AGGermany AGNES: Abstraction-guided Framework for Deep Neural Networks Security
Işıl DilligDillig, Işıl University of Texas at AustinUnited States Programming-by-Demonstration for Long-Horizon Robot Tasks Semantic Code Refactoring for Abstract Data Types
Rayna DimitrovaDimitrova, Rayna CISPA Helmholtz Center for Information Security Solving Infinite-State Games via Acceleration Co-chair in Program Committee within the VMCAI -track
Christos DimoulasDimoulas, Christos Northwestern UniversityUnited States Effectful Software Contracts
Yuantian DingDing, Yuantian Purdue University Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations
Hasra DodampegamaDodampegama, Hasra University of Birmingham Explanation and Knowledge Acquisition in Ad Hoc Teamwork
Mike DoddsDodds, Mike Galois, Inc. TBC
Stephen DolanDolan, Stephen Jane Street TBC Unboxed data constructors -- or, how cpp decides a halting problem Committee Member in Program Committee within the POPL -track
Alastair F. DonaldsonDonaldson, Alastair F. Imperial College LondonUnited Kingdom Publicity Co-Chair in Organizing Committee for POPL 2024 Randomised Testing of the Dafny Compiler Associate Chair in Program Committee within the POPL -track
Rui DongDong, Rui University of MichiganUnited States Efficient Bottom-Up Synthesis for Programs with Local Variables Committee Member in Artifact Evaluation Committee within the VMCAI -track Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Brijesh DongolDongol, Brijesh University of SurreyUnited Kingdom A Reachability Logic for a Weak Memory Model with Promises A Fully Verified Persistency Library Organizing Committee in Organizing Committee within the The Future of Weak Memory-track
Dana Drachsler CohenDrachsler Cohen, Dana TechnionIsrael Verification of Neural Networks’ Local Differential Classification Privacy
Stefanie Eva DrerupDrerup, Stefanie Eva University of MünsterGermany Deductive Verification of Parameterized Embedded Systems modeled in SystemC
Derek DreyerDreyer, Derek MPI-SWSGermany Program Chair in Organizing Committee for POPL 2024 Program Chair in Program Committee within the POPL -track
Sophia DrossopoulouDrossopoulou, Sophia Imperial College LondonUnited Kingdom Committee Member in Program Committee within the POPL -track
Ke DuDu, Ke An Iris Instance for Verifying CompCert C Programs
Anand DukkipatiDukkipati, Anand University of Michigan Total Type Error Localization and Recovery with Holes
Ross DuncanDuncan, Ross Cambridge Quantum Computing Committee Member in Program Committee within the PLanQC-track Committee Member in Organizing Committee within the PLanQC-track
Bruno DutertreDutertre, Bruno Amazon Web Services Committee Member in Program Committee within the VMCAI -track
Yotam DvirDvir, Yotam Tel Aviv University Committee Member in Artifact Evaluation Committee within the VMCAI -track
Emanuele D’OsualdoD’Osualdo, Emanuele MPI-SWSGermany Committee Member in Program Committee within the POPL -track
E Gabriel EbnerEbner, Gabriel Microsoft Research Lean Formalization of Extended Regular Expression Matching with Lookarounds
Chelsea EdmondsEdmonds, Chelsea University of SheffieldUnited Kingdom Formal Probabilistic Methods for Combinatorial Structures in Isabelle/HOL
Paul EichlerEichler, Paul CISPA - Helmholtz Center for Information SecurityGermany Parameterized Verification of Disjunctive Timed Networks
Marcello EiermannEiermann, Marcello Utrecht UniversityNetherlands AGNES: Abstraction-guided Framework for Deep Neural Networks Security
Susan EisenbachEisenbach, Susan Imperial College LondonUnited Kingdom Work in Progress: Modelling Incorrect Programs in the Open World with Dafny
Richard A. EisenbergEisenberg, Richard A. Jane StreetUnited States Co-chair in Program Committee within the WITS-track
Clemens EisenhoferEisenhofer, Clemens Vienna University of TechnologyAustria Committee Member in Artifact Evaluation Committee within the VMCAI -track
Neta EladElad, Neta Tel Aviv UniversityIsrael An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
Martin ElsmanElsman, Martin University of Copenhagen, DenmarkDenmark Explicit Effects and Effect Constraints in ReML
Michael EmmiEmmi, Michael Amazon Web ServicesUnited States Committee Member in Program Committee within the VMCAI -track
Cristian EneEne, Cristian Verimag, GrenobleFrance Function synthesis for maximizing model counting
Constantin EneaEnea, Constantin Ecole Polytechnique / LIX / CNRSFrance Scaling Verification of Concurrent Programs with the Civl Verifier
Andres ErbsenErbsen, Andres PC Member in Program Committee within the CPP-track
Esra ErdemErdem, Esra Sabanci University, TurkeyTurkey Committee Member in Program Committee within the PADL-track
Joseph EremondiEremondi, Joseph University of EdinburghUnited Kingdom Strictly Monotone Brouwer Trees for Well Founded Recursion Over Multiple Arguments
Julian ErhardErhard, Julian Technical University of MunichGermany Correctness Witness Validation by Abstract Interpretation
Ran EttingerEttinger, Ran Israel Academic College in Ramat Gan Teaching Logic and Set Theory with Dafny
F Xaver FabianFabian, Xaver Cispa Helmholtz Center for Information Security Lifting Compiler Security Properties to Stronger Attackers: the Speculation Case
Claudia FaggianFaggian, Claudia Université de Paris & CNRS Higher Order Bayesian Networks, Exactly
Chris FallinFallin, Chris FastlyUnited States Steering Committee Member in Steering Committee within the PriSC-track
Andong FanFan, Andong The Hong Kong University of Science and TechnologyChina When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
František FarkaFarka, František BedRock Systems Modularizing CPU Semantics for Virtualization
Azadeh FarzanFarzan, Azadeh University of TorontoCanada Commutativity Simplifies Proofs of Parameterized Programs Coarser Equivalences for Causal Concurrency TBD
Marco FavoritoFavorito, Marco Banca d'Italia Ontological Reasoning over Shy and Warded Datalog+/- for Streaming-based Architectures
Aleksandr FedchinFedchin, Aleksandr Tufts UniversityUnited States Dafny Test Generation
Grigory FedyukovichFedyukovich, Grigory Florida State UniversityUnited States Committee Member in Program Committee within the VMCAI -track
Matthias FelleisenFelleisen, Matthias Northeastern UniversityUnited States Effectful Software Contracts
Amy FeltyFelty, Amy University of OttawaCanada Committee Member in Program Committee within the CoqPL-track
Nick FengFeng, Nick University of Toronto Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Xinyu FengFeng, Xinyu Nanjing University & HuaweiChina Committee Member in Program Committee within the POPL -track
Jerome FeretFeret, Jerome INRIA ParisFrance Committee Member in Organizing Committee within the N40AI-track
Kostas FerlesFerles, Kostas Veridise Inc.United States Web Co-Chair in Organizing Committee for POPL 2024
Carla FerreiraFerreira, Carla NOVA University LisbonPortugal Committee Member in Program Committee within the POPL -track
Francisco FerreiraFerreira, Francisco Royal Holloway, University of London PC Member in Program Committee within the CPP-track
Nathanaël FijalkowFijalkow, Nathanaël CNRS, LaBRI, and Alan Turing InstituteFrance Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic Machine Learning Meets Program Synthesis Committee Member in Program Committee within the VMCAI -track
Jean-Christophe FilliatreFilliatre, Jean-Christophe CNRSFrance Programme Committee in Program Committee within the Dafny-track
Bernd FinkbeinerFinkbeiner, Bernd CISPA Helmholtz Center for Information SecurityGermany Committee Member in Program Committee within the POPL -track
Alain FinkelFinkel, Alain ENS Paris SaclayFrance Resilience and Home-Space for WSTS
Valeria FiondaFionda, Valeria University of Calabria A direct ASP encoding for Declare
Matthew FlattFlatt, Matthew University of UtahUnited States Committee Member in Program Committee within the PADL-track
Matthew FluetFluet, Matthew Rochester Institute of TechnologyUnited States Automatic Parallelism Management
Yannick ForsterForster, Yannick InriaFrance MetaCoq Tutorial
Jeffrey S. FosterFoster, Jeffrey S. Tufts UniversityUnited States Dafny Test Generation
Nate FosterFoster, Nate Cornell UniversityUnited States TBD
Simon FowlerFowler, Simon University of GlasgowUnited Kingdom Committee Member in Program Committee within the PADL-track
Justin FrankFrank, Justin University of Maryland, College Park Generating Well-Typed Terms that are not "Useless" Indexed Types for a Statically Safe WebAssembly
Cameron FreerFreer, Cameron Massachusetts Institute of TechnologyUnited States Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets Committee Member in Program Committee within the POPL -track Committee Member in Steering Committee within the LAFI-track
Hadar FrenkelFrenkel, Hadar CISPA Helmholtz Center for Information SecurityGermany Committee Member in Program Committee within the VMCAI -track
Hannes FreyFrey, Hannes University of KoblenzGermany On the Verification of a Subgraph Construction Algorithm
Andy FriesenFriesen, Andy Roblox Towards an Unsound But Complete Type System: Work In Progress on New Non-Strict Mode for Luau
Megan FrisellaFrisella, Megan Brown University Pulse: Proof-oriented Programming in a Concurrent Separation Logic DSL in F*
Samantha FrohlichFrohlich, Samantha University of BristolUnited Kingdom Speaker in Speakers within the PLMW @ POPL-track
Aymeric FromherzFromherz, Aymeric InriaFrance Committee Member in Program Committee within the POPL -track
Dan FruminFrumin, Dan University of GroningenNetherlands Modular Denotational Semantics for Effects with Guarded Interaction Trees Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Hongfei FuFu, Hongfei Shanghai Jiao Tong UniversityChina Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving
G Philipp G. HaselwarterG. Haselwarter, Philipp Aarhus University The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
Philipp GablerGabler, Philipp Independent researcher JuliaBUGS: A Graph-Based Probabilistic Programming Language using BUGS syntax
Fabio GadducciGadducci, Fabio University of Pisa Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-Deterministic Observers
Siddhartha GadgilGadgil, Siddhartha Indian Institute of Science Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture
Emilio Jesús Gallego AriasGallego Arias, Emilio Jesús INRIAFrance Integrating Dependency Building with Document Checking in Coq
Letterio GallettaGalletta, Letterio IMT School for Advanced Studies LuccaItaly When Obfuscations Preserve Cryptographic Constant-Time
Vashti GalpinGalpin, Vashti University of EdinburghUnited Kingdom Committee Member in Programme Committee within the PROPL-track
Sankalp GambhirGambhir, Sankalp Ecole Polytechnique Federale de Lausanne (EPFL)Switzerland Interpolation and Quantifiers in Ortholattices
Moses GanardiGanardi, Moses MPI-SWSGermany Ramsey Quantifiers in Linear Arithmetics
Ronald GarciaGarcia, Ronald University of British ColumbiaCanada Committee Member in Program Committee within the POPL -track
Philippa GardnerGardner, Philippa Imperial College LondonUnited Kingdom General Chair in Organizing Committee for POPL 2024 Unified Compositional Formal Methods: Exact Separation Logic and the Gillian Platform for Correctness and Incorrectness Reasoning
Francesco GavazzoGavazzo, Francesco University of Pisa, ItalyItaly Committee Member in Program Committee within the POPL -track
Hong GeGe, Hong University of Cambridge JuliaBUGS: A Graph-Based Probabilistic Programming Language using BUGS syntax
Martin GebserGebser, Martin University of Klagenfurt, AustriaAustria Co-chair in Programme Chairs within the PADL-track
Luke GeesonGeeson, Luke University College London (UCL)United Kingdom The Future of Compiler Testing with Weak Memory Models is Relaxed
Adam GellerGeller, Adam Computer Science, University of British ColumbiaCanada Indexed Types for a Statically Safe WebAssembly
Matin GhavamiGhavami, Matin Massachusetts Institute of TechnologyUnited States MultiSPPL: extending SPPL with multivariate leaf nodes
Giorgio GhelliGhelli, Giorgio Universita di Pisa Validation of Modern JSON Schema: Formalization and Complexity
Dan GhicaGhica, Dan HuaweiUnited Kingdom Committee Member in Program Committee within the GALOP-track
Silvia GhilezanGhilezan, Silvia University of Novi Sad, Mathematical Institute SASASerbia Committee Member in Selection Committee within the POPL Student Research Competition-track
Alexis GhyselenGhyselen, Alexis University of Bologna On Model-Checking Higher-Order Effectful Programs
Roberto GiacobazziGiacobazzi, Roberto University of ArizonaUnited States Monotonicity and the Precision of Program Analysis Committee Member in Organizing Committee within the N40AI-track Committee Member in Program Committee within the POPL -track
Paolo G. GiarrussoGiarrusso, Paolo G. BedRock Systems Modularizing CPU Semantics for Virtualization
Guillaume GirolGirol, Guillaume CEA, List, Université Paris Saclay Inference of Robust Reachability Constraints
Vladimir GladshteinGladshtein, Vladimir Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Andrés GoensGoens, Andrés University of Amsterdam Guided Equality Saturation
Amir Kafshdar GoharshadyGoharshady, Amir Kafshdar Hong Kong University of Science and TechnologyHong Kong Committee Member in Program Committee within the VMCAI -track
Harrison GoldsteinGoldstein, Harrison University of PennsylvaniaUnited States Speaker in Speakers within the PLMW @ POPL-track
Eli GoldweberGoldweber, Eli University Of Michigan Testing Specifications In Dafny
Anitha GollamudiGollamudi, Anitha University of Massachusetts LowellUnited States Committee Member in Selection Committee within the POPL Student Research Competition-track
Hannah GommerstadtGommerstadt, Hannah Vassar College PLMW Chair in Organizing Committee within the PLMW @ POPL-track Committee Member in Program Committee within the PriSC-track
Léon GondelmanGondelman, Léon Aarhus UniversityDenmark Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
Georges GonthierGonthier, Georges Inria Steering Committee Member in Steering Committee within the CPP-track
Akshay GopalakrishnanGopalakrishnan, Akshay McGill University TBC
Colin GordonGordon, Colin Drexel UniversityUnited States Committee Member in Program Committee within the POPL -track
Roberta GoriGori, Roberta University of PisaItaly Committee Member in Program Committee within the Incorrectness-track
Maria I. GorinovaGorinova, Maria I. TwitterUnited Kingdom Committee Member in Program Committee within the LAFI-track
Alexey GotsmanGotsman, Alexey IMDEA Software InstituteSpain Committee Member in Program Committee within the POPL -track
Cassandra GranadeGranade, Cassandra Dual Space Solutions, LLC Committee Member in Program Committee within the PLanQC-track
Gabriel GrandGrand, Gabriel Massachusetts Institute of TechnologyUnited States Effective Sequential Monte Carlo for Language Model Probabilistic Programs
Michael GreenbergGreenberg, Michael Stevens Institute of TechnologyUnited States Industrial Relations Co-Chair in Organizing Committee for POPL 2024
Simon Oddershede GregersenGregersen, Simon Oddershede Aarhus UniversityDenmark Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
Karuna GrewalGrewal, Karuna Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Alberto GriggioGriggio, Alberto Fondazione Bruno KesslerItaly Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking
Radu GrigoreGrigore, Radu FacebookUnited Kingdom Committee Member in Program Committee within the PEPM-track
Harrison GrodinGrodin, Harrison Decalf: A Directed, Effectful Cost-Aware Logical Framework
Tobias GrosserGrosser, Tobias University of EdinburghUnited Kingdom Guided Equality Saturation
Ronghui GuGu, Ronghui Columbia UniversityUnited States Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions
Marco GuarnieriGuarnieri, Marco IMDEA Software InstituteSpain Lifting Compiler Security Properties to Stronger Attackers: the Speculation Case Steering Committee Member in Steering Committee within the PriSC-track
Simon GuilloudGuilloud, Simon École Polytechnique Fédérale de LausanneSwitzerland Interpolation and Quantifiers in Ortholattices Orthologic with Axioms
Guanchen GuoGuo, Guanchen Peking UniversityChina Fusing Direct Manipulations into Functional Programs
Gopal GuptaGupta, Gopal University of Texas at Dallas FOLD-SE: An Efficient Rule-based Machine Learning Algorithm with Scalable Explainability Using Logic Programming and Kernel-Grouping for Improving Interpretability of Convolutional Neural Networks Automated Interactive Domain-Specific Conversational Agents that Understand Human Dialogs Committee Member in Program Committee within the PADL-track
Jens Oliver GutsfeldGutsfeld, Jens Oliver Westfälische Wilhelm-Universität Münster (WWU), GermanyGermany A Navigation Logic for Recursive Programs with Dynamic Thread Creation Deciding Asynchronous Hyperproperties for Recursive Programs
Armaël GuéneauGuéneau, Armaël Université Paris-Saclay - CNRS - ENS Paris-Saclay - InriaFrance Melocoton: A Program Logic for Verified Interoperability Between OCaml and C (Invited Talk) The Logical Essence of Well-Bracketed Control Flow Thunks and Debits in Separation Logic with Time Credits
Tobias GürtlerGürtler, Tobias Saarland University, Saarland Informatics Campus Belief Programming in Partially Observable Probabilistic Environments
H Liana HadareanHadarean, Liana Amazon Web ServicesUnited States Committee Member in Program Committee within the VMCAI -track
Matthew HagueHague, Matthew Royal Holloway University of LondonUnited Kingdom Parikh's Theorem Made Symbolic String Solving for Verification
Ernst Moritz HahnHahn, Ernst Moritz Netherlands AGNES: Abstraction-guided Framework for Deep Neural Networks Security
Angus HammondHammond, Angus University of Cambridge An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic
Lasse Letager HansenHansen, Lasse Letager Aarhus University Specifying Smart Contract with Hax and ConCert A formal security analysis of Blockchain voting The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
David HarelHarel, David Weizmann Institute of Science, Israel Two Projects on Human Interaction with AI
Robert HarperHarper, Robert Carnegie Mellon UniversityUnited States Decalf: A Directed, Effectful Cost-Aware Logical Framework
Vahid HashemiHashemi, Vahid AUDI AGGermany AGNES: Abstraction-guided Framework for Deep Neural Networks Security
Daniel HausmannHausmann, Daniel University of GothenburgSweden Generic Model Checking for Modal Fixpoint Logics in COOL-MC
Klaus HavelundHavelund, Klaus NASA/Caltech Jet Propulsion LaboratoryUnited States TP-DejaVu: Combining Operational and Declarative Runtime Verification
Deyuan (Mike) HeHe, Deyuan (Mike) Princeton UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Xiao HeHe, Xiao University of Science and Technology BeijingChina Fusing Direct Manipulations into Functional Programs
Jesko Hecking-HarbuschHecking-Harbusch, Jesko Bosch ResearchGermany Formal Runtime Error Detection During Development in the Automotive Industry
Philippe HeimHeim, Philippe CISPA Helmholtz Center for Information Security Solving Infinite-State Games via Acceleration
Matthias HeizmannHeizmann, Matthias University of Freiburg, GermanyGermany Petrification: Software Model Checking for Programs with Dynamic Thread Management
Fritz HengleinHenglein, Fritz Department of Computer Science, University of Copenhagen (DIKU) and Deon DigitalDenmark Committee Member in Program Committee within the POPL -track
Paula HerberHerber, Paula University of Munster, GermanyGermany Deductive Verification of Parameterized Embedded Systems modeled in SystemC
Chris HeunenHeunen, Chris University of EdinburghUnited Kingdom With a Few Square Roots, Quantum Computing is as Easy as Pi
Brandon HewerHewer, Brandon University of Nottingham Quotient Haskell: Lightweight Quotient Types for All
Michael HicksHicks, Michael Amazon Web Services and the University of MarylandUnited States Improving the Stability of Type Safety Proofs in Dafny Cedar: A language for expressing fast, safe, and fine-grained authorization policies Committee Member in Program Committee within the POPL -track
Kesha HietalaHietala, Kesha Amazon Web ServicesUnited States Committee Member in Program Committee within the PLanQC-track PC Member in Program Committee within the CPP-track
Mathieu HilaireHilaire, Mathieu ENS Paris SaclayFrance Resilience and Home-Space for WSTS
Daniel HillerströmHillerström, Daniel Huawei Zurich Research CenterSwitzerland Soundly Handling Linearity
Jonas Kastberg HinrichsenHinrichsen, Jonas Kastberg Aarhus University, DenmarkDenmark Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement Verified Message-Passing Concurrency in Iris: Separation Logic Meets Session Types Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
Nao HirokawaHirokawa, Nao JAIST Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
Andrew K. HirschHirsch, Andrew K. University at Buffalo, SUNYUnited States Committee Member in Organizing Committee within the PLMW @ POPL-track Committee Member in Program Committee within the POPL -track
Singh HitarthHitarth, Singh Committee Member in Artifact Evaluation Committee within the VMCAI -track
Son HoHo, Son INRIAFrance Incremental Proof Development in Dafny with Module-Based Induction
Peter HoefnerHoefner, Peter Australian National University Shoggoth - A Formal Foundation for Strategic Rewriting
Jochen HoenickeHoenicke, Jochen Universität FreiburgGermany Committee Member in Program Committee within the VMCAI -track
Hossein HojjatHojjat, Hossein Tehran Institute for Advanced Studies (TeIAS)Iran Committee Member in Program Committee within the VMCAI -track
Steven HoltzenHoltzen, Steven Northeastern UniversityUnited States Towards a Categorical Model of the Lilac Separation Logic A Multi-language Approach to Probabilistic Program Inference Co-chair in Program Committee within the LAFI-track Committee Member in Organizing Committee within the LAFI-track
Chih-Duo HongHong, Chih-Duo National Chengchi UniversityTaiwan Regular Abstractions for Array Systems
Kuen-Bang Hou (Favonia)Hou (Favonia), Kuen-Bang University of MinnesotaUnited States Committee Member in Program Committee within the POPL -track PC Member in Program Committee within the CPP-track
Emil HoulborgHoulborg, Emil IT University of Copenhagen Asynchronous Reactive Programming with Modal Types in Haskell
Jon HowellHowell, Jon VMware ResearchUnited States Domesticating Automation
Cătălin HriţcuHriţcu, Cătălin MPI-SPGermany The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography Securing Verified IO Programs Against Unverified Code in F* Steering Committee Member in Steering Committee within the PriSC-track Committee Member in Program Committee within the POPL -track Steering Committee Chair in Steering Committee within the CPP-track
Jingmei HuHu, Jingmei Amazon Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Qinheping HuHu, Qinheping Amazon Web ServicesUnited States Committee Member in Program Committee within the VMCAI -track
Zhenjiang HuHu, Zhenjiang Peking UniversityChina Fusing Direct Manipulations into Functional Programs
Xinyue HuangHuang, Xinyue East China Normal UniversityChina Model-Guided Synthesis for LTL over Finite Traces
Xuejing HuangHuang, Xuejing University of Hong KongChina Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Marieke HuismanHuisman, Marieke University of TwenteNetherlands Deductive Verification of Parameterized Embedded Systems modeled in SystemC Committee Member in Program Committee within the VMCAI -track
Merlin HummlHumml, Merlin Friedrich-Alexander Universität Erlangen-NürnbergGermany Generic Model Checking for Modal Fixpoint Logics in COOL-MC
Mathieu HuotHuot, Mathieu MIT MultiSPPL: extending SPPL with multivariate leaf nodes Reverse mode ADEV via YOLO: tangent estimators transpose to gradient estimators
Chung-Kil HurHur, Chung-Kil Seoul National UniversitySouth Korea In-order execution nails every weak memory behavior
Graham HuttonHutton, Graham University of Nottingham, UKUnited Kingdom Quotient Haskell: Lightweight Quotient Types for All
Sander HuyghebaertHuyghebaert, Sander Vrije Universiteit Brussel Secure Calling Conventions for CHERI Capability Machines in Practice (Work in Progress) Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Benjamin Salling HvassHvass, Benjamin Salling Aarhus University The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
I Giovambattista IanniIanni, Giovambattista University of Calabria, ItalyItaly Rethinking Answer Set Programming Templates Forgetting Techniques for Optimizing ASP-based Stream Reasoning
Antonio IeloIelo, Antonio University of Calabria A direct ASP encoding for Declare
Emilio IncertoIncerto, Emilio IMT School for Advanced Studies Lucca Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures
Daniela InclezanInclezan, Daniela Miami UniversityUnited States Committee Member in Program Committee within the PADL-track
Apoorv IngleIngle, Apoorv University of IowaUnited States Video Chair in Organizing Committee for POPL 2024
Lef IoannidisIoannidis, Lef University of PennsylvaniaUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
J Adham JabarinJabarin, Adham Ben Gurion University The Complex(ity) Landscape of Checking Infinite Descent
Guilhem JaberJaber, Guilhem Nantes UniversitéFrance Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the GALOP-track
Jules JacobsJacobs, Jules Radboud University Nijmegen Verified Message-Passing Concurrency in Iris: Separation Logic Meets Session Types Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing
Swen JacobsJacobs, Swen CISPAGermany Parameterized Verification of Disjunctive Timed Networks Automatic and Incremental Repair for Speculative Information Leaks
Alec JacobsonJacobson, Alec University of Toronto Sparse Differentiation in Computer Graphics
Suresh JagannathanJagannathan, Suresh Purdue UniversityUnited States Type-Based Incorrectness Reasoning
Georges-Axel JaloyanJaloyan, Georges-Axel Amazon Web Services Enhancing Proof Stability
Tomi JanhunenJanhunen, Tomi Tampere UniversityFinland Committee Member in Program Committee within the PADL-track
Patrik JanssonJansson, Patrik Chalmers University of TechnologySweden Committee Member in Programme Committee within the PROPL-track
Prasad JayantiJayanti, Prasad Department of Computer Science, Dartmouth College, USA A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability
Siddhartha JayantiJayanti, Siddhartha Google Research A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability
Alan JeffreyJeffrey, Alan RobloxUnited States Towards an Unsound But Complete Type System: Work In Progress on New Non-Strict Mode for Luau
Thomas P. JensenJensen, Thomas P. INRIA Rennes Committee Member in Program Committee within the PriSC-track
Artur JezJez, Artur University of Wroclaw Parikh's Theorem Made Symbolic String Solving for Verification
Ranjit JhalaJhala, Ranjit University of California at San DiegoUnited States Mechanizing Refinement Types
Limin JiaJia, Limin Carnegie Mellon University Automatically Enforcing Rust Trait Properties Committee Member in Program Committee within the POPL -track
Songlin JiaJia, Songlin Purdue University, USAUnited States Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs
Philip Johnson-FreydJohnson-Freyd, Philip Sandia National Laboratories Towards a Categorical Model of the Lilac Separation Logic A Formalization of Core Why3 in Coq
Joost J. JoostenJoosten, Joost J. University of Barcelona UTC time, formally verified
Jacques-Henri JourdanJourdan, Jacques-Henri CNR, LMFFrance Thunks and Debits in Separation Logic with Time Credits Committee Member in Program Committee within the WITS-track
Ralf JungJung, Ralf ETH ZürichSwitzerland Committee Member in Program Committee within the CoqPL-track Committee Member in Selection Committee within the POPL Student Research Competition-track
K Robin KaarsgaardKaarsgaard, Robin University of Southern DenmarkDenmark With a Few Square Roots, Quantum Computing is as Easy as Pi Committee Member in Program Committee within the PLanQC-track
Anan KabahaKabaha, Anan Technion, Israel Institute of TechnologyIsrael Verification of Neural Networks’ Local Differential Classification Privacy
Younesse KaddarKaddar, Younesse University of OxfordUnited Kingdom Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets
Jan-Oliver KaiserKaiser, Jan-Oliver BedRock Systems, MPI-SWSGermany Committee Member in Program Committee within the CoqPL-track
Shoaib KamilKamil, Shoaib Adobe Research Sparse Differentiation in Computer Graphics
Benjamin Lucien KaminskiKaminski, Benjamin Lucien Saarland University; University College LondonGermany Hoare-Like Triples and Kleene Algebras with Top and Tests Quantitative Weakest Hyper Pre Caesar: A Verifier for Probabilistic Programs Belief Programming in Partially Observable Probabilistic Environments Committee Member in Program Committee within the LAFI-track
Ohad KammarKammar, Ohad University of EdinburghUnited Kingdom LGBTQ+ Host in Organizing Committee for POPL 2024 Shoggoth - A Formal Foundation for Strategic Rewriting Foundations of Type-Driven Probabilistic Modelling Committee Member in Diversity, Equity, and Inclusion Committee within the POPL Diversity, Equity and Inclusion-track Committee Member in Selection Committee within the POPL Student Research Competition-track Committee Member in Steering Committee within the LAFI-track
Jeehoon KangKang, Jeehoon KAISTSouth Korea Committee Member in Program Committee within the POPL -track
Ambrus KaposiKaposi, Ambrus Eötvös Loránd University Internal parametricity, without an interval
Manos KapritsosKapritsos, Manos University of Michigan, USA Testing Specifications In Dafny
Nat KarmiosKarmios, Nat Imperial College LondonUnited Kingdom Unified Compositional Formal Methods: Exact Separation Logic and the Gillian Platform for Correctness and Incorrectness Reasoning
Shyam KarraKarra, Shyam CISPAGermany Parameterized Verification of Disjunctive Timed Networks
Jacek KarwowskiKarwowski, Jacek University of OxfordPoland Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets
Joost-Pieter KatoenKatoen, Joost-Pieter RWTH Aachen UniversityGermany Caesar: A Verifier for Probabilistic Programs Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs Committee Member in Program Committee within the VMCAI -track
Panagiotis KatsarosKatsaros, Panagiotis Aristotle University of ThessalonikiGreece TP-DejaVu: Combining Operational and Declarative Runtime Verification
Guy KatzKatz, Guy Hebrew UniversityIsrael Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training
Daniela KaufmannKaufmann, Daniela TU Wien Committee Member in Program Committee within the VMCAI -track
Fuga KawamataKawamata, Fuga Waseda University Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers
Gabriele KellerKeller, Gabriele Utrecht UniversityNetherlands Committee Member in Organizing Committee within the PEPM-track
Ariel KellisonKellison, Ariel Cornell UniversityUnited States VCFloat2: Floating-point error analysis in Coq
Steven KeuchelKeuchel, Steven Vrije Universiteit BrusselBelgium Secure Calling Conventions for CHERI Capability Machines in Practice (Work in Progress)
Mohammad Wahiduzzaman KhanKhan, Mohammad Wahiduzzaman UL Lafayette Type-based Gradual Typing Performance Optimization
Artem KhyzhaKhyzha, Artem Tel Aviv University, IsraelUkraine Arm Architecture and Formal Artifacts: Memory Model and Instruction Semantics
Oisín KidneyKidney, Oisín Imperial College LondonUnited Kingdom Algebraic Effects Meet Hoare Logic in Cubical Agda
Dohan KimKim, Dohan University of Innsbruck Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
Zachary KincaidKincaid, Zachary Princeton UniversityUnited States Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis Committee Member in Program Committee within the POPL -track
Dominik KirstKirst, Dominik Ben-Gurion University of the Negev A mechanised and constructive reverse analysis of soundness and completeness of bi-intuitionistic logic
Gerwin KleinKlein, Gerwin CSIRO's Data61 and UNSW SydneyAustralia Committee Member in Steering Committee within the CPP-track
Vasileios KlimisKlimis, Vasileios Queen Mary University of London TBC
Bartek KlinKlin, Bartek University of OxfordUnited Kingdom Polyregular functions on unordered trees of bounded height
Dominik KlumppKlumpp, Dominik University of FreiburgGermany Petrification: Software Model Checking for Programs with Dynamic Thread Management Commutativity Simplifies Proofs of Parameterized Programs Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Hsiang-Shang ‘Josh’ KoKo, Hsiang-Shang ‘Josh’ Institute of Information Science, Academia SinicaTaiwan PC Member in Program Committee within the CPP-track
Naoki KobayashiKobayashi, Naoki University of TokyoJapan Borrowable Fractional Ownership Types for Verification
Thomas KoehlerKoehler, Thomas INRIAFrance Guided Equality Saturation
Jérémie KoenigKoenig, Jérémie Yale UniversityUnited States Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules
Wen KokkeKokke, Wen University of Edinburgh PC Member in Program Committee within the CPP-track
Ekaterina KomendantskayaKomendantskaya, Ekaterina Heriot-Watt University and Southampton UniversityUnited Kingdom Whats and Whys of Neural Network Verification (A Declarative Programming Perspective)
Joomy KorkutKorkut, Joomy Princeton UniversityUnited States Committee Member in Artifact Evaluation Committee within the VMCAI -track
Laura KovácsKovács, Laura TU WienAustria Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs
Robbert KrebbersKrebbers, Robbert Radboud University NijmegenNetherlands Unification for Subformula Linking under Quantifiers Verified Message-Passing Concurrency in Iris: Separation Logic Meets Session Types Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing Steering Committee Member in Steering Committee within the CPP-track
Jacco KrijnenKrijnen, Jacco Utrecht University InducTeX: A MetaCoq plugin for typesetting inductive definitions
Shankaranarayanan KrishnaKrishna, Shankaranarayanan IIT Bombay, India On-The-Fly Static Analysis via Dynamic Bidirected Dyck Reachability How Hard is Weak-Memory Testing?
Shriram KrishnamurthiKrishnamurthi, Shriram Brown UniversityUnited States A Core Calculus for Documents
Neel KrishnaswamiKrishnaswami, Neel University of CambridgeUnited Kingdom Student Research Competition Co-Chair in Organizing Committee for POPL 2024 Speaker in Speakers within the PLMW @ POPL-track Co-chair in Selection Committee within the POPL Student Research Competition-track
Matthis KruseKruse, Matthis CISPA Helmholtz Center for Information SecurityGermany Secure Composition of SPECTRE Mitigations
Nikolai KudasovKudasov, Nikolai Innopolis University, RussiaRussia Formalizing the ∞-categorical Yoneda lemma
Burcu Kulahcioglu OzkanKulahcioglu Ozkan, Burcu Delft University of TechnologyNetherlands Committee Member in Program Committee within the VMCAI -track
Viktor KunčakKunčak, Viktor EPFL, SwitzerlandSwitzerland Interpolation and Quantifiers in Ortholattices Orthologic with Axioms
Bettina KönighoferKönighofer, Bettina Committee Member in Program Committee within the VMCAI -track
Robert KünnemannKünnemann, Robert CISPA Helmholtz Center for Information Security Computational-Bounded Robust Compilation and Universally Composable Security
L Yash LadLad, Yash University of Utah Implementation and Synthesis of Math Library Functions
Ralf LaemmelLaemmel, Ralf Facebook London Committee Member in Program Committee within the PEPM-track
Ambroise LafontLafont, Ambroise Inria, France A diagram editor to mechanize categorical proofs
Ori LahavLahav, Ori Tel Aviv UniversityIsrael A case against semantic dependencies Co-chair in Program Committee within the VMCAI -track
Jim LairdLaird, Jim University of BathUnited Kingdom Committee Member in Program Committee within the GALOP-track
Roman LakenbrinkLakenbrink, Roman University of MünsterGermany A Navigation Logic for Recursive Programs with Dynamic Thread Creation
Aniket LalLal, Aniket IIT Bombay On-The-Fly Static Analysis via Dynamic Bidirected Dyck Reachability
Peter LammichLammich, Peter The University of Manchester PC Member in Program Committee within the CPP-track
Leonidas LampropoulosLampropoulos, Leonidas University of Maryland, College ParkGreece Artifact Evaluation Co-Chair in Organizing Committee for POPL 2024 Generating Well-Typed Terms that are not "Useless" PLMW Co-Chair in Organizing Committee within the PLMW @ POPL-track
Vincent LaporteLaporte, Vincent IMDEA Software Institute, Spain Committee Member in Program Committee within the PriSC-track
Andrea LattuadaLattuada, Andrea VMware ResearchSwitzerland Domesticating Automation Programme Committee in Program Committee within the Dafny-track
Jacob LaurelLaurel, Jacob University of Illinois at Urbana-ChampaignUnited States Abstract Interpretation for Automatic Differentiation
Mickaël LaurentLaurent, Mickaël Université de ParisFrance Polymorphic Type Inference for Dynamic Languages
Didier Le BotlanLe Botlan, Didier LAAS-CNRS, INSA-ToulouseFrance Project and Conquer: Fast Quantifier Elimination for Checking Petri Nets Reachability
K. Rustan M. LeinoLeino, K. Rustan M. AmazonUnited States Steering Committee Chair in Steering Committee within the Dafny-track
Meven Lennon-BertrandLennon-Bertrand, Meven University of CambridgeUnited Kingdom Martin-Löf à la Coq MetaCoq Tutorial
Rodolphe LepigreLepigre, Rodolphe BedRock SystemsGermany Committee Member in Program Committee within the POPL -track
Xavier LeroyLeroy, Xavier Collège de FranceFrance Well-founded recursion done right
Martin LesterLester, Martin University of ReadingUnited Kingdom Cutting the Cake Into Crumbs: Verifying Envy-Free Cake-Cutting Protocols using Bounded Integer Arithmetic
Reese LevineLevine, Reese University of California at Santa CruzUnited States Evolving Weak Memory Models for Evolving Architectures
Alexander K. LewLew, Alexander K. Massachusetts Institute of TechnologyUnited States Toward Probabilistic Coarse-to-Fine Program Synthesis Reverse mode ADEV via YOLO: tangent estimators transpose to gradient estimators Effective Sequential Monte Carlo for Language Model Probabilistic Programs
Bohan LiLi, Bohan State Key Laboratory of Computer Science Institute of Software, Chinese Academy of Sciences, Beijing, ChinaChina Efficient Local Search for Nonlinear Real Arithmetic
Elaine LiLi, Elaine NYUUnited States Programme Committee in Program Committee within the Dafny-track
Guanyan LiLi, Guanyan University of Oxford Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving
Jianwen LiLi, Jianwen East China Normal University, ChinaChina Model-Guided Synthesis for LTL over Finite Traces
Jiaying LILI, Jiaying Microsoft ReLU Hull Approximation
John LiLi, John Northeastern University Towards a Categorical Model of the Lilac Separation Logic
Xiang LiLi, Xiang University of Michigan, Ann ArborUnited States Efficient Bottom-Up Synthesis for Programs with Local Variables
Yao LiLi, Yao Portland State UniversityUnited States Committee Member in Selection Committee within the POPL Student Research Competition-track
Yishuai LiLi, Yishuai Alibaba GroupChina Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Yongkang LiLi, Yongkang East China Normal UniversityChina Model-Guided Synthesis for LTL over Finite Traces
Chencheng LiangLiang, Chencheng Uppsala UniversitySweden Boosting Constrained Horn Solving by Unsat Core Learning
Hongjin LiangLiang, Hongjin Nanjing UniversityChina Committee Member in Program Committee within the PriSC-track
Anthony Widjaja LinLin, Anthony Widjaja TU Kaiserslautern; MPI-SWSGermany Parikh's Theorem Made Symbolic String Solving for Verification Ramsey Quantifiers in Linear Arithmetics Regular Abstractions for Array Systems
Sam LindleyLindley, Sam University of EdinburghUnited Kingdom Soundly Handling Linearity
Pengyu LiuLiu, Pengyu Tsinghua University SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog Compilation
Shuyang LiuLiu, Shuyang UCLA Committee Member in Artifact Evaluation Committee within the VMCAI -track
Si LiuLiu, Si ETH ZurichSwitzerland Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training
Y. Annie LiuLiu, Y. Annie Stony Brook UniversityUnited States Committee Member in Program Committee within the PADL-track
Yiyun LiuLiu, Yiyun University of Maryland at College Park Internalizing Indistinguishability with Dependent Types
Zongyuan LiuLiu, Zongyuan Aarhus UniversityDenmark An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic
Francesco LogozzoLogozzo, Francesco FacebookUnited States Committee Member in Organizing Committee within the N40AI-track
Giuseppe LomurnoLomurno, Giuseppe University of Pisa, Italy Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-Deterministic Observers
Sarah LoosLoos, Sarah Google PC Member in Program Committee within the CPP-track
Anna LukinaLukina, Anna TU Delft Committee Member in Program Committee within the VMCAI -track
Andreas LööwLööw, Andreas Imperial College London Unified Compositional Formal Methods: Exact Separation Logic and the Gillian Platform for Correctness and Incorrectness Reasoning
M Zhongkui MaMa, Zhongkui The University of Queensland ReLU Hull Approximation
Anil MadhavapeddyMadhavapeddy, Anil University of Cambridge, UKUnited Kingdom Co-chair in Programme Committee within the PROPL-track Co-chair in Chairs within the PROPL-track
P. MadhusudanMadhusudan, P. University of Illinois at Urbana-ChampaignUnited States Automated Datastructure Verification using Unfoldings and SMT Solving: Foundations and FO-Completeness
Assia MahboubiMahboubi, Assia INRIAFrance Committee Member in Program Committee within the POPL -track
Kenji MaillardMaillard, Kenji Inria – LS2N, Université de NantesFrance Martin-Löf à la Coq
Rupak MajumdarMajumdar, Rupak MPI-SWSGermany Reachability in Continuous Pushdown VASS Positive Almost-Sure Termination – Complexity and Proof Rules
Petar MaksimovićMaksimović, Petar Imperial College London, UK Unified Compositional Formal Methods: Exact Separation Logic and the Gillian Platform for Correctness and Incorrectness Reasoning
Gregory MalechaMalecha, Gregory BedRock SystemsUnited States Towards Modular Specification and Verification of Concurrent Hypervisor-based Isolation Modularizing CPU Semantics for Virtualization Committee Member in Program Committee within the POPL -track
Konstantinos MamourasMamouras, Konstantinos Rice UniversityUnited States Efficient Matching of Regular Expressions with Lookaround Assertions
Vikash K. MansinghkaMansinghka, Vikash K. Massachusetts Institute of TechnologyUnited States MultiSPPL: extending SPPL with multivariate leaf nodes Toward Probabilistic Coarse-to-Fine Program Synthesis Reverse mode ADEV via YOLO: tangent estimators transpose to gradient estimators Effective Sequential Monte Carlo for Language Model Probabilistic Programs
William ManskyMansky, William University of Illinois ChicagoUnited States Compositional Verification of Concurrent C Programs with Search Structure Templates An Iris Instance for Verifying CompCert C Programs Committee Member in Program Committee within the POPL -track
Luc MarangetMaranget, Luc InriaFrance Arm Architecture and Formal Artifacts: Memory Model and Instruction Semantics
Raef MaroofMaroof, Raef University of Michigan Total Type Error Localization and Recovery with Holes
Lina MarssoMarsso, Lina University of TorontoCanada Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Guido MartínezMartínez, Guido Microsoft ResearchUnited States Pulse: Proof-oriented Programming in a Concurrent Separation Logic DSL in F* Securing Verified IO Programs Against Unverified Code in F*
Christoph MathejaMatheja, Christoph DTUDenmark Workshops Co-Chair in Organizing Committee for POPL 2024 Caesar: A Verifier for Probabilistic Programs
Umang MathurMathur, Umang National University of SingaporeSingapore Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic Predictive Monitoring against Pattern Regular Languages Coarser Equivalences for Causal Concurrency How Hard is Weak-Memory Testing?
Théo MatriconMatricon, Théo CNRS, LaBRI, University of BordeauxFrance Committee Member in Artifact Evaluation Committee within the VMCAI -track
Kazutaka MatsudaMatsuda, Kazutaka Tohoku UniversityJapan Committee Member in Program Committee within the PEPM-track
Yusuke MatsushitaMatsushita, Yusuke The University of Tokyo Borrowable Fractional Ownership Types for Verification
Ralph MatthesMatthes, Ralph IRIT (CNRS and Univ. of Toulouse) Displayed Monoidal Categories for the Semantics of Linear Logic
McKenna McCallMcCall, McKenna Committee Member in Program Committee within the PriSC-track
Paul E. McKenneyMcKenney, Paul E. Compilers should get over themselves and respect semantic dependencies!
Sean McLaughlinMcLaughlin, Sean Amazon Web Services Enhancing Proof Stability Portfolio Solving for Dafny
Aastha MehtaMehta, Aastha The University of British Columbia Microarchitectural Side-Channel Mitigations for Serverless Applications
Wolfgang MeierMeier, Wolfgang CertiCoq-Wasm: Verified compilation from Coq to WebAssembly
Orestis MelkonianMelkonian, Orestis University of EdinburghUnited Kingdom Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Stephen MellMell, Stephen University of Pennsylvania Optimal Program Synthesis via Abstract Interpretation
Paul-André MellièsMelliès, Paul-André CNRS; Université de ParisFrance Committee Member in Program Committee within the GALOP-track
Alexandra MendesMendes, Alexandra Faculty of Engineering, University of Porto & INESC TECPortugal Committee Member in Program Committee within the PADL-track
Eric MercerMercer, Eric Brigham Young UniversityUnited States Verifying Dafny Contract Integrity
Denis MerigouxMerigoux, Denis INRIAFrance Committee Member in Program Committee within the POPL -track
Roland MeyerMeyer, Roland TU BraunschweigGermany Committee Member in Program Committee within the VMCAI -track
Jesse MichelMichel, Jesse Massachusetts Institute of Technology Sparse Differentiation in Computer Graphics
Marco MilaneseMilanese, Marco Sorbonne UniversityFrance Generation of Violation Witnesses by Under-Approximating Abstract Interpretation
Mae MilanoMilano, Mae University of California at BerkeleyUnited States Speaker in Speakers within the PLMW @ POPL-track Committee Member in Program Committee within the POPL -track
Dale MillerMiller, Dale INRIA Saclay and LIX/Institut Polytechnique de ParisFrance Steering Committee Member in Steering Committee within the CPP-track
Anders MiltnerMiltner, Anders Simon Fraser UniversityCanada Workshops Co-Chair in Organizing Committee for POPL 2024
Antoine MinéMiné, Antoine Sorbonne UniversitéFrance Generation of Violation Witnesses by Under-Approximating Abstract Interpretation Sound Abstract Nonexploitability Analysis Committee Member in Organizing Committee within the N40AI-track
Sasa MisailovicMisailovic, Sasa University of Illinois at Urbana-ChampaignUnited States Abstract Interpretation for Automatic Differentiation
Meghana MissulaMissula, Meghana The University of Texas at Austin Programming-by-Demonstration for Long-Horizon Robot Tasks
Alexandre MoineMoine, Alexandre InriaFrance DisLog: A Separation Logic for Disentanglement
Alberto MomiglianoMomigliano, Alberto Università degli Studi di Milano PC Member in Program Committee within the CPP-track
David MonniauxMonniaux, David Université Grenoble Alpes - CNRS - Grenoble INP - VerimagFrance Memory simulations, security and optimization in a verified compiler Committee Member in Program Committee within the VMCAI -track
Raúl E. MontiMonti, Raúl E. University of TwenteNetherlands Deductive Verification of Parameterized Embedded Systems modeled in SystemC
Simon W. MooreMoore, Simon W. University of Cambridge Committee Member in Organizing Committee within the POCL-track
Marcel MoosbruggerMoosbrugger, Marcel TU WienAustria Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs
Andreia MordidoMordido, Andreia LASIGE, University of LisbonPortugal Parametric Subtyping for Structural Parametric Polymorphism
J. Garrett MorrisMorris, J. Garrett University of IowaUnited States Soundly Handling Linearity
Sean MossMoss, Sean University of Oxford Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets
Laurent MounierMounier, Laurent Université Grenoble AlpesFrance Function synthesis for maximizing model counting
Cameron MoyMoy, Cameron Northeastern UniversityUnited States Effectful Software Contracts
Kevin MuMu, Kevin University of Washington Sparse Differentiation in Computer Graphics
Eric MugnierMugnier, Eric University of California San Diego Portfolio Solving for Dafny
Ike MulderMulder, Ike Radboud University NijmegenNetherlands Unification for Subformula Linking under Quantifiers
Stefan K. MullerMuller, Stefan K. Illinois Institute of TechnologyUnited States Pipelines and Beyond: Graph Types for ADTs with Futures Disentanglement with Futures, State, and Interaction Committee Member in Program Committee within the POPL -track
Cesar MunozMunoz, Cesar NASAUnited States A Temporal Differential Dynamic Logic Formal Embedding
Adithya MuraliMurali, Adithya University of Illinois at Urbana-ChampaignUnited States Automated Datastructure Verification using Unfoldings and SMT Solving: Foundations and FO-Completeness
Andrzej MurawskiMurawski, Andrzej University of OxfordUnited Kingdom Guaranteed Bounds for Discrete Probabilistic Programs with Loops via Generating Functions Committee Member in Organising Committee within the GALOP-track Committee Member in Program Committee within the GALOP-track
Toby MurrayMurray, Toby University of MelbourneAustralia Committee Member in Program Committee within the Incorrectness-track
Andrew MyersMyers, Andrew Cornell University Steering Committee Member in Steering Committee within the PriSC-track
Magnus O. MyreenMyreen, Magnus O. Chalmers University of Technology Committee Member in Program Committee within the PADL-track PC Member in Program Committee within the CPP-track
Glen MévelMével, Glen Thunks and Debits in Separation Logic with Time Credits
Peter MüllerMüller, Peter ETH ZurichSwitzerland Programme Committee in Program Committee within the Dafny-track Committee Member in Program Committee within the POPL -track
Markus Müller-OlmMüller-Olm, Markus University of MünsterGermany A Navigation Logic for Recursive Programs with Dynamic Thread Creation Deciding Asynchronous Hyperproperties for Recursive Programs
Julian MüllnerMüllner, Julian TU Wien Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs
N Takashi NakayamaNakayama, Takashi The University of TokyoJapan Borrowable Fractional Ownership Types for Verification
Kedar NamjoshiNamjoshi, Kedar Nokia Bell LabsUnited States Committee Member in Program Committee within the VMCAI -track
Daniele Nantes-SobrinhoNantes-Sobrinho, Daniele Imperial College LondonUnited Kingdom Diversity, Equity, and Inclusion Co-Chair in Organizing Committee for POPL 2024 Unified Compositional Formal Methods: Exact Separation Logic and the Gillian Platform for Correctness and Incorrectness Reasoning Co-chair in Diversity, Equity, and Inclusion Committee within the POPL Diversity, Equity and Inclusion-track
Satya Prakash NayakNayak, Satya Prakash Max Planck Institute for Software Systems (MPI-SWS)Germany Solving Two-Player Games under Progress Assumptions
Daniel NeiderNeider, Daniel Technical University of Dortmund, GermanyGermany Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic
Max S. NewNew, Max S. University of MichiganUnited States Committee Member in Program Committee within the POPL -track
Duc-Than NguyenNguyen, Duc-Than University of Illinois at ChicagoUnited States Compositional Verification of Concurrent C Programs with Search Structure Templates
Kim NguyễnNguyễn, Kim Université Paris-SaclayFrance Polymorphic Type Inference for Dynamic Languages
Jason NiehNieh, Jason Columbia University Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions
Eske Hoy NielsenNielsen, Eske Hoy Aarhus University A formal security analysis of Blockchain voting
Tobias NießenNießen, Tobias TU Wien Finding counterexamples to ∀∃ hyperproperties
Abel NietoNieto, Abel Aarhus UniversityDenmark Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
Nikos NikolerisNikoleris, Nikos Arm Research Arm Architecture and Formal Artifacts: Memory Model and Instruction Semantics
Tobias NipkowNipkow, Tobias Technische Universität München Steering Committee Member in Steering Committee within the CPP-track
Lars NitzkeNitzke, Lars University of FreiburgGermany Petrification: Software Model Checking for Programs with Dynamic Thread Management
Yue NiuNiu, Yue Carnegie Mellon UniversityUnited States Decalf: A Directed, Effectful Cost-Aware Logical Framework
James NobleNoble, James Creative Research & ProgrammingNew Zealand Work in Progress: Modelling Incorrect Programs in the Open World with Dafny Colouring Flags with Dafny & Idris Learn 'em Dafny
Ulf NorellNorell, Ulf Gothenburg UniversitySweden Committee Member in Program Committee within the POPL -track
Michael NorrishNorrish, Michael Australian National UniversityAustralia PC Member in Program Committee within the CPP-track
Paige Randall NorthNorth, Paige Randall Utrecht University Univalent Double Categories PC Member in Program Committee within the CPP-track
Filippo Alberto Edoardo Nuccio Mortarino Majno di CapriglioNuccio Mortarino Majno di Capriglio, Filippo Alberto Edoardo Université Jean Monnet Saint-ÉtienneFrance A Formalization of Complete Discrete Valuation Rings and Local Fields
Fernando Lucatelli NunesNunes, Fernando Lucatelli Utrecht University Homomorphic Reverse Differentiation of Iteration
Andreas NuytsNuyts, Andreas KU Leuven, BelgiumBelgium Internal and Observational Parametricity for Cubical Agda
O Liam O'ConnorO'Connor, Liam University of EdinburghUnited Kingdom Shoggoth - A Formal Foundation for Strategic Rewriting Committee Member in Program Committee within the PEPM-track
Peter W. O'HearnO'Hearn, Peter W. Meta; University College LondonUnited Kingdom Committee Member in Program Committee within the Incorrectness-track
Hugo O'KeeffeO'Keeffe, Hugo ARM Arm Architecture and Formal Artifacts: Memory Model and Instruction Semantics
Sabine OechsnerOechsner, Sabine University of EdinburghUnited Kingdom Committee Member in Selection Committee within the POPL Student Research Competition-track
Christoph OhremOhrem, Christoph University of MünsterGermany A Navigation Logic for Recursive Programs with Dynamic Thread Creation Deciding Asynchronous Hyperproperties for Recursive Programs
Emilia OikarinenOikarinen, Emilia University of HelsinkiFinland Committee Member in Program Committee within the PADL-track
Cyrus OmarOmar, Cyrus University of MichiganUnited States Total Type Error Localization and Recovery with Holes
Moran OmerOmer, Moran Bar Ilan University, IsraelIsrael TP-DejaVu: Combining Operational and Declarative Runtime Verification
C.-H. Luke OngOng, C.-H. Luke NTU Guaranteed Bounds for Discrete Probabilistic Programs with Loops via Generating Functions A slice sampler for the Indian Buffet Process: expressivity in nonparametric probabilistic programming Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving
Dominic OrchardOrchard, Dominic University of Kent, UK and University of Cambridge, UKUnited Kingdom Co-chair in Programme Committee within the PROPL-track Committee Member in Chairs within the PROPL-track
P Francesco PacenzaPacenza, Francesco Department of Mathematics and Computer Science, University of CalabriaItaly Rethinking Answer Set Programming Templates Forgetting Techniques for Optimizing ASP-based Stream Reasoning
Parth PadalkarPadalkar, Parth THE UNIVERSITY OF TEXAS AT DALLAS Using Logic Programming and Kernel-Grouping for Improving Interpretability of Convolutional Neural Networks Automated Interactive Domain-Specific Conversational Agents that Understand Human Dialogs
Oded PadonPadon, Oded VMware ResearchUnited States Domesticating Automation CLOVER: Closed-Loop Verifiable Code Generation An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
Shankara PailoorPailoor, Shankara University of Texas at AustinUnited States Semantic Code Refactoring for Abstract Data Types
Abhinandan PalPal, Abhinandan University of BirminghamUnited Kingdom Abstract Interpretation-Based Feature Importance for Support Vector Machines
Jens PalsbergPalsberg, Jens University of California, Los Angeles (UCLA)United States Committee Member in Program Committee within the VMCAI -track
Zhiyi PanPan, Zhiyi University of Michigan Total Type Error Localization and Recovery with Holes
Pavel PanchekhaPanchekha, Pavel University of UtahUnited States Implementation and Synthesis of Math Library Functions
Hugo PaquetPaquet, Hugo LIPN, Université Sorbonne Paris NordFrance A slice sampler for the Indian Buffet Process: expressivity in nonparametric probabilistic programming Committee Member in Program Committee within the GALOP-track Committee Member in Program Committee within the LAFI-track
Seung Hoon ParkPark, Seung Hoon Imperial College London Unified Compositional Formal Methods: Exact Separation Logic and the Gillian Platform for Correctness and Incorrectness Reasoning
Matthew J. ParkinsonParkinson, Matthew J. Microsoft Azure ResearchUnited Kingdom Some things I wish I hadn’t seen
Francesco ParoliniParolini, Francesco Sorbonne UniversitéFrance Sound Abstract Nonexploitability Analysis
Lionel ParreauxParreaux, Lionel Hong Kong University of Science and TechnologyChina When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism
Marco PatrignaniPatrignani, Marco University of TrentoItaly Session Chair of Session 1 (part of PriSC) Introduction Steering Committee Member in Steering Committee within the PriSC-track PC Chair in Program Committee within the PriSC-track
Noah PattonPatton, Noah The University of Texas at Austin Programming-by-Demonstration for Long-Horizon Robot Tasks
Christine Paulin-MohringPaulin-Mohring, Christine Université Paris-Saclay PC Member in Program Committee within the CPP-track
Lawrence PaulsonPaulson, Lawrence University of CambridgeUnited Kingdom Formal Probabilistic Methods for Combinatorial Structures in Isabelle/HOL
Daniele PautassoPautasso, Daniele Università di Torino Higher Order Bayesian Networks, Exactly
Andreas PavlogiannisPavlogiannis, Andreas Aarhus UniversityDenmark On-The-Fly Static Analysis via Dynamic Bidirected Dyck Reachability How Hard is Weak-Memory Testing? Committee Member in Program Committee within the POPL -track
Jennifer PaykinPaykin, Jennifer Intel LabsUnited States Committee Member in Program Committee within the PLanQC-track Committee Member in Program Committee within the POPL -track
Doron PeledPeled, Doron Bar Ilan UniversityIsrael TP-DejaVu: Combining Operational and Declarative Runtime Verification
Hila PelegPeleg, Hila TechnionIsrael Committee Member in Program Committee within the POPL -track
Yuxiang PengPeng, Yuxiang University of MarylandUnited States A Case for Synthesis of Recursive Quantum Unitary Programs SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog Compilation Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Simona PerriPerri, Simona University of Calabria, Italy Forgetting Techniques for Optimizing ASP-based Stream Reasoning
Simon Peyton JonesPeyton Jones, Simon Epic Games United Kingdom Committee Member in Program Committee within the POPL -track
Frank PfenningPfenning, Frank Carnegie Mellon University, USA Parametric Subtyping for Structural Parametric Polymorphism
Jean Pichon-PharabodPichon-Pharabod, Jean Aarhus UniversityDenmark CertiCoq-Wasm: Verified compilation from Coq to WebAssembly An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic Committee Member in Program Committee within the POPL -track
Brigitte PientkaPientka, Brigitte McGill UniversityCanada PC Chair in Program Committee within the CPP-track Steering Committee Member in Steering Committee within the CPP-track PC Chair in Organizing Committee within the CPP-track
Benjamin C. PiercePierce, Benjamin C. University of PennsylvaniaUnited States Committee Member in Programme Committee within the PROPL-track
Frank PiessensPiessens, Frank KU Leuven Compiler Support for Control-Flow Linearization Using Architectural Mimicry Steering Committee Member in Steering Committee within the PriSC-track
Clément Pit-ClaudelPit-Claudel, Clément EPFLUnited States Incremental Proof Development in Dafny with Module-Based Induction Committee Member in Program Committee within the PriSC-track
Andrew M. PittsPitts, Andrew M. University of Cambridge Committee Member in Program Committee within the POPL -track
Gordon PlotkinPlotkin, Gordon Google Effect Handlers for Choice-Based Learning Homomorphic Reverse Differentiation of Iteration
Andreas PodelskiPodelski, Andreas University of FreiburgGermany Commutativity Simplifies Proofs of Parameterized Programs
Anton PodkopaevPodkopaev, Anton JetBrains Research, Constructor UniversityNetherlands Committee Member in Program Committee within the POPL -track
Piotr PolesiukPolesiuk, Piotr University of Wrocław Functorial Syntax for All
Elizabeth PolgreenPolgreen, Elizabeth University of EdinburghUnited Kingdom Committee Member in Program Committee within the VMCAI -track
Nadia PolikarpovaPolikarpova, Nadia University of California at San DiegoUnited States Programme Committee in Program Committee within the Dafny-track
Enrico PontelliPontelli, Enrico New Mexico State University Committee Member in Program Committee within the PADL-track
Andrei PopescuPopescu, Andrei University of SheffieldUnited Kingdom Nominal Recursors as Epi-Recursors The Complex(ity) Landscape of Checking Infinite Descent Committee Member in Selection Committee within the POPL Student Research Competition-track Committee Member in Program Committee within the POPL -track Steering Committee Member in Steering Committee within the CPP-track
François PottierPottier, François InriaFrance Thunks and Debits in Separation Logic with Time Credits
Jonathan ProtzenkoProtzenko, Jonathan Microsoft Research, RedmondUnited States Steering Committee Member in Steering Committee within the PriSC-track Committee Member in Program Committee within the POPL -track
Simon PruckerPrucker, Simon Friedrich-Alexander Universität Erlangen-NürnbergGermany Generic Model Checking for Modal Fixpoint Logics in COOL-MC
Geguang PuPu, Geguang East China Normal UniversityChina Model-Guided Synthesis for LTL over Finite Traces
Loïc PujetPujet, Loïc Stockholm University Martin-Löf à la Coq
Pierre-Marie PédrotPédrot, Pierre-Marie INRIAFrance Martin-Löf à la Coq Committee Member in Program Committee within the POPL -track
Thibaut PéramiPérami, Thibaut University of Cambridge TBC An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic
George PîrleaPîrlea, George National University of Singapore Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
Q Shaz QadeerQadeer, Shaz FacebookUnited States Scaling Verification of Concurrent Programs with the Civl Verifier
Siyuan Brant QianQian, Siyuan Brant University of Illinois at Urbana-Champaign; Zhejiang UniversityUnited States Abstract Interpretation for Automatic Differentiation
Jianxing QinQin, Jianxing Shanghai Jiao Tong University VST-A: A Foundationally Sound Annotation Verifier
Xin QinQin, Xin University of Southern California Committee Member in Artifact Evaluation Committee within the VMCAI -track
Xueying QinQin, Xueying The University of Edinburgh Shoggoth - A Formal Foundation for Strategic Rewriting
Xiaokang QiuQiu, Xiaokang Purdue UniversityUnited States Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations Committee Member in Program Committee within the POPL -track
Weihao QuQu, Weihao Boston University Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Jochen QuanteQuante, Jochen Bosch ResearchGermany Formal Runtime Error Detection During Development in the Automotive Industry
Benjamin QuiringQuiring, Benjamin University of Maryland Generating Well-Typed Terms that are not "Useless"
R Azalea RaadRaad, Azalea Imperial College LondonUnited Kingdom Organizing Committee in Organizing Committee within the The Future of Weak Memory-track Organizer in Organizing Committee within the Incorrectness-track Committee Member in Program Committee within the Incorrectness-track Organizer in Program Committee within the O'Hearn Fest-track
Florian RabeRabe, Florian Amazon Web Services Enhancing Proof Stability
Arjun RadhakrishnaRadhakrishna, Arjun MicrosoftUnited States Committee Member in Program Committee within the VMCAI -track Committee Member in Program Committee within the POPL -track
Jonathan Ragan-KelleyRagan-Kelley, Jonathan Massachusetts Institute of TechnologyUnited States Sparse Differentiation in Computer Graphics
Mukund RaghothamanRaghothaman, Mukund University of Southern CaliforniaUnited States Committee Member in Program Committee within the PADL-track
Ritam RahaRaha, Ritam University of Antwerp, Antwerp, BelgiumBelgium Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic
Kia RahmaniRahmani, Kia The University of Texas at Austin Programming-by-Demonstration for Long-Horizon Robot Tasks
Mike RaineyRainey, Mike Carnegie Mellon UniversityUnited States Automatic Parallelism Management
Sriram RajamaniRajamani, Sriram Microsoft Research Committee Member in Program Committee within the POPL -track
Abhiramon RajasekharanRajasekharan, Abhiramon The University of Texas at Dallas Automated Interactive Domain-Specific Conversational Agents that Understand Human Dialogs
Zvonimir RakamaricRakamaric, Zvonimir Amazon Web ServicesUnited States Dafny Test Generation
Itsaka RakotonirinaRakotonirina, Itsaka MPI-SP Decision and Complexity of Dolev-Yao Hyperproperties
Tahina RamananandroRamananandro, Tahina Microsoft ResearchUnited States Pulse: Proof-oriented Programming in a Concurrent Separation Logic DSL in F* PC Member in Program Committee within the CPP-track
Jan-Paul Ramos-DavilaRamos-Davila, Jan-Paul Cornell UniversityUnited States Gradual Verification for Smart Contracts
Steven RamsayRamsay, Steven University of BristolUnited Kingdom Ill-Typed Programs Don't Evaluate Ill-Typed Programs Don't Evaluate Committee Member in Program Committee within the POPL -track
Robert RandRand, Robert University of ChicagoUnited States Committee Member in Program Committee within the VMCAI -track Committee Member in Program Committee within the PLanQC-track Committee Member in Organizing Committee within the PLanQC-track
Francesca RandoneRandone, Francesca IMT School for Advanced Studies Lucca Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures
Francesco RanzatoRanzato, Francesco University of PadovaItaly Abstract Interpretation-Based Feature Importance for Support Vector Machines Committee Member in Program Committee within the VMCAI -track Committee Member in Organizing Committee within the N40AI-track
Nima RasekhRasekh, Nima Max Planck Institute for Mathematics Univalent Double Categories
Aseem RastogiRastogi, Aseem Microsoft ResearchIndia Diversity, Equity, and Inclusion Co-Chair in Organizing Committee for POPL 2024 Pulse: Proof-oriented Programming in a Concurrent Separation Logic DSL in F* Co-chair in Diversity, Equity, and Inclusion Committee within the POPL Diversity, Equity and Inclusion-track
Frédéric RecoulesRecoules, Frédéric CEA, List Inference of Robust Reachability Constraints
Gianluca RedondiRedondi, Gianluca Fondazione Bruno Kessler Towards the verification of a generic interlocking logic: Dafny meets parameterized model checking
Baber RehmanRehman, Baber The University of Hong KongChina Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Alastair ReidReid, Alastair Intel/Intel LabsUnited Kingdom Committee Member in Program Committee within the PriSC-track
Jan ReinekeReineke, Jan Saarland UniversityGermany Committee Member in Program Committee within the PriSC-track
Luis Angel Rodriguez ReinersReiners, Luis Angel Rodriguez University of CalabriaItaly Marketplace Logistic via Answer Set Programming
Hadrien RenaudRenaud, Hadrien CNRSFrance Arm Architecture and Formal Artifacts: Memory Model and Instruction Semantics
Mathys RennelaRennela, Mathys INRIA ParisFrance Committee Member in Program Committee within the PLanQC-track Program Chair in Organizing Committee within the PLanQC-track
Thomas RepsReps, Thomas University of Wisconsin-MadisonUnited States Committee Member in Program Committee within the POPL -track
Roie ReshefReshef, Roie TechnionIsrael Verification of Neural Networks’ Local Differential Classification Privacy
Eduardo Hermo ReyesReyes, Eduardo Hermo University of Barcelona and Formal Vindications S.L. UTC time, formally verified
McCoy Reynolds BeckerReynolds Becker, McCoy Reverse mode ADEV via YOLO: tangent estimators transpose to gradient estimators
Francesco RiccaRicca, Francesco University of Calabria, ItalyItaly A direct ASP encoding for Declare
Oliver RichardsonRichardson, Oliver Cornell University Mixture Languages
Emily RiehlRiehl, Emily Johns Hopkins University Formalizing the ∞-categorical Yoneda lemma
James RielyRiely, James DePaul UniversityUnited States Committee Member in Program Committee within the POPL -track
Francis RinaldiRinaldi, Francis Illinois Institute of TechnologyUnited States Pipelines and Beyond: Graph Types for ADTs with Futures
Martin C. RinardRinard, Martin C. Massachusetts Institute of TechnologyUnited States MultiSPPL: extending SPPL with multivariate leaf nodes
Talia RingerRinger, Talia University of Illinois at Urbana-ChampaignUnited States Committee Member in Program Committee within the POPL -track
Xavier RivalRival, Xavier Inria; ENS; CNRS; PSL UniversityFrance Committee Member in Program Committee within the VMCAI -track Organizing Committee in Organizing Committee within the N40AI-track
Exequiel RivasRivas, Exequiel Tallinn University of Technology Securing Verified IO Programs Against Unverified Code in F*
Christine RizkallahRizkallah, Christine University of MelbourneAustralia Committee Member in Program Committee within the POPL -track
Juan Conejero RodríguezRodríguez, Juan Conejero University of Barcelona and Formal Vindications S.L. UTC time, formally verified
Tiark RompfRompf, Tiark Purdue UniversityUnited States Rhyme: A Data-Centric Expressive Query Language for Nested Data Structures Flan: An Expressive and Efficient Datalog Compiler for Program Analysis Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs Committee Member in Program Committee within the POPL -track
Neil Julien RossRoss, Neil Julien Dalhousie UniversityCanada Committee Member in Program Committee within the PLanQC-track Committee Member in Organizing Committee within the PLanQC-track Committee Member in Program Committee within the POPL -track
Andreas RossbergRossberg, Andreas IndependentGermany Organizer in Organizing Committee within the WAW-track
Reuben N. S. RoweRowe, Reuben N. S. Royal Holloway University of LondonUnited Kingdom The Complex(ity) Landscape of Checking Infinite Descent
Daniel RoyRoy, Daniel University of Toronto Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets
Rajarshi RoyRoy, Rajarshi Max Planck Institute for Software Systems, Kaiserslautern, GermanyGermany Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic
Fabian RuchRuch, Fabian UnaffiliatedSweden Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Philipp RuemmerRuemmer, Philipp University of Regensburg and Uppsala UniversityGermany String Solving for Verification Committee Member in Program Committee within the VMCAI -track PC Member in Program Committee within the CPP-track
Neea RuschRusch, Neea Augusta UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Alejandro RussoRusso, Alejandro Chalmers University of Technology, SwedenArgentina Speaker in Speakers within the PLMW @ POPL-track Committee Member in Program Committee within the PEPM-track
Sukyoung RyuRyu, Sukyoung KAISTSouth Korea Committee Member in Program Committee within the POPL -track
Gregers Thomas Skat RørdamRørdam, Gregers Thomas Skat IT University of Copenhagen Asynchronous Reactive Programming with Modal Types in Haskell
Philipp RümmerRümmer, Philipp University of Regensburg and Uppsala UniversityGermany Boosting Constrained Horn Solving by Unsat Core Learning
S William S. MosesS. Moses, William Massachusetts Institute of Technology Sparse Differentiation in Computer Graphics
Simmo SaanSaan, Simmo University of Tartu, EstoniaEstonia Correctness Witness Validation by Abstract Interpretation
Amr SabrySabry, Amr Indiana UniversityUnited States With a Few Square Roots, Quantum Computing is as Easy as Pi Committee Member in Program Committee within the PLanQC-track
Irmak SaglamSaglam, Irmak Max Planck Institute for Software Systems (MPI-SWS)Germany Solving Two-Player Games under Progress Assumptions
Ken SakayoriSakayori, Ken The University of TokyoJapan Borrowable Fractional Ownership Types for Verification
Emanuel SallingerSallinger, Emanuel TU Wien & University of Oxford Ontological Reasoning over Shy and Warded Datalog+/- for Streaming-based Architectures
Zeynep G. SaribaturSaribatur, Zeynep G. TU WienAustria Committee Member in Program Committee within the PADL-track
Susmit SarkarSarkar, Susmit University of St. Andrews Committee Member in Program Committee within the POPL -track
Carlo SartianiSartiani, Carlo Università della Basilicata Validation of Modern JSON Schema: Formalization and Complexity
Ryosuke SatoSato, Ryosuke University of TokyoJapan Borrowable Fractional Ownership Types for Verification
Gerhard SchellhornSchellhorn, Gerhard Universitaet AugsburgGermany A Fully Verified Persistency Library
Gabriel SchererScherer, Gabriel INRIA SaclayFrance Unboxed data constructors -- or, how cpp decides a halting problem
Stefanie ScherzingerScherzinger, Stefanie Universität Passau Validation of Modern JSON Schema: Formalization and Complexity
Maximilian SchlundSchlund, Maximilian Bosch ResearchGermany Formal Runtime Error Detection During Development in the Automotive Industry
Anne-Kathrin SchmuckSchmuck, Anne-Kathrin MPI-SWSGermany Solving Two-Player Games under Progress Assumptions Committee Member in Program Committee within the VMCAI -track
Clara SchneidewindSchneidewind, Clara MPI-SP Decision and Complexity of Dolev-Yao Hyperproperties
Sven-Bodo ScholzScholz, Sven-Bodo Radboud UniversityNetherlands Committee Member in Program Committee within the PEPM-track
Tom SchrijversSchrijvers, Tom KU LeuvenBelgium Committee Member in Program Committee within the PADL-track
Lutz SchröderSchröder, Lutz University of Erlangen-NurembergGermany Generic Model Checking for Modal Fixpoint Logics in COOL-MC
Philipp SchröerSchröer, Philipp RWTH Aachen UniversityGermany Caesar: A Verifier for Probabilistic Programs
Michael SchwarzSchwarz, Michael Technische Universität MünchenGermany Correctness Witness Validation by Abstract Interpretation
Frank SchüsseleSchüssele, Frank University of FreiburgGermany Petrification: Software Model Checking for Programs with Dynamic Thread Management
Helmut SeidlSeidl, Helmut Technische Universität MünchenGermany Correctness Witness Validation by Abstract Interpretation
Taro SekiyamaSekiyama, Taro National Institute of InformaticsJapan Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers
Olga SeleznovaSeleznova, Olga TechnionIsrael Verification of Neural Networks’ Local Differential Classification Privacy
Peter SelingerSelinger, Peter Dalhousie UniversityCanada Committee Member in Program Committee within the PLanQC-track
Yanis SellamiSellami, Yanis CEA, List, Univ. Grenoble Alpes Inference of Robust Reachability Constraints
Ilya SergeySergey, Ilya National University of SingaporeSingapore Industrial Relations Co-Chair in Organizing Committee for POPL 2024 Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic Co-chair in Programme Chairs within the PADL-track
Peter SewellSewell, Peter University of CambridgeUnited Kingdom Keynote: Can we reason about the security of concurrent systems code? An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic Organizing Committee in Organizing Committee within the The Future of Weak Memory-track Workshop Chair in Organizing Committee within the POCL-track Committee Member in Program Committee within the POPL -track
Bhakti ShahShah, Bhakti University of Chicago Video Chair in Organizing Committee for POPL 2024 Integrating Dependency Building with Document Checking in Coq
Amir ShaikhhaShaikhha, Amir University of EdinburghUnited Kingdom Structured Tensor Algebra for Efficient Discrete Probabilistic Inference
Chung-chieh ShanShan, Chung-chieh Indiana UniversityUnited States Committee Member in Steering Committee within the LAFI-track
Zhong ShaoShao, Zhong Yale UniversityUnited States Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules Committee Member in Invited Speakers within the GALOP-track Steering Committee Member in Steering Committee within the CPP-track
Ying ShengSheng, Ying Stanford University CLOVER: Closed-Loop Verifiable Code Generation
Dilan ShethSheth, Dilan Imperial College London Randomised Testing of the Dafny Compiler
Jessica ShiShi, Jessica University of Pennsylvania Internalizing Indistinguishability with Dependent Types
Ian ShillitoShillito, Ian Australian National University A mechanised and constructive reverse analysis of soundness and completeness of bi-intuitionistic logic
Shweta ShindeShinde, Shweta ETH ZurichSwitzerland Introduction Steering Committee Member in Steering Committee within the PriSC-track PC Chair in Program Committee within the PriSC-track
Kiraku ShintaniShintani, Kiraku Japan Advanced Institute of Science and Technology Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
Mahsa ShirmohammadiShirmohammadi, Mahsa CNRS & IRIF, Paris On Learning Polynomial Recursive Programs
Sharon ShohamShoham, Sharon Tel Aviv UniversityIsrael An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification
Michael ShulmanShulman, Michael University of San Diego Internal parametricity, without an interval
Nikolaj SidorencoSidorenco, Nikolaj Aarhus University A formal security analysis of Blockchain voting
Filip SieczkowskiSieczkowski, Filip Heriot-Watt UniversityUnited Kingdom Functorial Syntax for All The Essence of Generalized Algebraic Data Types
Jeremy G. SiekSiek, Jeremy G. Indiana University, USAUnited States Committee Member in Program Committee within the POPL -track
Mihaela SighireanuSighireanu, Mihaela IRIF, Université Paris Diderot, FranceFrance Committee Member in Program Committee within the VMCAI -track
Alexandra SilvaSilva, Alexandra Cornell UniversityUnited States Associate Chair in Program Committee within the POPL -track
Ben SimnerSimner, Ben TBC
Abhishek Kr SinghSingh, Abhishek Kr Tel Aviv UniversityIsrael Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Gagandeep SinghSingh, Gagandeep University of Illinois at Urbana-Champaign; VMware ResearchUnited States Abstract Interpretation for Automatic Differentiation Committee Member in Program Committee within the VMCAI -track Committee Member in Program Committee within the POPL -track
Kunal SinghSingh, Kunal Carnegie Mellon University Gradual Verification for Smart Contracts
Satnam SinghSingh, Satnam GroqUnited States Committee Member in Program Committee within the POPL -track
Jeffrey Mark SiskindSiskind, Jeffrey Mark Elmore Family School of Electrical and Computer Engineering, Purdue UniversityUnited States Committee Member in Steering Committee within the LAFI-track
Meghana Aparna SistlaSistla, Meghana Aparna The University of Texas at AustinUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
KC SivaramakrishnanSivaramakrishnan, KC Tarides; IIT MadrasIndia Committee Member in Programme Committee within the PROPL-track Committee Member in Program Committee within the PEPM-track Committee Member in Program Committee within the POPL -track
Tom SmedingSmeding, Tom Utrecht UniversityNetherlands Efficient CHAD
Kate SmithSmith, Kate Committee Member in Program Committee within the PLanQC-track
Viorica Sofronie-StokkermansSofronie-Stokkermans, Viorica University of KoblenzGermany On the Verification of a Subgraph Construction Algorithm
Kristina SojakovaSojakova, Kristina InriaFrance Committee Member in Selection Committee within the POPL Student Research Competition-track Committee Member in Program Committee within the POPL -track
Armando Solar-LezamaSolar-Lezama, Armando Massachusetts Institute of TechnologyUnited States Toward Probabilistic Coarse-to-Fine Program Synthesis
Fu SongSong, Fu State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, and University of Chinese Academy of Sciences Beijing, ChinaChina EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis
Thodoris SotiropoulosSotiropoulos, Thodoris ETH ZurichSwitzerland API-driven Program Synthesis for Testing Static Typing Implementations
Matthieu SozeauSozeau, Matthieu InriaFrance MetaCoq Tutorial Committee Member in Program Committee within the WITS-track
Bas SpittersSpitters, Bas Aarhus UniversityDenmark Specifying Smart Contract with Hax and ConCert CertiCoq-Wasm: Verified compilation from Coq to WebAssembly A formal security analysis of Blockchain voting
Bas SpittersSpitters, Bas Concordium Blockchain Research Center, Aarhus University The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
Bas SpittersSpitters, Bas Aarhus UniversityDenmark PC Member in Program Committee within the CPP-track
Arnaud SpiwackSpiwack, Arnaud TweagFrance Committee Member in Program Committee within the PADL-track
Mohan SridharanSridharan, Mohan University of Birmingham Explanation and Knowledge Acquisition in Ad Hoc Teamwork
Priya SrikumarSrikumar, Priya Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Pranav SrinivasanSrinivasan, Pranav University of Michigan / VMware Research Domesticating Automation
Caleb StanfordStanford, Caleb University of California, DavisUnited States Artifact Evaluation Co-Chair in Organizing Committee for POPL 2024
Ian StarkStark, Ian The University of EdinburghUnited Kingdom Committee Member in Organizing Committee within the POCL-track
Kathrin StarkStark, Kathrin Heriot-Watt UniversityUnited Kingdom Co-chair in Program Committee within the CoqPL-track Committee Member in Program Committee within the POPL -track
Sam StatonStaton, Sam University of OxfordUnited Kingdom A slice sampler for the Indian Buffet Process: expressivity in nonparametric probabilistic programming Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets
Deian StefanStefan, Deian University of California at San DiegoUnited States Steering Committee Chair in Steering Committee within the PriSC-track
Leo StefanescoStefanesco, Leo MPI-SWSGermany Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
Sergei StepanenkoStepanenko, Sergei Aarhus UniversityDenmark The Essence of Generalized Algebraic Data Types
Jonathan SterlingSterling, Jonathan University of CambridgeUnited Kingdom Decalf: A Directed, Effectful Cost-Aware Logical Framework The Essence of Generalized Algebraic Data Types
Michel SteuwerSteuwer, Michel TU Berlin; University of EdinburghGermany Shoggoth - A Formal Foundation for Strategic Rewriting Guided Equality Saturation
Sam StitesStites, Sam Northeastern University A Multi-language Approach to Probabilistic Program Inference
Elias StormeStorme, Elias KU Leuven Secure Calling Conventions for CHERI Capability Machines in Practice (Work in Progress)
Aaron StrahlbergerStrahlberger, Aaron Friedrich-Alexander-Universität Erlangen-NürnbergGermany Generic Model Checking for Modal Fixpoint Logics in COOL-MC
Ofer StrichmanStrichman, Ofer TechnionIsrael Model-Guided Synthesis for LTL over Finite Traces
Zhendong SuSu, Zhendong ETH ZurichSwitzerland API-driven Program Synthesis for Testing Static Typing Implementations
Chuyue SunSun, Chuyue Stanford University CLOVER: Closed-Loop Verifiable Code Generation
Haojia SunSun, Haojia Shanghai Jiao Tong UniversityChina Gradual Verification for Smart Contracts
Pu SunSun, Pu ShanghaiTech University EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis
Xianda SunSun, Xianda University of Cambridge JuliaBUGS: A Graph-Based Probabilistic Programming Language using BUGS syntax
Yaozhu SunSun, Yaozhu University of Hong KongChina Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Nikhil SwamySwamy, Nikhil Microsoft ResearchUnited States Pulse: Proof-oriented Programming in a Concurrent Separation Logic DSL in F*
David SwaseySwasey, David BedRock Systems Towards Modular Specification and Verification of Concurrent Hypervisor-based Isolation
Loïc SylvestreSylvestre, Loïc LIP6 - Sorbonne Université, Paris Hardware implementation of OCaml using a synchronous functional language
Jocelyn SérotSérot, Jocelyn Institut Pascal, Clermont-Ferrand Hardware implementation of OCaml using a synchronous functional language
T Anand Rao TadipatriTadipatri, Anand Rao Indian Institute of Science Education and Research Formalizing Giles Gardam's Disproof of Kaplansky's Unit Conjecture
Yoshiki TakashimaTakashima, Yoshiki Carnegie Mellon UniversityUnited States Automatically Enforcing Rust Trait Properties
Jinhao TanTan, Jinhao University of Hong Kong Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Yong Kiam TanTan, Yong Kiam *Institute for Infocomm Research, ASTAR** PC Member in Program Committee within the CPP-track
Wenhao TangTang, Wenhao University of EdinburghUnited Kingdom Soundly Handling Linearity
J Tanner SlagelTanner Slagel, J A Temporal Differential Dynamic Logic Formal Embedding
Éric TanterTanter, Éric University of Chile Securing Verified IO Programs Against Unverified Code in F*
Runzhou TaoTao, Runzhou Columbia UniversityUnited States A Case for Synthesis of Recursive Quantum Unitary Programs Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions
Philip TascheTasche, Philip University of TwenteNetherlands Deductive Verification of Parameterized Embedded Systems modeled in SystemC
Joseph TassarottiTassarotti, Joseph NYUUnited States Asynchronous Probabilistic Couplings in Higher-Order Separation Logic Program Chair in Program Chairs within the Dafny-track
Enrico TassiTassi, Enrico INRIAFrance Committee Member in Program Committee within the CoqPL-track PC Member in Program Committee within the CPP-track
Zachary TatlockTatlock, Zachary University of WashingtonUnited States Sparse Differentiation in Computer Graphics
Landon TaylorTaylor, Landon Utah State UniversityUnited States Committee Member in Artifact Evaluation Committee within the VMCAI -track
Gabriele TedeschiTedeschi, Gabriele University of Pisa, Italy Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-Deterministic Observers
Anastasios TemperekidisTemperekidis, Anastasios Aristotle University of ThessalonikiGreece TP-DejaVu: Combining Operational and Declarative Runtime Verification
Joshua B. TenenbaumTenenbaum, Joshua B. Massachusetts Institute of TechnologyUnited States Toward Probabilistic Coarse-to-Fine Program Synthesis
Tachio TerauchiTerauchi, Tachio Waseda UniversityJapan Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers
Romain TetleyTetley, Romain VsCoq 2, new foundations
K. S. ThejaswiniThejaswini, K. S. The University of Warwick Solving Two-Player Games under Progress Assumptions
René ThiemannThiemann, René University of Innsbruck Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
Ramanathan S. ThinniyamThinniyam, Ramanathan S. Uppsala University Reachability in Continuous Pushdown VASS
Andrew ThomasThomas, Andrew University of Cambridge JuliaBUGS: A Graph-Based Probabilistic Programming Language using BUGS syntax
Jiaxu TianTian, Jiaxu East China Normal UniversityChina Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training
Sarah TilscherTilscher, Sarah Technische Universität MünchenGermany Correctness Witness Validation by Abstract Interpretation
Amin TimanyTimany, Amin Aarhus UniversityDenmark Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement Modular Denotational Semantics for Effects with Guarded Interaction Trees The Logical Essence of Well-Bracketed Control Flow Committee Member in Program Committee within the POPL -track Conference Chair in Organizing Committee within the CPP-track
Laura TitoloTitolo, Laura NIA/NASA LaRCUnited States A Temporal Differential Dynamic Logic Formal Embedding
Ben L. TitzerTitzer, Ben L. Carnegie Mellon UniversityUnited States Committee Member in Program Committee within the POPL -track
Alwen TiuTiu, Alwen The Australian National University PC Member in Program Committee within the CPP-track
Aaron TombTomb, Aaron Amazon Web ServicesUnited States Dafny Test Generation Portfolio Solving for Dafny
Hazem TorfahTorfah, Hazem Chalmers University of TechnologySweden Committee Member in Program Committee within the VMCAI -track
Emina TorlakTorlak, Emina Amazon Web Services, USAUnited States Improving the Stability of Type Safety Proofs in Dafny Associate Chair in Program Committee within the POPL -track
Dmitriy TraytelTraytel, Dmitriy University of CopenhagenDenmark Steering Committee Member in Steering Committee within the CPP-track Conference Chair in Organizing Committee within the CPP-track
Mirco TribastoneTribastone, Mirco IMT Institute for Advanced Studies Lucca, Italy Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures
Alix TrieuTrieu, Alix ANSSIFrance Committee Member in Program Committee within the PriSC-track
Phil TrinderTrinder, Phil University of Glasgow Guided Equality Saturation
Jean-Baptiste TristanTristan, Jean-Baptiste Amazon Web ServicesUnited States Generation of Verified Assembly Code Using Dafny and Reinforcement Learning Randomised Testing of the Dafny Compiler VMC: a Dafny Library for Verified Monte Carlo Algorithms Steering Committee Chair in Steering Committee within the Dafny-track PC Member in Program Committee within the CPP-track Committee Member in Steering Committee within the LAFI-track
Ninet TristanTristan, Ninet Thales A Verified Compiler for Packet Filtering
Anton TrunovTrunov, Anton TON FoundationUnited Arab Emirates Committee Member in Program Committee within the PADL-track
Stelios TsampasTsampas, Stelios Committee Member in Program Committee within the PriSC-track
Takeshi TsukadaTsukada, Takeshi Chiba UniversityJapan Enriched Presheaf Model of Quantum FPC
Omkar TuppeTuppe, Omkar IIT BombayIndia On-The-Fly Static Analysis via Dynamic Bidirected Dyck Reachability
Nikos TzevelekosTzevelekos, Nikos Queen Mary University of LondonUnited Kingdom Committee Member in Program Committee within the POPL -track Committee Member in Organising Committee within the GALOP-track Co-chair in Program Committee within the GALOP-track
U Hiroshi UnnoUnno, Hiroshi University of TsukubaJapan Automating Relational Verification of Infinite-State Programs Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers Committee Member in Program Committee within the POPL -track
Caterina UrbanUrban, Caterina Inria & École Normale Supérieure \| Université PSLFrance Abstract Interpretation-Based Feature Importance for Support Vector Machines Monotonicity and the Precision of Program Analysis Organizing Committee in Organizing Committee within the N40AI-track
Alex UsherUsher, Alex Imperial College London Randomised Testing of the Dafny Compiler
V Armin VakilVakil, Armin University Of Michigan Testing Specifications In Dafny
John van de Weteringvan de Wetering, John University of AmsterdamNetherlands Committee Member in Program Committee within the PLanQC-track
Rob van Glabbeekvan Glabbeek, Rob The University of Edinburgh Shoggoth - A Formal Foundation for Strategic Rewriting
Antoine Van MuylderVan Muylder, Antoine Inria Paris and Paris 7 Internal and Observational Parametricity for Cubical Agda
Thomas Van StrydonckVan Strydonck, Thomas KULeuven Secure Calling Conventions for CHERI Capability Machines in Practice (Work in Progress)
Julien VanegueVanegue, Julien Bloomberg, USAUnited States Towards Temporal Adversarial Logic
Alexa VanHattumVanHattum, Alexa Wellesley CollegeUnited States Committee Member in Program Committee within the PriSC-track
Gabriele VanoniVanoni, Gabriele IRIF, Université Paris Cité Higher Order Bayesian Networks, Exactly Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Daan VanoverloopVanoverloop, Daan KU Leuven Compiler Support for Control-Flow Linearization Using Architectural Mimicry
Moshe VardiVardi, Moshe Rice UniversityUnited States Model-Guided Synthesis for LTL over Finite Traces
Marco VassenaVassena, Marco Utrecht UniversityNetherlands Web Co-Chair in Organizing Committee for POPL 2024 Committee Member in Program Committee within the PriSC-track
Niki VazouVazou, Niki IMDEA Software Institute Mechanizing Refinement Types Speaker in Speakers within the PLMW @ POPL-track
Margus VeanesVeanes, Margus Microsoft Lean Formalization of Extended Regular Expression Matching with Lookarounds
Sathiyanarayana Venkatesan RameshVenkatesan Ramesh, Sathiyanarayana Max Planck Institute for Software Systems Positive Almost-Sure Termination – Complexity and Proof Rules
Lena VerschtVerscht, Lena Saarland University, Saarland Informatics Campus Hoare-Like Triples and Kleene Algebras with Top and Tests
Lizzie Hernandez VideaVidea, Lizzie Hernandez Microsoft A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability
Thomas VigourouxVigouroux, Thomas VERIMAG - UGAFrance Function synthesis for maximizing model counting
Vighnesh VijayVijay, Vighnesh Roblox Towards an Unsound But Complete Type System: Work In Progress on New Non-Strict Mode for Luau
Jules VillardVillard, Jules MetaUnited Kingdom Committee Member in Program Committee within the Incorrectness-track Committee Member in Program Committee within the POPL -track Organizer in Program Committee within the O'Hearn Fest-track
Yakir VizelVizel, Yakir Technion—Israel Institute of TechnologyIsrael Automatic and Incremental Repair for Speculative Information Leaks
Vesal VojdaniVojdani, Vesal University of TartuEstonia Correctness Witness Validation by Abstract Interpretation
Matthijs VákárVákár, Matthijs Utrecht University Homomorphic Reverse Differentiation of Iteration Efficient CHAD Co-chair in Program Committee within the LAFI-track Committee Member in Organizing Committee within the LAFI-track
W Andrew WagnerWagner, Andrew Northeastern University All the Binaries Together: A Semantic Approach to Application Binary Interfaces
Cassidy WaldripWaldrip, Cassidy Brigham Young UniversityUnited States Verifying Dafny Contract Integrity
Johannes WallnerWallner, Johannes Graz University of TechnologyAustria Committee Member in Program Committee within the PADL-track
Charlie WalpoleWalpole, Charlie University of Bristol Ill-Typed Programs Don't Evaluate Ill-Typed Programs Don't Evaluate
Michael WalterWalter, Michael Ruhr-Universität Bochum Committee Member in Program Committee within the PLanQC-track
Huaduo WangWang, Huaduo THE UNIVERSITY OF TEXAS AT DALLAS FOLD-SE: An Efficient Rule-based Machine Learning Algorithm with Scalable Explainability Using Logic Programming and Kernel-Grouping for Improving Interpretability of Convolutional Neural Networks
Meng WangWang, Meng University of BristolUnited Kingdom Co-chair in Organizing Committee within the PEPM-track
Peixin WangWang, Peixin University of Oxford Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Qinshi WangWang, Qinshi Princeton University VST-A: A Foundationally Sound Annotation Verifier
Shengyi WangWang, Shengyi Princeton University, USA Compositional Verification of Concurrent C Programs with Search Structure Templates
Xinyu WangWang, Xinyu University of MichiganUnited States Efficient Bottom-Up Synthesis for Programs with Local Variables
Yayu WangWang, Yayu The University of British Columbia Microarchitectural Side-Channel Mitigations for Serverless Applications
Yuepeng WangWang, Yuepeng Simon Fraser UniversityCanada Semantic Code Refactoring for Abstract Data Types
Yuting WangWang, Yuting Shanghai Jiao Tong UniversityChina Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules
Zhonghan WangWang, Zhonghan Institute of Software/CAS ChinaChina Efficient Local Search for Nonlinear Real Arithmetic
Robert N. M. WatsonWatson, Robert N. M. University of Cambridge Committee Member in Organizing Committee within the POCL-track
Conrad WattWatt, Conrad University of CambridgeUnited Kingdom Virtualization Chair in Organizing Committee for POPL 2024 Organizer in Organizing Committee within the WAW-track
Heike WehrheimWehrheim, Heike University of Oldenburg A Reachability Logic for a Weak Memory Model with Promises A Fully Verified Persistency Library
Guannan WeiWei, Guannan Purdue UniversityUnited States Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Niels van der WeideWeide, Niels van der Radboud University Nijmegen, Netherlands Univalent Double Categories Displayed Monoidal Categories for the Semantics of Linear Logic
Jonathan WeinbergerWeinberger, Jonathan Johns Hopkins University Formalizing the ∞-categorical Yoneda lemma
Stephanie WeirichWeirich, Stephanie University of PennsylvaniaUnited States Internalizing Indistinguishability with Dependent Types
Georg Weissenbacher