POPL 2024 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (1145)

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
Vytautas AbramaviciusAbramavicius, Vytautas PASQAL SAS Qadence: a differentiable interface for digital-analog programs
Umut A. AcarAcar, Umut A. Carnegie Mellon UniversityUnited States Disentanglement with Futures, State, and Interaction Automatic Parallelism Management
Beniamino AccattoliAccattoli, Beniamino Inria & Ecole PolytechniqueFrance Normal Form Bisimulations by Value
Nate AckermanAckerman, Nate Harvard University Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets
Andy Adams-MoranAdams-Moran, Andy MetaUnited Kingdom Session Chair of Session 4 (part of O'Hearn Fest)
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
Sharan AgrawalAgrawal, Sharan University of Cambridge, UK Scalable agent-based models for optimized policy design: applications to the economics of biodiversity and carbon
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 RichWasm: Bringing Safe, Fine-Grained, Shared Memory Interoperability to WebAssembly All the Binaries Together: A Semantic Approach to Application Binary Interfaces Towards a Categorical Model of the Lilac Separation Logic Steering Committee Member in Steering Committee within the PriSC-track
Benedikt AhrensAhrens, Benedikt Delft University of TechnologyNetherlands Displayed Monoidal Categories for the Semantics of Linear Logic Univalent Double Categories 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 Arm and University College LondonUnited Kingdom Elegance and generosity are scientific values - And other things I've learned from Peter Arm Architecture and Formal Artifacts: Memory Model and Instruction Semantics
Guillaume AllaisAllais, Guillaume University of StrathclydeUnited Kingdom Scoped and Typed Staging by Evaluation
Ricardo AlmeidaAlmeida, Ricardo University of Edinburgh Morello Cerise: proving secure encapsulation (work in progress)
Anoud AlshnakatAlshnakat, Anoud KTH Royal Institute of Technology HOL4P4: A Heapless Small-Step Semantics and Type System for P4
Thorsten AltenkirchAltenkirch, Thorsten University of Nottingham Internal parametricity, without an interval
Mario AlvianoAlviano, Mario University of CalabriaItaly Session Chair of Answer Set Programming II (part of PADL) Marketplace Logistic via Answer Set Programming Rethinking Answer Set Programming Templates
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 Polynomial-time Classical Simulation of Roetteler’s Shifted Bent Function Algorithm Committee Member in Program Committee within the PLanQC-track Committee Member in Organizing Committee within the PLanQC-track
Abhishek AnandAnand, Abhishek BedRock SystemsUnited 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
Damián ArquezArquez, Damián University of Chile Differential Privacy in an Impure World
Ellen ArvidssonArvidsson, Ellen Uppsala UniversitySweden Concurrent Mutation must go
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 Session Chair of Formalizations of Category Theory (part of CPP) 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 Towards a Language-parametric DSL for Refactoring (Short Paper) Committee Member in Program Committee within the POPL -track
Jakub BachurskiBachurski, Jakub University of CambridgePoland Embedding Pointful Array Programming in Python
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
Alexander BandukwalaBandukwala, Alexander Unaffiliated Toward a Live, Rich, Composable, and Collaborative Planetary Compute Engine
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
Aurèle BarrièreBarrière, Aurèle EPFLSwitzerland Session Chair of Wednesday Lunch Session Previews (part of POPL Session Previews)
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 Welcome Rust on Morello 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
Thomas BauereissBauereiss, Thomas University of Cambridge The Morello ISA semantics, proof, and test generation
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
Benjamin BennetzenBennetzen, Benjamin Department of Computer Science, Aalborg University A type-safe generalized editor calculus (Extended Abstract)
Nick BentonBenton, Nick MetaUnited Kingdom Session Chair of Session 3 (part of O'Hearn Fest) Pete's Footprints Types 3: Session Preview Committee Member in Program Committee within the POPL -track
Josh BerdineBerdine, Josh SkipLabsUnited Kingdom Symbolic Execution with Separating Decision Diagrams
George BerdovskiyBerdovskiy, George University of California, Davis Zero-Cost Capabilities: Retrofitting Effect Safety in Rust
Daniil BerezunBerezun, Daniil JetBrains Research; Constructor University BremenNetherlands A Case Study in Functional Conversion and Mode Inference in miniKanren
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
Yves BertotBertot, Yves INRIAFrance Session with the Coq Development Team
Nathalie BertrandBertrand, Nathalie INRIA Rennes Committee Member in Program Committee within the VMCAI -track
Frédéric BessonBesson, Frédéric INRIA PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams
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 Proving capability safety in the presence of indirect sentries An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic The Essence of Generalized Algebraic Data Types Asynchronous Probabilistic Couplings in Higher-Order Separation Logic 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
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
Dines BjørnerBjørner, Dines DTUDenmark The 0'th PEPM Event: October 1987—and Andrei Petrovich Ershov: 1977–1988 (Invited Contribution)
Sandrine BlazyBlazy, Sandrine University of RennesFrance Session Chair of Business Meeting (part of CPP) Session Chair of Logic and Beyond (part of CPP) Mechanized Proofs: Session Preview PC Chair in Program Committee within the CPP-track Committee Member in Steering 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 Toward a Live, Rich, Composable, and Collaborative Planetary Compute Engine Total Type Error Localization and Recovery with Holes
Pauline BlohmBlohm, Pauline Uni MünsterGermany Deductive Verification of Parameterized Embedded Systems modeled in SystemC
Lison Blondeau-PatissierBlondeau-Patissier, Lison LIS & I2M, Aix-Marseille UniversitéFrance Taylor Expansion is Game Semantics
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
Hans-J. BoehmBoehm, Hans-J. Google What we learned from C++ atomics and memory model standardization
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
Joe BondBond, Joe University of Bristol, UK Fluid: towards transparent, self-explanatory research outputs
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
Peio BorthelleBorthelle, Peio Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, LAMA, 73000 ChambéryFrance An abstract, certified account of Operational Game Semantics
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 Session Chair of Friday Morning Session Previews (part of POPL Session Previews) When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism Capturing Types (TOPLAS)
Gert-Jan BothBoth, Gert-Jan PASQAL SAS Qadence: a differentiable interface for digital-analog programs
Nicola BottaBotta, Nicola Potsdam Institute for Climate Impact Research (PIK) Can computer science help climate policy making?
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
Maddy BowersBowers, Maddy Massachusetts Institute of TechnologyUnited States Toward Probabilistic Coarse-to-Fine Program Synthesis
William J. BowmanBowman, William J. University of British ColumbiaCanada Session Chair of Session 2 (part of WITS) 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 Capturing Types (TOPLAS) Committee Member in Program Committee within the POPL -track
Edwin BradyBrady, Edwin University of St Andrews, UKUnited Kingdom Session Chair of Session 4 (part of WITS) Yaffle: A New Core for Idris 2 Committee Member in Program Committee within the PEPM-track Committee Member in Program Committee within the WITS-track
Franz BrausseBrausse, Franz The University of Manchester ESBMC-CHERI: Towards Verification of C/C++ Programs for CHERI Platforms with ESBMC
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
Stephen BrookesBrookes, Stephen CMU CSL and relaxed memory
James BrotherstonBrotherston, James Strong vs. weak separating conjunction in CSL
Fraser BrownBrown, Fraser CMU Committee Member in Program Committee within the POPL -track
Alessandro BruniBruni, Alessandro IT University of Copenhagen Declarative Languages for Safe AI
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
Benedict BuntingBunting, Benedict University of OxfordUnited Kingdom Operational Algorithmic Game Semantics
Matteo BusiBusi, Matteo University Ca' Foscari, VeniceItaly Session Chair of Session 3 (part of PriSC) 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 UniversityUnited 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 Session Chair of Session 4 (part of POCL ) The Morello ISA semantics, proof, and test generation 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
Chris CasinghinoCasinghino, Chris Jane Street Jane Street Board Game Night
Giuseppe CastagnaCastagna, Giuseppe CNRS; Université Paris CitéFrance Polymorphic Type Inference for Dynamic Languages
Elias CastegrenCastegren, Elias KTH Royal Institute of Technology Concurrent Mutation must go
Ethan CecchettiCecchetti, Ethan University of Wisconsin-MadisonUnited States Computational-Bounded Robust Compilation and Universally Composable Security
Lorenzo CeragioliCeragioli, Lorenzo IMT Lucca, Italy Effect Semantics for Quantum Protocols 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 Verifying a concurrent file system with sequential reasoning Co-chair in Program Committee within the CoqPL-track
Soham ChakrabortyChakraborty, Soham TU DelftNetherlands Session Chair of Synthesis 1 (part of POPL ) Heterogeneous concurrency -- a new frontier for weak memory 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
Kostia ChardonnetChardonnet, Kostia Università di BolognaItaly MELL proof-nets without boxes: thirty years later
Arthur CharguéraudCharguéraud, Arthur InriaFrance Session Chair of Verified Compilation (part of CPP) 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 (The Hong Kong University of Science and Technology) 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 PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams
Luke CheesemanCheeseman, Luke Imperial College LondonUnited Kingdom Concurrent Mutation must go
Huamin ChenChen, Huamin RED HAT Kepler Watt Store: Kepler Software Watt Watcher Store
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 SCI SemiconductorUnited Kingdom Capabilities for safe cross-language interoperability 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
Ezequiel CimadevillaCimadevilla, Ezequiel Instituto de Fisica de Cantabria The programming challenges of climate data analysis
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 Session Chair of Session 1 (part of GALOP) Taylor Expansion is Game Semantics Committee Member in Organising Committee within the GALOP-track Co-chair in Program Committee within the GALOP-track
Jessica ClarkeClarke, Jessica University of CambridgeUnited Kingdom Morello software and compilers
Sylvan ClebschClebsch, Sylvan Microsoft Azure ResearchUnited Kingdom Concurrent Mutation must go
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
Andrea ColledanColledan, Andrea University of Bologna & INRIA Sophia Antipolis Circuit Width Estimation via Effect Typing and Linear Dependency (Extended Abstract)
Luisa CollodiCollodi, Luisa University of FlorenceItaly Guaranteed inference for probabilistic programs: a parallelisable, small-step operational approach
Youyou CongCong, Youyou Tokyo Institute of TechnologyJapan Session Chair of Program Inversion & DSLs (part of PEPM) An Intrinsically Typed Compiler for Algebraic Effect Handlers One-Pass CPS Translation of Dependent Types (Talk Proposal) 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
Byron CookCook, Byron AmazonUnited States Massive proofs for the masses
Simon CookseyCooksey, Simon NVIDIAUnited Kingdom Programmers love mind-bogglingly complicated weak memory models Rust on Morello
Lucas C. CordeiroCordeiro, Lucas C. University of Manchester, UKUnited Kingdom ESBMC-CHERI: Towards Verification of C/C++ Programs for CHERI Platforms with ESBMC
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 Is Peter Correct or Incorrect?
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: Or, Lambda: The Ultimate Document
Caroline CronjägerCronjäger, Caroline Vrije Universiteit AmsterdamNetherlands 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 Mario DagradaDagrada, Mario PASQAL SAS Qadence: a differentiable interface for digital-analog programs
Ugo Dal LagoDal Lago, Ugo University of Bologna & INRIA Sophia AntipolisItaly Circuit Width Estimation via Effect Typing and Linear Dependency (Extended Abstract) On Interaction, Efficiency, and Reversibility 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
Michael DalesDales, Michael University of Cambridge, UK Session Chair of Software engineering and ecosystems (part of PROPL) Discussion on multidisciplinary PROPL-work
Mila Dalla PredaDalla Preda, Mila University of VeronaItaly Monotonicity and the Precision of Program Analysis
Mads DamDam, Mads KTH HOL4P4: A Heapless Small-Step Semantics and Type System for P4
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
Kinnari DaveDave, Kinnari Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire Méthodes Formelles Quantum and Classical Control (work-in-progress)
Cristina DavidDavid, Cristina University of BristolUnited Kingdom Fluid: towards transparent, self-explanatory research outputs
Emanuele De AngelisDe Angelis, Emanuele IASI-CNRItaly A Historical Perspective on Program Transformation and Recent Developments (Invited Contribution) 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
Ulrik de Muelenaerede Muelenaere, Ulrik University of Notre Dame QGAT: A Generate-and-Test Paradigm for Quantum Circuits
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
Folkert de Vriesde Vries, Folkert University of Groningen Type-directed defunctionalization in the presence of typeclasses and monomorphization
Abhishek DeDe, Abhishek University of BirminghamUnited Kingdom MELL proof-nets without boxes: thirty years later
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
Xavier DenisDenis, Xavier Université Paris-Saclay, CNRS, ENS Paris-Saclay, INRIA, Laboratoire Méthodes FormellesFrance Student Volunteer Co-Chair in Organizing Committee for POPL 2024
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 Session Chair of Session 4 (part of PriSC) Secure Calling Conventions for CHERI Capability Machines in Practice (Work in Progress) Proving capability safety in the presence of indirect sentries 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 Session Chair of Session 1: Openning, Keynote, SAT, SMT and Automated Reasoning (part of VMCAI ) 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
Dino DistefanoDistefano, Dino Meta With Peter from Theory to Engineering
Hasra DodampegamaDodampegama, Hasra University of Birmingham Explanation and Knowledge Acquisition in Ad Hoc Teamwork
Mike DoddsDodds, Mike Galois, Inc. How Do We Know That Weak Memory Matters? Weak Memory and Concurrent Separation Logic: Session Preview
Stephen DolanDolan, Stephen Jane Street Why Languages Should Preserve Load-Store Order 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 Extraordinary Meeting: The Publicity Chairs Reflect on the Peer-Review Process 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 Session Chair of Session 3 (part of The Future of Weak Memory) Session Chair of Session 4 (part of The Future of Weak Memory) A Reachability Logic for a Weak Memory Model with Promises Welcome 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
Alexandre DreweryDrewery, Alexandre INRIA From Java to Kotlin with Contextual Equality Saturation
Derek DreyerDreyer, Derek MPI-SWSGermany Program Chair in Organizing Committee for POPL 2024 Session Chair of Keynote 1 (part of POPL ) Opening Panel Later Credits: A Case Study in the Unreasonable Effectiveness of Separation Logic Panelist in Panelists within the PLMW @ POPL-track Program Chair in Program Committee within the POPL -track
Sophia DrossopoulouDrossopoulou, Sophia Imperial College LondonUnited Kingdom Session Chair of Concurrency (part of POPL ) Concurrent Mutation must go Object Capabilities Committee Member in Program Committee within the POPL -track
Justin DuDu, Justin University of California, San DiegoUnited States GPU-Accelerated Synthesis of Boolean Circuits
Ke DuDu, Ke An Iris Instance for Verifying CompCert C Programs
Irina DudinaDudina, Irina University of Edinburgh CHERI static analysis
Anand DukkipatiDukkipati, Anand University of Michigan Total Type Error Localization and Recovery with Holes
Ross DuncanDuncan, Ross Quantinuum Session Chair of Compilation (part of PLanQC) GUPPY: Pythonic Quantum-Classical Programming Introducing BRAT Committee Member in Program Committee within the PLanQC-track Committee Member in Organizing Committee within the PLanQC-track
Jana DunfieldDunfield, Jana Queen's University, Kingston, OntarioCanada Focusing on Refinement Typing (TOPLAS)
Bruno DutertreDutertre, Bruno Amazon Web Services Committee Member in Program Committee within the VMCAI -track
Alessio DuèDuè, Alessio University of Pisa Effect handlers in Zig (extended abstract)
Yotam DvirDvir, Yotam Tel Aviv University A Denotational Approach to Release/Acquire Concurrency A Denotational Approach to Release/Acquire Concurrency Committee Member in Artifact Evaluation Committee within the VMCAI -track
Alejandro Díaz-CaroDíaz-Caro, Alejandro ICC (UBA-CONICET) & UNQArgentina A feasible and unitary programming language with quantum control
Emanuele D’OsualdoD’Osualdo, Emanuele MPI-SWSGermany Session Chair of Logical Foundations (part of POPL ) Logical Foundations: Session Preview Committee Member in Program Committee within the POPL -track
E Gabriel EbnerEbner, Gabriel Microsoft Research Lean Formalization of Extended Regular Expression Matching with Lookarounds
Dimitrios EconomouEconomou, Dimitrios Queen's University, CanadaCanada Focusing on Refinement Typing (TOPLAS)
Chelsea EdmondsEdmonds, Chelsea University of SheffieldUnited Kingdom Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma
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 Object Capabilities
Richard A. EisenbergEisenberg, Richard A. Jane StreetUnited States Session Chair of Session 1 (part of WITS) Jane Street Board Game Night Types 2: Session Preview 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
Vincent ElfvingElfving, Vincent PASQAL SAS Qadence: a differentiable interface for digital-analog programs
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
Igor EngelEngel, Igor JetBrains Research; Constructor University BremenGermany A Case Study in Functional Conversion and Mode Inference in miniKanren
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 ReginaCanada Strictly Monotone Brouwer Trees for Well Founded Recursion Over Multiple Arguments
Julian ErhardErhard, Julian Technical University of MunichGermany Correctness Witness Validation by Abstract Interpretation
Guilherme EspadaEspada, Guilherme LASIGE, University of LisbonPortugal Committee Member in AV Committee for POPL 2024
Ran EttingerEttinger, Ran NVIDIA and Ben-Gurion University of the Negev and 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 Normal Form Bisimulations by Value Declarative Languages for Safe AI Higher Order Bayesian Networks, Exactly
James FairbanksFairbanks, James University of Florida Categorical Composition of Discrete Exterior Calculus Climate Models
Chris FallinFallin, Chris FastlyUnited States Steering Committee Member in Steering Committee within the PriSC-track
Andong FanFan, Andong HKUST (The Hong Kong University of Science and Technology)China 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 A New Perspective on Commutativity in Verification Commutativity Simplifies Proofs of Parameterized Programs Coarser Equivalences for Causal Concurrency
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
Richard FeldmanFeldman, Richard Type-directed defunctionalization in the presence of typeclasses and monomorphization
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 Session Chair of Invited Talks 3 (part of N40AI ) 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
Patrick FerrisFerris, Patrick University of Cambridge, UKUnited Kingdom Discussion on multidisciplinary PROPL-work
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
Fabio FioravantiFioravanti, Fabio University of Chieti-PescaraItaly A Historical Perspective on Program Transformation and Recent Developments (Invited Contribution)
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
Alcides FonsecaFonseca, Alcides University of LisbonPortugal Implementing separation logic using an SMT-backed Frame Rule
Yannick ForsterForster, Yannick InriaFrance MetaCoq Tutorial
Jeffrey S. FosterFoster, Jeffrey S. Tufts UniversityUnited States Dafny Test Generation
Nate FosterFoster, Nate Cornell University and Jane StreetUnited States Session Previews Co-Chair in Organizing Committee for POPL 2024 The Network is the Computer: A Programming Language Perspective
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
Megan FrisellaFrisella, Megan Brown University Pulse: Proof-oriented Programming in a Concurrent Separation Logic DSL in F*
Samantha FrohlichFrohlich, Samantha University of BristolUnited Kingdom Session Chair of Wednesday Afternoon Session Previews (part of POPL Session Previews) Consider Collaboration Speaker in Speakers within the PLMW @ POPL-track
Aymeric FromherzFromherz, Aymeric InriaFrance Committee Member in Program Committee within the POPL -track
Daniel FruminFrumin, Daniel 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
Ren FukaishiFukaishi, Ren The University of TokyoJapan Productivity Verification for Functional Programs by Reduction to Termination Verification
G Philipp GablerGabler, Philipp Independent researcher JuliaBUGS: A Graph-Based Probabilistic Programming Language using BUGS syntax
Fabio GadducciGadducci, Fabio University of Pisa Effect Semantics for Quantum Protocols 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 Session with the Coq Development Team 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 Session Chair of Policy and decision making / Brainstorming (part of PROPL) Assessing the availability, reproducibility and reuseability of research software 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
Dapeng GaoGao, Dapeng University of Cambridge Compartmentalisation models
Ronald GarciaGarcia, Ronald University of British ColumbiaCanada Session Chair of Gradual Typing and Verification (part of POPL ) Gradual Typing and Verification: Session Preview Committee Member in Program Committee within the POPL -track
Philippa GardnerGardner, Philippa Imperial College LondonUnited Kingdom General Chair in Organizing Committee for POPL 2024 Session Chair of SIGPLAN Awards, PC Chair's Report, and Business Meeting (part of POPL ) Mechanising WebAssembly Well? Unified Compositional Symbolic Execution Unified Compositional Formal Methods: Exact Separation Logic and the Gillian Platform for Correctness and Incorrectness Reasoning Verified Software at Scale
Francesco GavazzoGavazzo, Francesco University of Pisa, ItalyItaly Committee Member in Program Committee within the POPL -track
Hong GeGe, Hong University of Cambridge Bayesian inference using probabilistic programming JuliaBUGS: A Graph-Based Probabilistic Programming Language using BUGS syntax Hong Ge: Bayesian inference using probabilistic programming
Martin GebserGebser, Martin University of Klagenfurt, AustriaAustria Session Chair of Declarative Programming for AI (part of PADL) Session Chair of Types and Effects (part of PADL) Co-chair in Programme Chairs within the PADL-track
Luke GeesonGeeson, Luke University College London (UCL)United Kingdom Weak Memory Demands Model-based Compiler Testing
Adam GellerGeller, Adam Computer Science, University of British ColumbiaCanada Indexed Types for a Statically Safe WebAssembly
Aina Linn GeorgesGeorges, Aina Linn Max Planck Institute for Software Systems (MPI-SWS) Proving capability safety in the presence of indirect sentries
Jad Elkhaleq GhalayiniGhalayini, Jad Elkhaleq University of CambridgeUnited Kingdom SSA is Freyd Categories
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 Session Chair of Short Talks (part of N40AI ) Short talks: Past, Present and Future of AI
Roberto GiacobazziGiacobazzi, Roberto University of Arizona, Tucson, Arizona, USAUnited States Program Analysis: Session Preview
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
Ryan GibbGibb, Ryan Session Chair of Modelling and analysis / Energy and efficiency (part of PROPL)
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
Robert GlückGlück, Robert University of CopenhagenDenmark Partial Evaluation of Reversible Flowchart Programs
Patrice GodefroidGodefroid, Patrice Lacework Peter, the May and the Must, and Lacework
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 Consider Collaboration 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
Kirill GolubevGolubev, Kirill University of LisbonPortugal Implementing separation logic using an SMT-backed Frame Rule
Hannah GommerstadtGommerstadt, Hannah Vassar College Session Chair of Fourth Session (part of PLMW @ POPL) 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 What Compilers desire from Weak Memory Semantics
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
Eric GoubaultGoubault, Eric Ecole Polytechnique Short talks: Past, Present and Future of AI
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 Asynchronous Probabilistic Couplings in Higher-Order Separation Logic Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
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
Roberto GuancialeGuanciale, Roberto KTH Royal Institute of TechnologySweden HOL4P4: A Heapless Small-Step Semantics and Type System for P4
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
Roland GuichardGuichard, Roland PASQAL SAS Qadence: a differentiable interface for digital-analog programs
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 Session Chair of Answer Set Programming I (part of PADL) FOLD-SE: An Efficient Rule-based Machine Learning Algorithm with Scalable Explainability Declarative Languages for Safe AI 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 CampusGermany Belief Programming in Partially Observable Probabilistic Environments
H Liana HadareanHadarean, Liana Amazon Web ServicesUnited States Committee Member in Program Committee within the VMCAI -track
Ayaz HafizHafiz, Ayaz RWX Type-directed defunctionalization in the presence of typeclasses and monomorphization
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
Emmanuel HainryHainry, Emmanuel LORIA, Université de Lorraine A feasible and unitary programming language with quantum control
Angus HammondHammond, Angus University of Cambridge Morello Cerise: proving secure encapsulation (work in progress) 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
Mark HarmanHarman, Mark Meta Platforms, Inc. and UCLUnited Kingdom Working with Peter O'Hearn in academia and industry
Robert HarperHarper, Robert Carnegie Mellon UniversityUnited States Decalf: A Directed, Effectful Cost-Aware Logical Framework
Sarah HarrisHarris, Sarah University of Kent Rust on Morello
Philipp G. HaselwarterHaselwarter, Philipp G. Aarhus University The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography Asynchronous Probabilistic Couplings in Higher-Order Separation Logic
Vahid HashemiHashemi, Vahid AUDI AGGermany AGNES: Abstraction-guided Framework for Deep Neural Networks Security
Daniel HausmannHausmann, Daniel University of GothenburgSweden Fair omega-Regular Games 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
Niklas HeimHeim, Niklas PASQAL SAS Qadence: a differentiable interface for digital-analog programs
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 Session Chair of Automata And Complexity (part of POPL ) Session Chair of History of PEPM (part of PEPM) In memoriam Neil Deaton Jones 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 Session Chair of Synthesis 2 (part of POPL ) 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 Stack Switching in WebAssembly with Effect Handlers 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
Kengo HirataHirata, Kengo University of Edinburgh Quantum Controlled Measurements via Program Transformation
Nao HirokawaHirokawa, Nao Japan Advanced Institute of Science and Technology Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
Andrew K. HirschHirsch, Andrew K. University at Buffalo, SUNYUnited States Session Chair of Third Session (part of PLMW @ POPL) Higher-Order Effectful Programs: Session Preview Committee Member in Organizing Committee within the PLMW @ POPL-track Committee Member in Program Committee within the POPL -track
Tom HirschowitzHirschowitz, Tom Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000 ChambéryFrance An abstract, certified account of Operational Game Semantics
Singh HitarthHitarth, Singh Committee Member in Artifact Evaluation Committee within the VMCAI -track
Son HoHo, Son INRIAFrance Session Chair of Thursday Afternoon Session Previews (part of POPL Session Previews) 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 Session Chair of Machine and Automata Learning (part of POPL ) Session Chair of Third Session (part of LAFI) Session Chair of Poster and Interactive Session (part of LAFI) Session Chair of Second Session (part of LAFI) Session Chair of First Session (part of LAFI) A Multi-language Approach to Probabilistic Program Inference Towards a Categorical Model of the Lilac Separation Logic Machine and Automata Learning: Session Preview 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 Session Chair of Type Theory (part of POPL ) Session Chair of Formalizing Mathematics (part of CPP) asai: a Library for Compiler Diagnostics Type Theory: Session Preview Committee Member in Program Committee within the POPL -track PC Member in Program Committee within the CPP-track
Tyler HouHou, Tyler University of California, BerkeleyUnited States Efficient Incremental Computation for Halide
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 Session Chair of Effect Handlers (part of POPL ) 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
Hongyi HuangHuang, Hongyi National University of Singapore Formal Methods to Save the Earth
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
John HuiHui, John Columbia University, New YorkUnited States Committee Member in AV Committee for POPL 2024
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 Reverse mode ADEV via YOLO: tangent estimators transpose to gradient estimators MultiSPPL: extending SPPL with multivariate leaf nodes
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) 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 Committee Member in AV Committee for POPL 2024 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 Session Chair of Session 4 (part of GALOP) Operational game semantics for generative algebraic effects and handlers An abstract, certified account of Operational Game Semantics Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the GALOP-track
Jules JacobsJacobs, Jules Radboud University Nijmegen Session Chair of Probabilistic Programs (part of POPL ) Panel Probabilistic Programs: Session Preview Verified Message-Passing Concurrency in Iris: Separation Logic Meets Session Types Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing Panelist in Panelists within the PLMW @ POPL-track
Swen JacobsJacobs, Swen CISPAGermany Automatic and Incremental Repair for Speculative Information Leaks Parameterized Verification of Disjunctive Timed Networks
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 Technology and University of GothenbrugSweden Can computer science help climate policy making? 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
Hamza JaâfarJaâfar, Hamza Inria Operational game semantics for generative algebraic effects and handlers
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 ZurichSwitzerland Separation Logic: Session Preview 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 Declarative Languages for Safe AI 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
Cezary KaliszykKaliszyk, Cezary University of Innsbruck Improved Assistance for Interactive Proof
Shoaib KamilKamil, Shoaib Adobe Research Sparse Differentiation in Computer Graphics
Benjamin Lucien KaminskiKaminski, Benjamin Lucien Saarland University; University College LondonGermany Quantitative Weakest Hyper Pre Hoare-Like Triples and Kleene Algebras with Top and Tests Caesar: A Verifier for Probabilistic Programs Belief Programming in Partially Observable Probabilistic Environments Automata and Complexity: Session Preview Committee Member in Program Committee within the LAFI-track
Ohad KammarKammar, Ohad University of EdinburghUnited Kingdom LGBTQ+ Host in Organizing Committee for POPL 2024 A Denotational Approach to Release/Acquire Concurrency Foundations of Type-Driven Probabilistic Modelling Shoggoth - A Formal Foundation for Strategic Rewriting 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
Alperen KelesKeles, Alperen University of Maryland at College ParkUnited States Tail: A Typed and Structured Document Editor
Gabriele KellerKeller, Gabriele Utrecht UniversityNetherlands Session Chair of Types & Staging (part of PEPM) Opening Committee Member in Organizing Committee within the PEPM-track
Ariel E. KellisonKellison, Ariel E. Cornell UniversityUnited States Session Chair of Wednesday Morning Session Previews (part of POPL Session Previews) 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)
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
Oleg KiselyovKiselyov, Oleg Tohoku UniversityJapan Complete Stream Fusion for Software-Defined Radio
Aleks KissingerKissinger, Aleks University of Oxford Session Chair of New Directions for Quantum Programming (part of PLanQC) Graphical Primitive Recursion For String Diagrams Optimal compilation of parametrised quantum circuits
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 Chasing Unicorns and Not Losing Hope in Validating Weak Memory Persistency Models
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 Ownership Types for Verification of Programs with Pointer Arithmetic Productivity Verification for Functional Programs by Reduction to Termination Verification Borrowable Fractional Ownership Types for Verification
Tomoaki KobayashiKobayashi, Tomoaki Tohoku UniversityJapan Complete Stream Fusion for Software-Defined Radio
Mark KochKoch, Mark Quantinuum GUPPY: Pythonic Quantum-Classical Programming Introducing BRAT
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 Declarative Languages for Safe AI PC Member in Program Committee within the CPP-track
Ekaterina KomendantskayaKomendantskaya, Ekaterina Heriot-Watt University and Southampton UniversityUnited Kingdom Session Chair of Panel Discussion (part of PADL) Whats and Whys of Neural Network Verification (A Declarative Programming Perspective)
Lydia KondyludouKondyludou, Lydia Session Chair of Thursday Breakfast Session Previews (part of POPL Session Previews)
Joomy KorkutKorkut, Joomy Bloomberg LPUnited States Committee Member in Artifact Evaluation Committee within the VMCAI -track
Paulette KoronkevichKoronkevich, Paulette University of British Columbia Session Chair of Friday Afternoon Session Previews (part of POPL Session Previews)
Konstantin KorovinKorovin, Konstantin University of Manchester ESBMC-CHERI: Towards Verification of C/C++ Programs for CHERI Platforms with ESBMC
Vasileios KoutavasKoutavas, Vasileios Trinity College DublinIreland Fully Abstract Normal Form Bisimulation for Call-by-Value PCF
András KovácsKovács, András University of Gothenburg Efficient Evaluation with Controlled Definition Unfolding
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: Or, Lambda: The Ultimate Document
Neel KrishnaswamiKrishnaswami, Neel University of CambridgeUnited Kingdom Student Research Competition Co-Chair in Organizing Committee for POPL 2024 How to Give a Talk Focusing on Refinement Typing (TOPLAS) 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 UniversityRussia 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 Session Chair of Session 8: Concurrency, Program and System Verification, Closing (part of VMCAI ) Interpolation and Quantifiers in Ortholattices Orthologic with Axioms Automated Verification: Session Preview
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 Tuomas LaakkonenLaakkonen, Tuomas Quantinuum Optimal compilation of parametrised quantum circuits
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 Ecole PolytechniqueFrance A diagram editor to mechanize categorical proofs
Ori LahavLahav, Ori Tel Aviv UniversityIsrael Session Chair of Session 5: keynote, Program and System Verification (part of VMCAI ) A Denotational Approach to Release/Acquire Concurrency 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
Christopher LamLam, Christopher University of Illinois at Urbana-ChampaignUnited States Committee Member in AV Committee for POPL 2024
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 Session Chair of Second Session (part of PLMW @ POPL) Panel Generating Well-Typed Terms that are not "Useless" PLMW Co-Chair in Organizing Committee within the PLMW @ POPL-track
Adrienne LancelotLancelot, Adrienne Inria, LIX Ecole Polytechnique, IRIF Université Paris CitéFrance Normal Form Bisimulations by Value
Vincent LaporteLaporte, Vincent IMDEA Software Institute, Spain Committee Member in Program Committee within the PriSC-track
Christophe LaprunLaprun, Christophe RED HAT Kepler Watt Store: Kepler Software Watt Watcher Store
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é Paris Cité / IRIFFrance Polymorphic Type Inference for Dynamic Languages
Alan LawrenceLawrence, Alan Quantinuum GUPPY: Pythonic Quantum-Classical Programming Introducing BRAT
Didier Le BotlanLe Botlan, Didier LAAS-CNRS, INSA-ToulouseFrance Project and Conquer: Fast Quantifier Elimination for Checking Petri Nets Reachability
Edward LeeLee, Edward University of WaterlooCanada Capturing Types (TOPLAS)
K. Rustan M. LeinoLeino, K. Rustan M. AmazonUnited States Steering Committee Chair in Steering Committee within the Dafny-track
Louis LemonnierLemonnier, Louis Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, Laboratoire Méthodes Formelles Quantum and Classical Control (work-in-progress)
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 Mechanizing Abstract Interpretation 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
Paul Blain LevyLevy, Paul Blain University of BirminghamUnited Kingdom Game-enriched categories
Alexander K. LewLew, Alexander K. Massachusetts Institute of TechnologyUnited States Effective Sequential Monte Carlo for Language Model Probabilistic Programs Toward Probabilistic Coarse-to-Fine Program Synthesis Reverse mode ADEV via YOLO: tangent estimators transpose to gradient estimators
Ondřej LhotákLhoták, Ondřej University of WaterlooCanada Capturing Types (TOPLAS)
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
Jialin LiLi, Jialin National University of Singapore, Singapore Formal Methods to Save the Earth
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 Regular Abstractions for Array Systems Parikh's Theorem Made Symbolic Ramsey Quantifiers in Linear Arithmetics String Solving for Verification
Yu-Yang LinLin, Yu-Yang Queen Mary University of London Fully Abstract Normal Form Bisimulation for Call-by-Value PCF
Sam LindleyLindley, Sam University of EdinburghUnited Kingdom Session Chair of Higher-Order Effectful Programs (part of POPL ) Effect Handlers: Session Preview 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
Xulei LiuLiu, Xulei Delft University of TechnologyNetherlands Session Chair of Friday Breakfast Session Previews (part of POPL Session Previews) Towards a Language-parametric DSL for Refactoring (Short Paper)
Y. Annie LiuLiu, Y. Annie Stony Brook UniversityUnited States Incremental Computation: What Is the Essence? (Invited Contribution) Committee Member in Program Committee within the PADL-track
Yiyun LiuLiu, Yiyun University of Pennsylvania 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
Thomas LivelyLively, Thomas GoogleUnited States A Brief Tour of Binaryen
Francesco LogozzoLogozzo, Francesco FacebookUnited States Committee Member in Organizing Committee within the N40AI -track
Giuseppe LomurnoLomurno, Giuseppe University of Pisa, Italy Effect Semantics for Quantum Protocols 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
Rana LullaLulla, Rana University of California San Diego GPU-Accelerated Synthesis of Boolean Circuits
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 QueenslandAustralia ReLU Hull Approximation
Julian MackayMackay, Julian Victoria University of WellingtonNew Zealand Object Capabilities
Anil MadhavapeddyMadhavapeddy, Anil University of Cambridge, UKUnited Kingdom Session Chair of Keynote (part of PROPL) Discussion and brain storming: How can the CS/PL community help address the current planetary crises? 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 INRIAFrance 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 Session Chair of Automated Verification (part of POPL ) 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 Algorithmic Verification: Session Preview Efficient Matching of Regular Expressions with Lookaround Assertions
Vikash K. MansinghkaMansinghka, Vikash K. Massachusetts Institute of TechnologyUnited States Effective Sequential Monte Carlo for Language Model Probabilistic Programs Toward Probabilistic Coarse-to-Fine Program Synthesis Reverse mode ADEV via YOLO: tangent estimators transpose to gradient estimators MultiSPPL: extending SPPL with multivariate leaf nodes
William ManskyMansky, William University of Illinois ChicagoUnited States Session Chair of Weak Memory and Concurrent Separation Logic (part of POPL ) 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
Louis Marott NormannMarott Normann, Louis University of CopenhagenDenmark Partial Evaluation of Reversible Flowchart Programs
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 Securing Verified IO Programs Against Unverified Code in F* Pulse: Proof-oriented Programming in a Concurrent Separation Logic DSL in F*
Hidehiko MasuharaMasuhara, Hidehiko Tokyo Institute of TechnologyJapan An Intrinsically Typed Compiler for Algebraic Effect Handlers
Cristina MatacheMatache, Cristina University of Edinburgh An algebraic theory of named threads (work in progress)
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 Formal Methods to Save the Earth 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, Université de Toulouse, CNRS, Toulouse INP, UT3, Toulouse Displayed Monoidal Categories for the Semantics of Linear Logic
Laurent MauborgneMauborgne, Laurent Absint GmbH Short talks: Past, Present and Future of AI
Conor McBrideMcBride, Conor University of Strathclyde Monoidal Adventures Introducing BRAT
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 Portfolio Solving for Dafny Enhancing Proof Stability
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
Rafael MenezesMenezes, Rafael University of ManchesterUnited Kingdom ESBMC-CHERI: Towards Verification of C/C++ Programs for CHERI Platforms with ESBMC
Lucy MenonMenon, Lucy Northeastern University Session Chair of Thursday Lunch Session Previews (part of POPL Session Previews)
Eric MercerMercer, Eric Brigham Young UniversityUnited States Verifying Dafny Contract Integrity
Denis MerigouxMerigoux, Denis INRIAFrance Committee Member in Program Committee within the POPL -track
Dominique MeryMery, Dominique Université de Lorraine, CNRS, INRIA / LORIA & Telecom Nancy, FranceFrance Short talks: Past, Present and Future of AI
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 Princeton UniversityUnited States Session Chair of Types 1 (part of POPL ) Managing undergraduate research, as mentor and mentee Speaker in Speakers within the PLMW @ POPL-track Committee Member in Program Committee within the POPL -track
Luka MiljakMiljak, Luka Delft University of TechnologyNetherlands Towards a Language-parametric DSL for Refactoring (Short Paper)
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 Session Chair of Invited Talks 1 (part of N40AI ) Sound Abstract Nonexploitability Analysis Generation of Violation Witnesses by Under-Approximating Abstract Interpretation 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 Session Chair of Session 2: SAT, SMT and Automated Reasoning (part of VMCAI ) Short talks: Past, Present and Future of AI 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 Session Chair of Session 3 (part of POCL ) 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 University of LisbonPortugal Parametric Subtyping for Structural Parametric Polymorphism
J. Garrett MorrisMorris, J. Garrett University of IowaUnited States Soundly Handling Linearity
Luke MorrisMorris, Luke University of Florida Categorical Composition of Discrete Exterior Calculus Climate Models
Andreas Tor MortensenMortensen, Andreas Tor Department of Computer Science, Aalborg University A type-safe generalized editor calculus (Extended Abstract)
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
João P. MoutinhoMoutinho, João P. PASQAL SAS Qadence: a differentiable interface for digital-analog programs
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
Reed MullanixMullanix, Reed McMaster UniversityUnited States asai: a Library for Compiler Diagnostics
Stefan K. MullerMuller, Stefan K. Illinois Institute of TechnologyUnited States Session Chair of Types 2 (part of POPL ) 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
Ilya MuravjovMuravjov, Ilya Saint Petersburg State University Optimization of the Context-Free Language Reachability Matrix-Based Algorithm
Andrzej MurawskiMurawski, Andrzej University of OxfordUnited Kingdom Operational Algorithmic Game Semantics 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
Minh NguyenNguyen, Minh University of BristolUnited Kingdom Fluid: towards transparent, self-explanatory research outputs
Kim NguyễnNguyễn, Kim Université Paris-SaclayFrance Polymorphic Type Inference for Dynamic Languages
Lê Thành Dũng NguyễnNguyễn, Lê Thành Dũng École normale supérieure de LyonFrance Invisible pebbles and the geometry of affine higher-order tree transducers
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 WienAustria 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 On Modelling Heap Invariants for Type Systems in Dafny Work in Progress: Modelling Incorrect Programs in the Open World with Dafny Object Capabilities 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. Lacework; University College LondonUnited Kingdom AI for the People My Journey to the Dark Side: Under-Approximation, Incorrectness, Proof 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
Martin OderskyOdersky, Martin EPFLSwitzerland Inside the Scala Capture Checker Capturing Types (TOPLAS)
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 Toward a Live, Rich, Composable, and Collaborative Planetary Compute Engine 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 Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving Guaranteed Bounds for Discrete Probabilistic Programs with Loops via Generating Functions A slice sampler for the Indian Buffet Process: expressivity in nonparametric probabilistic programming
Dominic OrchardOrchard, Dominic University of Kent, UK and University of Cambridge, UKUnited Kingdom Discussion and brain storming: How can the CS/PL community help address the current planetary crises? 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 Session Chair of Quantum Computing (part of POPL ) Domesticating Automation CLOVER: Closed-Loop Verifiable Code Generation Quantum Computing: Session Preview 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 PiR (πr): Probabilistic Interpretation of Robustness
Jens PalsbergPalsberg, Jens University of California, Los Angeles (UCLA)United States Quantum Abstract Interpretation 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 Session Chair of Session 3 (part of GALOP) 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 Session Chair of Session 1 (part of O'Hearn Fest) Designing Wait-free Weak Reference Counting Some things I wish I hadn’t seen Concurrent Mutation must go
Francesco ParoliniParolini, Francesco Sorbonne UniversitéFrance Sound Abstract Nonexploitability Analysis
Lionel ParreauxParreaux, Lionel HKUST (The Hong Kong University of Science and Technology)China 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 using the Lovász Local Lemma
Daniele PautassoPautasso, Daniele Università di Torino Higher Order Bayesian Networks, Exactly
Andreas PavlogiannisPavlogiannis, Andreas Aarhus UniversityDenmark Session Chair of Algorithmic Verification (part of POPL ) 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
Anurudh PeduriPeduri, Anurudh Ruhr University Bochum QbC: Quantum Correctness by Construction
Doron PeledPeled, Doron Bar Ilan UniversityIsrael TP-DejaVu: Combining Operational and Declarative Runtime Verification
Hila PelegPeleg, Hila TechnionIsrael Synthesis 2: Session Preview 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
Roly PereraPerera, Roly University of Cambridge/University of BristolUnited Kingdom Fluid: towards transparent, self-explanatory research outputs
Simona PerriPerri, Simona University of Calabria, Italy Forgetting Techniques for Optimizing ASP-based Stream Reasoning
Alberto PettorossiPettorossi, Alberto University of Rome Tor Vergata; IASI-CNRItaly A Historical Perspective on Program Transformation and Recent Developments (Invited Contribution)
Simon Peyton JonesPeyton Jones, Simon Epic Games United Kingdom Solving constraints during type inference Type inference for application spines Committee Member in Program Committee within the POPL -track
Frank PfenningPfenning, Frank Carnegie Mellon University, USA Parametric Subtyping for Structural Parametric Polymorphism
Artem PianykhPianykh, Artem Facebook London Retrofitting Null-Safety into Java
Jean Pichon-PharabodPichon-Pharabod, Jean Aarhus UniversityDenmark CertiCoq-Wasm: Verified compilation from Coq to WebAssembly Proving capability safety in the presence of indirect sentries 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 Session Chair of Business Meeting (part of CPP) Session Chair of Interactive Proof Development (part of CPP) 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 Session Previews Co-Chair in Organizing Committee for POPL 2024 Session Chair of Wednesday Morning Sessions Previews (part of POPL Session Previews) Incremental Proof Development in Dafny with Module-Based Induction Committee Member in Program Committee within the PriSC-track
Nir PitermanPiterman, Nir University GothenburgSweden Fair omega-Regular Games
Andrew M. PittsPitts, Andrew M. University of Cambridge Committee Member in Program Committee within the POPL -track
Gordon PlotkinPlotkin, Gordon Google Homomorphic Reverse Differentiation of Iteration Effect Handlers for Choice-Based Learning
Andreas PodelskiPodelski, Andreas University of FreiburgGermany Session Chair of Session 7: Probabilistic and Quantum Programs, Neural Networks (part of VMCAI ) Short talks: Past, Present and Future of AI 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
Hernán Ponce de LeónPonce de León, Hernán Huawei Dresden Research CenterGermany On the need for available, functional, and reusable memory models
Enrico PontelliPontelli, Enrico New Mexico State University Committee Member in Program Committee within the PADL-track
Andrei PopescuPopescu, Andrei University of SheffieldUnited Kingdom Session Chair of Mechanized Proofs (part of POPL ) The Complex(ity) Landscape of Checking Infinite Descent Nominal Recursors as Epi-Recursors 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
Maurizio ProiettiProietti, Maurizio IASI-CNRItaly A Historical Perspective on Program Transformation and Recent Developments (Invited Contribution)
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
Drew PurvesPurves, Drew Google DeepMindUnited Kingdom Setting the stage for AI for biodiversity
Romain PéchouxPéchoux, Romain Université de Lorraine; CNRS; Inria; LORIAFrance A feasible and unitary programming language with quantum control Quantum and Classical Control (work-in-progress)
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 System-level weak memory models: The need for formalisation, ISA semantics integration and model diversity 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 Meta, Inc.United States Concurrency: Session Preview
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 Session Chair of Medley (part of POPL ) Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations Synthesis 1: Session Preview Committee Member in Program Committee within the POPL -track
Weihao QuQu, Weihao Boston UniversityUnited States 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 Mikhail R. GadelhaR. Gadelha, Mikhail IgaliaBrazil ESBMC-CHERI: Towards Verification of C/C++ Programs for CHERI Platforms with ESBMC
Azalea RaadRaad, Azalea Imperial College LondonUnited Kingdom Session Chair of Separation Logic (part of POPL ) Session Chair of Types (part of Incorrectness) Session Chair of Concurrency, Security, & Hyper-properties (part of Incorrectness) Welcome Introduction Welcome Under-approximation for Scalable Bug Detection 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 Committee Member in AV Committee for POPL 2024 Gradual Verification for Smart Contracts Optimization of a Gradual Verifier: Lazy evaluation of Iso-recursive Predicates as Equi-recursive at Runtime
Steven RamsayRamsay, Steven University of BristolUnited Kingdom Session Chair of Types 3 (part of POPL ) 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 Session Chair of Verification (part of PLanQC) 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 MathematicsGermany 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
George RautaRauta, George University of Florida Categorical Composition of Discrete Exterior Calculus Climate Models
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
Giles RegerReger, Giles University of ManchesterUnited Kingdom ESBMC-CHERI: Towards Verification of C/C++ Programs for CHERI Platforms with ESBMC
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 UCLFrance Arm Architecture and Formal Artifacts: Memory Model and Instruction Semantics
Mathys RennelaRennela, Mathys INRIA ParisFrance Session Chair of Quantum Types (part of PLanQC) Committee Member in Program Committee within the PLanQC-track Program Chair in Organizing Committee within the PLanQC-track
Lisa RennelsRennels, Lisa University of California at BerkeleyUnited States Building Open Source Software for Climate Change Research — Lessons Learned from Mimi.jl
John ReppyReppy, John University of Chicago, USA Session Chair of Parallelism (part of POPL ) Parallelism: Session Preview
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 MIT 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 Session Chair of Session 6: Abstract Interpretation (part of VMCAI ) 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
Nikolaj Rossander KristensenRossander Kristensen, Nikolaj Department of Computer Science, Aalborg University A type-safe generalized editor calculus (Extended Abstract)
Andreas RossbergRossberg, Andreas IndependentGermany Lightning Talks - please sign up! Organizer in Organizing Committee within the WAW-track
Bastien RousseauRousseau, Bastien Aarhus UniversityDenmark Proving capability safety in the presence of indirect sentries
Reuben N. S. RoweRowe, Reuben N. S. Royal Holloway University of LondonUnited Kingdom The Complex(ity) Landscape of Checking Infinite Descent
Craig RoyRoy, Craig Quantinuum Introducing BRAT
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 The Potential of Information-Flow Control Research for helping GDPR Compliance From Theory to Practice: Crafting Differential Privacy Systems with Haskell Speaker in Speakers within the PLMW @ POPL-track Committee Member in Program Committee within the PEPM-track
Melody RuthRuth, Melody University of California San Diego GPU-Accelerated Synthesis of Boolean Circuits
Sukyoung RyuRyu, Sukyoung KAISTSouth Korea Generating Executable Specification from Formal Semantics of WebAssembly 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
Mooly SagivSagiv, Mooly Tel Aviv UniversityIsrael Trust but Verify: Scaling Deductive Verification with Abstract Interpretation
Irmak SaglamSaglam, Irmak Max Planck Institute for Software Systems (MPI-SWS)Germany Fair omega-Regular Games Solving Two-Player Games under Progress Assumptions
Ken SakayoriSakayori, Ken University of TokyoJapan Ownership Types for Verification of Programs with Pointer Arithmetic 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
V.R. SathiyanarayanaSathiyanarayana, V.R. MPI-SWS Positive Almost-Sure Termination – Complexity and Proof Rules
Ryosuke SatoSato, Ryosuke University of TokyoJapan Productivity Verification for Functional Programs by Reduction to Termination Verification Borrowable Fractional Ownership Types for Verification
Ina SchaeferSchaefer, Ina KITGermany QbC: Quantum Correctness by Construction
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
David SchmidtSchmidt, David Short talks: Past, Present and Future of AI
Anne-Kathrin SchmuckSchmuck, Anne-Kathrin Max Planck Institute for Software SystemsGermany Fair omega-Regular Games
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 Session Chair of Session 4: Infinite State Systems, Runtime Verification (part of VMCAI ) Correctness Witness Validation by Abstract Interpretation
Dominik SeitzSeitz, Dominik PASQAL SAS Qadence: a differentiable interface for digital-analog programs
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 SestoftSestoft, Peter IT University of CopenhagenDenmark The Genesis of Mix: Early Days of Self-Applicable Partial Evaluation (Invited Contribution)
Peter SewellSewell, Peter University of CambridgeUnited Kingdom Session Chair of Session 1 (part of POCL ) Keynote: Can we reason about the security of concurrent systems code? Welcome 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
Guruprerana ShabadiShabadi, Guruprerana École Polytechnique, Institut Polytechnique de ParisFrance Towards programmatic reinforcement learning: the case of deterministic gridworlds
Bhakti ShahShah, Bhakti University of Chicago Committee Member in AV Committee for POPL 2024 Video Chair in Organizing Committee for POPL 2024 Integrating Dependency Building with Document Checking in Coq A Lean Formalization of Cedar
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 Compositional Development of Certified System Software 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 Closing Remarks 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
Fedor ShmarovShmarov, Fedor The University of Manchester ESBMC-CHERI: Towards Verification of C/C++ Programs for CHERI Platforms with ESBMC
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 Session Chair of Keynote 2 (part of POPL ) Associate Chair in Program Committee within the POPL -track
Mário SilvaSilva, Mário LORIA, Université de Lorraine A feasible and unitary programming language with quantum control
Ben SimnerSimner, Ben Relaxed systems semantics and how we (hope to) reason above it
Jeremy SingerSinger, Jeremy University of GlasgowUnited Kingdom Sealed with a Library Call: Memory Allocators Should Track Capability Seal Operations
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
PARUL SINGHSINGH, PARUL RED HAT Kepler Watt Store: Kepler Software Watt Watcher Store
Satnam SinghSingh, Satnam GroqUnited States Session Chair of Domain-Specific Languages (part of POPL ) Committee Member in Program Committee within the POPL -track
Kartik SinghalSinghal, Kartik QuantinuumUnited States GUPPY: Pythonic Quantum-Classical Programming
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
Seyon SivarajahSivarajah, Seyon Quantinuum GUPPY: Pythonic Quantum-Classical Programming
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
J Tanner SlagelSlagel, J Tanner NASA A Temporal Differential Dynamic Logic Formal Embedding
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
Thomas SomersSomers, Thomas Radboud University Linking Session-Typed Channels in Separation Logic
Harald SondergaardSondergaard, Harald The University of MelbourneAustralia The Genesis of Mix: Early Days of Self-Applicable Partial Evaluation (Invited Contribution)
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
Kunjian SongSong, Kunjian The University of Manchester ESBMC-CHERI: Towards Verification of C/C++ Programs for CHERI Platforms with ESBMC
Thodoris SotiropoulosSotiropoulos, Thodoris ETH ZurichSwitzerland API-driven Program Synthesis for Testing Static Typing Implementations
Matthieu SozeauSozeau, Matthieu InriaFrance Session with the Coq Development Team MetaCoq Tutorial Committee Member in Program Committee within the WITS-track
Bas SpittersSpitters, Bas Aarhus UniversityDenmark CertiCoq-Wasm: Verified compilation from Coq to WebAssembly Specifying Smart Contract with Hax and ConCert A formal security analysis of Blockchain voting
Bas SpittersSpitters, Bas 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 Session Chair of Language Design (part of PADL) 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 Session Chair of Session 2 (part of POCL ) 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
Peter Buus SteffensenSteffensen, Peter Buus Department of Computer Science, Aalborg University A type-safe generalized editor calculus (Extended Abstract)
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
Lucas StinchcombeStinchcombe, Lucas Simon Fraser University Polynomial-time Classical Simulation of Roetteler’s Shifted Bent Function Algorithm
Sam StitesStites, Sam Northeastern University A Multi-language Approach to Probabilistic Program Inference
Elias StormeStorme, Elias KU LeuvenBelgium Secure Calling Conventions for CHERI Capability Machines in Practice (Work in Progress) 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
Vince SzabóSzabó, Vince Delft University of Technology Compilation Quotient (CQ): A Metric for the Compilation Hardness of Programming Languages
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
Izumi TanakaTanaka, Izumi University of TokyoJapan Ownership Types for Verification of Programs with Pointer Arithmetic
Wenhao TangTang, Wenhao University of EdinburghUnited Kingdom Session-Typed Effect Handlers Soundly Handling Linearity
Éric TanterTanter, Éric University of Chile Securing Verified IO Programs Against Unverified Code in F*
Runzhou TaoTao, Runzhou Columbia UniversityUnited States Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions A Case for Synthesis of Recursive Quantum Unitary Programs
Philip TascheTasche, Philip University of TwenteNetherlands Deductive Verification of Parameterized Embedded Systems modeled in SystemC
Joseph TassarottiTassarotti, Joseph NYUUnited States Session Chair of Probabilistic Programs and Testing / Verifying Contracts (part of Dafny) Session Chair of Testing and Teaching / Comparison (part of Dafny) Day opening Day closing 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 Effect Semantics for Quantum Protocols 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 Session Chair of Business Meeting (part of CPP) Session Chair of Mechanized separation logic (part of CPP) Business Meeting 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 Steering Committee Member in Steering Committee within the CPP-track Conference Chair in Organizing Committee within the CPP-track
Laura TitoloTitolo, Laura AMA/NASA LaRCUnited States A Temporal Differential Dynamic Logic Formal Embedding
Ben L. TitzerTitzer, Ben L. Carnegie Mellon UniversityUnited States WALI: A thin Linux kernel interface for WebAssembly 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 Portfolio Solving for Dafny Dafny Test Generation
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 Session Chair of Business Meeting (part of CPP) Session Chair of Isabelle, PVS (part of CPP) Business Meeting 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 PfComp: A Verified Compiler for Packet Filtering Leveraging Binary Decision Diagrams
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 Quantum Controlled Measurements via Program Transformation Enriched Presheaf Model of Quantum FPC
Syouki TsuyamaTsuyama, Syouki Tokyo Institute of TechnologyJapan An Intrinsically Typed Compiler for Algebraic Effect Handlers
Omkar TuppeTuppe, Omkar IIT BombayIndia On-The-Fly Static Analysis via Dynamic Bidirected Dyck Reachability
Nikos TzevelekosTzevelekos, Nikos Queen Mary University of LondonUnited Kingdom Session Chair of Session 2 (part of GALOP) Fully Abstract Normal Form Bisimulation for Call-by-Value PCF 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 Session Chair of Invited Talks 2 (part of N40AI ) Session Chair of Session 3: Security and Privacy, Model Checking and Synthesis (part of VMCAI ) 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 Optimal compilation of parametrised quantum circuits Committee Member in Program Committee within the PLanQC-track
Niels van der Weidevan der Weide, Niels Radboud University Displayed Monoidal Categories for the Semantics of Linear Logic Univalent Double Categories
Rob van Glabbeekvan Glabbeek, Rob The University of Edinburgh Shoggoth - A Formal Foundation for Strategic Rewriting
Antoine Van MuylderVan Muylder, Antoine KU Leuven Internal and Observational Parametricity for Cubical Agda
Orpheas van Rooijvan Rooij, Orpheas Radboud University A Substructural Type and Effect System
Thomas Van StrydonckVan Strydonck, Thomas KULeuven Secure Calling Conventions for CHERI Capability Machines in Practice (Work in Progress) Secure Calling Conventions for CHERI Capability Machines in Practice (Work in Progress)
Julien VanegueVanegue, Julien Bloomberg, USAUnited States Towards Temporal Adversarial Logic Bi-abductive adversarial program synthesis
Alexa VanHattumVanHattum, Alexa Wellesley CollegeUnited States Committee Member in Program Committee within the PriSC-track
Gabriele VanoniVanoni, Gabriele IRIF, Université Paris Cité Session Chair of Thursday Morning Session Previews (part of POPL Session Previews) Invisible pebbles and the geometry of affine higher-order tree transducers 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 Session Chair of Session 2 (part of PriSC) Committee Member in Program Committee within the PriSC-track
Lionel Vaux AuclairVaux Auclair, Lionel University of Aix-MarseilleFrance Taylor Expansion is Game Semantics
Niki VazouVazou, Niki IMDEA Software Institute Refinement Types from Light to Deep Verification Panel Types 1: Session Preview Mechanizing Refinement Types Speaker in Speakers within the PLMW @ POPL-track Panelist in Panelists within the PLMW @ POPL-track
Margus VeanesVeanes, Margus Microsoft Research Lean Formalization of Extended Regular Expression Matching with Lookarounds
Ekaterina VerbitskaiaVerbitskaia, Ekaterina JetBrains Research; Constructor University BremenSerbia A Case Study in Functional Conversion and Mode Inference in miniKanren
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
Andre VidelaVidela, Andre University Of Strathclyde Binding Syntax for Dependently-Typed Programs
Thomas VigourouxVigouroux, Thomas VERIMAG - UGAFrance Function synthesis for maximizing model counting
Jules VillardVillard, Jules MetaUnited Kingdom Session Chair of Program Analysis (part of POPL ) Introduction 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
Michael VollmerVollmer, Michael University of KentUnited Kingdom Rust on Morello
Matthijs VákárVákár, Matthijs Utrecht University Session Chair of Third Session (part of LAFI) Session Chair of Poster and Interactive Session (part of LAFI) Session Chair of Second Session (part of LAFI) Session Chair of First Session (part of LAFI) 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 Philip WadlerWadler, Philip University of Edinburgh Medley: Session Preview
Andrew WagnerWagner, Andrew Northeastern University All the Binaries Together: A Semantic Approach to Application Binary Interfaces
Luke WagnerWagner, Luke Fastly What is a WebAssembly component (and why?)
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 QbC: Quantum Correctness by Construction 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 Session Chair of Keynote & Termination analysis (part of PEPM) Opening 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
Theo WangWang, Theo University of Oxford Exploring the limitations of Contextual Modal Type Theory for Multi-Stage Programming
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 The state of Morello and CHERI Committee Member in Organizing Committee within the POCL -track
Conrad WattWatt, Conrad Nanyang Technological UniversitySingapore Virtualization Chair in Organizing Committee for POPL 2024 Lightning Talks - please sign up! 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
Jonathan WeinbergerWeinberger, Jonathan Johns Hopkins University Formalizing the ∞-categorical Yoneda lemma
Stephanie WeirichWeirich, Stephanie University of PennsylvaniaUnited States Internalizing Indistinguishability with Dependent Types
Georg WeissenbacherWeissenbacher, Georg TU WienAustria Finding counterexamples to ∀∃ hyperproperties
Aleksander WennersteenWennersteen, Aleksander PASQAL SAS Qadence: a differentiable interface for digital-analog programs
Sam WestrickWestrick, Sam Carnegie Mellon UniversityUnited States Panel DisLog: A Separation Logic for Disentanglement Automatic Parallelism Management Panelist in Panelists within the PLMW @ POPL-track
Lauren WhiteWhite, Lauren NASAUnited States A Temporal Differential Dynamic Logic Formal Embedding
Leo WhiteWhite, Leo Jane Street Committee Member in Program Committee within the PADL-track
John WickersonWickerson, John Imperial College LondonUnited Kingdom Publicity Co-Chair in Organizing Committee for POPL 2024 Session Chair of Session 1 (part of The Future of Weak Memory) Session Chair of Session 2 (part of The Future of Weak Memory) Welcome Domain-Specific Languages: Session Preview Extraordinary Meeting: The Publicity Chairs Reflect on the Peer-Review Process Organizing Chair in Organizing Committee within the The Future of Weak Memory-track
Thomas WiesWies, Thomas New York UniversityUnited States Committee Member in Program Committee within the POPL -track
Reinhard WilhelmWilhelm, Reinhard Saarland UniversityGermany Short talks: Past, Present and Future of AI
Max WillseyWillsey, Max UC BerkeleyUnited States Committee Member in Program Committee within the POPL -track
Hans WinderixWinderix, Hans KU Leuven Compiler Support for Control-Flow Linearization Using Architectural Mimicry
Tobias WinklerWinkler, Tobias RWTH Aachen UniversityGermany Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs
Theo WinterhalterWinterhalter, Theo INRIA SaclayFrance The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography Securing Verified IO Programs Against Unverified Code in F* MetaCoq Tutorial PC Member in Program Committee within the CPP-track
Jenna Wise (DiVincenzo)Wise (DiVincenzo), Jenna Purdue University Gradual Verification for Smart Contracts Sound Gradual Verification with Symbolic Execution
Konrad WitaszczykWitaszczyk, Konrad University of Cambridge, UK The state of Morello software and projects
Sebastian WolffWolff, Sebastian New York UniversityUnited States Chair in Artifact Evaluation Committee within the VMCAI -track
James WorrellWorrell, James University of OxfordUnited Kingdom On Learning Polynomial Recursive Programs
Tobias WrigstadWrigstad, Tobias Uppsala UniversitySweden On Modelling Heap Invariants for Type Systems in Dafny Work in Progress: Modelling Incorrect Programs in the Open World with Dafny Concurrent Mutation must go
Huiling WuWu, Huiling East China Normal UniversityChina Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
Jinhua WuWu, Jinhua Shanghai Jiao Tong UniversityChina Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules
Nicolas WuWu, Nicolas Imperial College LondonUnited Kingdom The Evolution of Effects Modular Higher-Order Effects Algebraic Effects Meet Hoare Logic in Cubical Agda Speaker in Speakers within the PLMW @ POPL-track
Xiaodi WuWu, Xiaodi 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 Program Committee within the POPL -track
Kobe WullaertWullaert, Kobe Delft University of Technology Displayed Monoidal Categories for the Semantics of Linear Logic
june wunderwunder, june Boston University Pipelines and Beyond: Graph Types for ADTs with Futures
X Anxhelo XhebrajXhebraj, Anxhelo Purdue UniversityUnited States Flan: An Expressive and Efficient Datalog Compiler for Program Analysis
Li-yao XiaXia, Li-yao University of Edinburgh Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Tongtong XiangXiang, Tongtong Amazon Web Services Enhancing Proof Stability
Shengping XiaoXiao, Shengping East China Normal UniversityChina Model-Guided Synthesis for LTL over Finite Traces
Ningning XieXie, Ningning University of TorontoCanada Effect Handlers for Choice-Based Learning Committee Member in Selection Committee within the POPL Student Research Competition-track Committee Member in Program Committee within the WITS-track
Ruifeng XieXie, Ruifeng Peking University Fusing Direct Manipulations into Functional Programs
Ming XuXu, Ming East China Normal UniversityChina Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
Yicong XuXu, Yicong East China Normal UniversityChina Model-Guided Synthesis for LTL over Finite Traces
Y Jeremy YallopYallop, Jeremy University of CambridgeUnited Kingdom Unboxed data constructors -- or, how cpp decides a halting problem Committee Member in Program Committee within the PEPM-track
Hongseok YangYang, Hongseok KAIST; IBSSouth Korea Session Chair of Session 2 (part of O'Hearn Fest) Peter's early work on parametricity, and why it still matters to me Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets
Tengshun YangYang, Tengshun SKLCS, Institute of Software, Chinese Academy of Sciences & University of Chinese Academy of Sciences Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving
Zhixuan YangYang, Zhixuan Imperial College LondonUnited Kingdom Algebraic Effects Meet Hoare Logic in Cubical Agda
Jianan YaoYao, Jianan Columbia UniversityUnited States Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions
Roland H. C. YapYap, Roland H. C. National University of Singapore, Singapore Committee Member in Program Committee within the PADL-track
Ugur Y. YavuzYavuz, Ugur Y. Boston University A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability
Richie YeungYeung, Richie University of Oxford Optimal compilation of parametrised quantum circuits
Kwangkeun YiYi, Kwangkeun Seoul National University Program Synthesis via Bi-directional Reduced-product Abstract Interpretation
Jacob YoungYoung, Jacob University of Maryland SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog Compilation
Neringa YoungYoung, Neringa Lithuania Treasurer & Conference Manager in Organizing Committee for POPL 2024
Weixin YuYu, Weixin University Of Michigan Testing Specifications In Dafny
Z Fabian ZaiserZaiser, Fabian University of Oxford VMC: a Dafny Library for Verified Monte Carlo Algorithms Guaranteed Bounds for Discrete Probabilistic Programs with Loops via Generating Functions
Yannick ZakowskiZakowski, Yannick InriaFrance An abstract, certified account of Operational Game Semantics Committee Member in Program Committee within the CoqPL-track Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the GALOP-track
Vadim ZalivaZaliva, Vadim University of Cambridge, UKUnited States Session Chair of Compiler / Program Verification (part of CPP) CHERI C semantics PC Member in Program Committee within the CPP-track
Vladimir ZamdzhievZamdzhiev, Vladimir InriaFrance Quantum and Classical Control (work-in-progress)
Tao ZanZan, Tao Longyan University Fusing Direct Manipulations into Functional Programs
Marco ZanellaZanella, Marco University of Padova, ItalyItaly Abstract Interpretation-Based Feature Importance for Support Vector Machines
Jessica ZangariZangari, Jessica Università della CalabriaItaly Session Chair of Knowledge Representation and Learning (part of PADL) Rethinking Answer Set Programming Templates Forgetting Techniques for Optimizing ASP-based Stream Reasoning Committee Member in Program Committee within the PADL-track
Steve ZdancewicZdancewic, Steve University of PennsylvaniaUnited States Optimal Program Synthesis via Abstract Interpretation Associate Chair in Program Committee within the POPL -track Steering Committee Member in Steering Committee within the CPP-track
Yankai ZengZeng, Yankai The University of Texas at Dallas Automated Interactive Domain-Specific Conversational Agents that Understand Human Dialogs
Georg ZetzscheZetzsche, Georg MPI-SWSGermany Ramsey Quantifiers in Linear Arithmetics Reachability in Continuous Pushdown VASS Committee Member in Program Committee within the POPL -track
Stefan ZetzscheZetzsche, Stefan Amazon Web ServicesUnited Kingdom Session Chair of Code Generation (part of Dafny) Session Chair of Applications (part of Dafny) Session Chair of Proof Stability / Brittleness / Scale (part of Dafny) VMC: a Dafny Library for Verified Monte Carlo Algorithms Day opening Day closing Program Chair in Program Chairs within the Dafny-track Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Bohua ZhanZhan, Bohua Institute of Software, Chinese Academy of SciencesChina Efficient Local Search for Nonlinear Real Arithmetic
Danfeng ZhangZhang, Danfeng Duke UniversityUnited States Student Research Competition Co-Chair in Organizing Committee for POPL 2024 Co-chair in Selection Committee within the POPL Student Research Competition-track
Hengchu ZhangZhang, Hengchu Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Ling ZhangZhang, Ling Shanghai Jiao Tong UniversityChina Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules
Linpeng ZhangZhang, Linpeng University College LondonUnited Kingdom Quantitative Weakest Hyper Pre
Min ZhangZhang, Min East China Normal UniversityChina Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training
Xing ZhangZhang, Xing Peking UniversityChina Fusing Direct Manipulations into Functional Programs
Yihong ZhangZhang, Yihong University of WashingtonUnited States Efficient Bottom-Up Synthesis for Programs with Local Variables
Yizhou ZhangZhang, Yizhou University of WaterlooCanada Committee Member in Selection Committee within the POPL Student Research Competition-track Committee Member in Program Committee within the POPL -track
Zhen ZhangZhang, Zhen Utah State UniversityUnited States Committee Member in Program Committee within the VMCAI -track
Eric ZhaoZhao, Eric University of MichiganUnited States Total Type Error Localization and Recovery with Holes
Qiyuan ZhaoZhao, Qiyuan National University of SingaporeSingapore Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
Zhulien ZhelezchevZhelezchev, Zhulien University of Bristol Graphical Primitive Recursion For String Diagrams
Dapeng ZhiZhi, Dapeng East China Normal UniversityChina Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training
Tan Zhi-XuanZhi-Xuan, Tan Massachusetts Institute of Technology Effective Sequential Monte Carlo for Language Model Probabilistic Programs Committee Member in Program Committee within the LAFI-track
Litao ZhouZhou, Litao Shanghai Jiao Tong University; University of Hong KongChina VST-A: A Foundationally Sound Annotation Verifier Compositional Programming with Full Iso-recursive Types Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Xiangyu ZhouZhou, Xiangyu University of Michigan Efficient Bottom-Up Synthesis for Programs with Local Variables
Zhe ZhouZhou, Zhe Purdue University Type-Based Incorrectness Reasoning
Shaopeng ZhuZhu, Shaopeng Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Ekaterina ZhuchkoZhuchko, Ekaterina Tallinn University of Technology Session Chair of Friday Lunch Session Previews (part of POPL Session Previews) Lean Formalization of Extended Regular Expression Matching with Lookarounds
Noam ZilbersteinZilberstein, Noam Cornell UniversityUnited States Session Chair of Opening (part of Incorrectness) Session Chair of Logics and Program Analysis (part of Incorrectness) Welcome Organizer in Organizing Committee within the Incorrectness-track Committee Member in Program Committee within the Incorrectness-track
Conrad ZimmermanZimmerman, Conrad Brown UniversityUnited States Sound Gradual Verification with Symbolic Execution
Margherita ZorziZorzi, Margherita Committee Member in Program Committee within the PLanQC-track
Lenore ZuckZuck, Lenore UICUnited States Committee Member in Program Committee within the VMCAI -track

POPL 2024 Contributors

Results (1145)

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia