POPL 2024 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (1141)

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 Flan: An Expressive and Efficient Datalog Compiler for Program Analysis Rhyme: A Data-Centric Expressive Query Language for Nested Data Structures
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 All the Binaries Together: A Semantic Approach to Application Binary Interfaces Steering Committee Member in Steering Committee within the PriSC-track RichWasm: Bringing Safe, Fine-Grained, Shared Memory Interoperability to WebAssembly Towards a Categorical Model of the Lilac Separation Logic
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 Sound Gradual Verification with Symbolic Execution Gradual Verification for Smart Contracts
Jade AlglaveAlglave, Jade Arm and University College LondonUnited Kingdom Arm Architecture and Formal Artifacts: Memory Model and Instruction Semantics Elegance and generosity are scientific values - And other things I've learned from Peter
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 Predictive Monitoring against Pattern Regular Languages Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
Carlo AngiuliAngiuli, Carlo Indiana UniversityUnited States Committee Member in Program Committee within the POPL -track
Andrew W. AppelAppel, Andrew W. Princeton University VST-A: A Foundationally Sound Annotation Verifier Committee Member in Program Committee within the POPL -track VCFloat2: Floating-point error analysis in Coq
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 Polynomial Time and Dependent types Session Chair of Formalizations of Category Theory (part of CPP) 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 BachBach, Casper Delft University of TechnologyNetherlands Committee Member in Program Committee within the POPL -track Towards a Language-parametric DSL for Refactoring (Short Paper)
Jakub BachurskiBachurski, Jakub University of CambridgePoland Embedding Pointful Array Programming in Python
Michael BackesBackes, Michael Cispa Helmholtz Center for Information Security Secure Composition of SPECTRE Mitigations Lifting Compiler Security Properties to Stronger Attackers: the Speculation Case
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 Rust on Morello Welcome Organizing Committee in Organizing Committee within the The Future of Weak Memory-track
Kevin BatzBatz, Kevin RWTH Aachen UniversityGermany Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs Caesar: A Verifier for 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 Types 3: Session Preview Committee Member in Program Committee within the POPL -track Session Chair of Session 3 (part of O'Hearn Fest) Pete's Footprints
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 An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic Asynchronous Probabilistic Couplings in Higher-Order Separation Logic Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement The Logical Essence of Well-Bracketed Control Flow The Essence of Generalized Algebraic Data Types Modular Denotational Semantics for Effects with Guarded Interaction Trees Proving capability safety in the presence of indirect sentries
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 Mechanized Proofs: Session Preview Session Chair of Business Meeting (part of CPP) Session Chair of Logic and Beyond (part of CPP) 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 Total Type Error Localization and Recovery with Holes Toward a Live, Rich, Composable, and Collaborative Planetary Compute Engine
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
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 Indexed Types for a Statically Safe WebAssembly Committee Member in Program Committee within the PriSC-track Session Chair of Session 2 (part of WITS)
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 Committee Member in Program Committee within the PEPM-track Session Chair of Session 4 (part of WITS) Yaffle: A New Core for Idris 2 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 Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Session Chair of Session 3 (part of PriSC) When Obfuscations Preserve Cryptographic Constant-Time Committee Member in Program Committee within the PriSC-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 Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-Deterministic Observers Effect Semantics for Quantum Protocols
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 ) How Hard is Weak-Memory Testing? Committee Member in Program Committee within the POPL -track Heterogeneous concurrency -- a new frontier for weak memory
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 Committee Member in Program Committee within the CoqPL-track Session Chair of Verified Compilation (part of CPP) 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
Jocelyn Qiaochu ChenChen, Jocelyn 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 Committee Member in Program Committee within the PriSC-track Capabilities for safe cross-language interoperability
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 Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Breandan ConsidineConsidine, Breandan McGill UniversityCanada A Tree Sampler for Bounded Context-Free Languages
É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 Rust on Morello Programmers love mind-bogglingly complicated weak memory models
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 New York University Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation
Patrick CousotCousot, Patrick Is Peter Correct or Incorrect?
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 On Model-Checking Higher-Order Effectful Programs On Interaction, Efficiency, and Reversibility Invited Speaker in Invited Speakers within the GALOP-track Circuit Width Estimation via Effect Typing and Linear Dependency (Extended Abstract)
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 CEA ListFrance Compiler Support for Control-Flow Linearization Using Architectural Mimicry 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
Ana de Almeida Borgesde Almeida Borges, Ana University of Barcelona and Formal Vindications S.L. UTC time, formally verified
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 Internal and Observational Parametricity for Cubical Agda Committee Member in Program Committee within the POPL -track Session Chair of Session 4 (part of PriSC) Secure Calling Conventions for CHERI Capability Machines in Practice (Work in Progress) Steering Committee Member in Steering Committee within the PriSC-track Secure Calling Conventions for CHERI Capability Machines in Practice (Work in Progress) Proving capability safety in the presence of indirect sentries
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 Semantic Code Refactoring for Abstract Data Types Programming-by-Demonstration for Long-Horizon Robot Tasks
Rayna DimitrovaDimitrova, Rayna CISPA Helmholtz Center for Information Security Solving Infinite-State Games via Acceleration Session Chair of Session 1: Openning, Keynote, SAT, SMT and Automated Reasoning (part of VMCAI ) 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
Jenna DiVincenzo (Wise)DiVincenzo (Wise), Jenna Purdue University Sound Gradual Verification with Symbolic Execution Gradual Verification for Smart Contracts
Hasra DodampegamaDodampegama, Hasra University of Birmingham Explanation and Knowledge Acquisition in Ad Hoc Teamwork
Mike DoddsDodds, Mike Galois, Inc. Weak Memory and Concurrent Separation Logic: Session Preview How Do We Know That Weak Memory Matters?
Stephen DolanDolan, Stephen Jane Street Unboxed data constructors -- or, how cpp decides a halting problem Committee Member in Program Committee within the POPL -track Why Languages Should Preserve Load-Store Order
Alastair F. DonaldsonDonaldson, Alastair F. Imperial College LondonUnited Kingdom Publicity Co-Chair in Organizing Committee for POPL 2024 Extraordinary Meeting: The Publicity Chairs Reflect on the Peer-Review Process Associate Chair in Program Committee within the POPL -track Randomised Testing of the Dafny Compiler
Rui DongDong, Rui University of MichiganUnited States Efficient Bottom-Up Synthesis for Programs with Local Variables Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Committee Member in Artifact Evaluation Committee within the VMCAI -track
Brijesh DongolDongol, Brijesh University of SurreyUnited Kingdom A Reachability Logic for a Weak Memory Model with Promises A Fully Verified Persistency Library Session Chair of Session 3 (part of The Future of Weak Memory) Session Chair of Session 4 (part of The Future of Weak Memory) Welcome 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 ) Program Chair in Program Committee within the POPL -track Opening Panel Panelist in Panelists within the PLMW @ POPL-track Later Credits: A Case Study in the Unreasonable Effectiveness of Separation Logic
Sophia DrossopoulouDrossopoulou, Sophia Imperial College LondonUnited Kingdom Session Chair of Concurrency (part of POPL ) Committee Member in Program Committee within the POPL -track Object Capabilities Concurrent Mutation must go
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) Introducing BRAT GUPPY: Pythonic Quantum-Classical Programming 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 Committee Member in Artifact Evaluation Committee within the VMCAI -track A Denotational Approach to Release/Acquire Concurrency
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 Logical Foundations: Session Preview Session Chair of Logical Foundations (part of POPL ) 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 Types 2: Session Preview Jane Street Board Game Night Session Chair of Session 1 (part of WITS) 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 UniversityTurkey 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 Higher Order Bayesian Networks, Exactly Declarative Languages for Safe AI Normal Form Bisimulations by Value
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 Commutativity Simplifies Proofs of Parameterized Programs Coarser Equivalences for Causal Concurrency A New Perspective on Commutativity in Verification
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 Machine Learning Meets Program Synthesis Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic 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
Justine FrankFrank, Justine 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 Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-Deterministic Observers Effect Semantics for Quantum Protocols
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 Gradual Typing and Verification: Session Preview Session Chair of Gradual Typing and Verification (part of POPL ) 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 Hong Ge: Bayesian inference using probabilistic programming JuliaBUGS: A Graph-Based Probabilistic Programming Language using BUGS syntax
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 T. GellerGeller, Adam T. 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 Program Analysis: Session Preview Monotonicity and the Precision of Program Analysis Committee Member in Program Committee within the POPL -track Session Chair of Short Talks (part of N40AI ) Short talks: Past, Present and Future of AI Committee Member in Organizing Committee within the N40AI -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 Committee Member in Program Committee within the PriSC-track Session Chair of Fourth Session (part of PLMW @ POPL) PLMW Chair in Organizing Committee within the PLMW @ POPL-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 Orthologic with Axioms Interpolation and Quantifiers in Ortholattices
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) Declarative Languages for Safe AI Automated Interactive Domain-Specific Conversational Agents that Understand Human Dialogs 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 Committee Member in Program Committee within the PADL-track
Jens Oliver GutsfeldGutsfeld, Jens Oliver Westfälische Wilhelm-Universität Münster (WWU), GermanyGermany Deciding Asynchronous Hyperproperties for Recursive Programs A Navigation Logic for Recursive Programs with Dynamic Thread Creation
Armaël GuéneauGuéneau, Armaël Université Paris-Saclay - CNRS - ENS Paris-Saclay - InriaFrance The Logical Essence of Well-Bracketed Control Flow Thunks and Debits in Separation Logic with Time Credits Melocoton: A Program Logic for Verified Interoperability Between OCaml and C (Invited Talk)
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 String Solving for Verification Parikh's Theorem Made Symbolic
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 An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic Morello Cerise: proving secure encapsulation (work in progress)
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 UniversityDenmark Asynchronous Probabilistic Couplings in Higher-Order Separation Logic The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography
Vahid HashemiHashemi, Vahid AUDI AGGermany AGNES: Abstraction-guided Framework for Deep Neural Networks Security
Daniel HausmannHausmann, Daniel University of GothenburgSweden Generic Model Checking for Modal Fixpoint Logics in COOL-MC Fair omega-Regular Games
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 ) Committee Member in Program Committee within the POPL -track Session Chair of History of PEPM (part of PEPM) In memoriam Neil Deaton Jones
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 Cedar: A language for expressing fast, safe, and fine-grained authorization policies Session Chair of Synthesis 2 (part of POPL ) Committee Member in Program Committee within the POPL -track Improving the Stability of Type Safety Proofs in Dafny
Kesha HietalaHietala, Kesha Amazon Web ServicesUnited States PC Member in Program Committee within the CPP-track Committee Member in Program Committee within the PLanQC-track
Mathieu HilaireHilaire, Mathieu ENS Paris SaclayFrance Resilience and Home-Space for WSTS
Daniel HillerströmHillerström, Daniel Huawei Zurich Research CenterSwitzerland Soundly Handling Linearity Stack Switching in WebAssembly with Effect Handlers
Jonas Kastberg HinrichsenHinrichsen, Jonas Kastberg Aarhus University, DenmarkDenmark Verified Message-Passing Concurrency in Iris: Separation Logic Meets Session Types Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
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 Higher-Order Effectful Programs: Session Preview Committee Member in Program Committee within the POPL -track Session Chair of Third Session (part of PLMW @ POPL) Committee Member in Organizing Committee within the PLMW @ 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 Machine and Automata Learning: Session Preview 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 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 Type Theory: Session Preview Session Chair of Type Theory (part of POPL ) Committee Member in Program Committee within the POPL -track asai: a Library for Compiler Diagnostics Session Chair of Formalizing Mathematics (part of CPP) 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 ) Securing Verified IO Programs Against Unverified Code in F* Committee Member in Program Committee within the POPL -track Steering Committee Member in Steering Committee within the PriSC-track The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography 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 MultiSPPL: extending SPPL with multivariate leaf nodes Reverse mode ADEV via YOLO: tangent estimators transpose to gradient estimators
Chung-Kil HurHur, Chung-Kil Seoul National UniversitySouth Korea In-order execution nails every weak memory behavior
Graham HuttonHutton, Graham University of Nottingham, UKUnited Kingdom Quotient Haskell: Lightweight Quotient Types for All
Sander HuyghebaertHuyghebaert, Sander Vrije Universiteit Brussel Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Secure Calling Conventions for CHERI Capability Machines in Practice (Work in Progress) Secure Calling Conventions for CHERI Capability Machines in Practice (Work in Progress)
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 Committee Member in Program Committee within the POPL -track 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 GALOP-track
Jules JacobsJacobs, Jules Radboud University Nijmegen Verified Message-Passing Concurrency in Iris: Separation Logic Meets Session Types Probabilistic Programs: Session Preview Session Chair of Probabilistic Programs (part of POPL ) Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing Panel Panelist in Panelists within the PLMW @ POPL-track
Swen JacobsJacobs, Swen CISPAGermany Parameterized Verification of Disjunctive Timed Networks Automatic and Incremental Repair for Speculative Information Leaks
Alec JacobsonJacobson, Alec University of Toronto Sparse Differentiation in Computer Graphics
Suresh JagannathanJagannathan, Suresh Purdue UniversityUnited States Type-Based Incorrectness Reasoning
Georges-Axel JaloyanJaloyan, Georges-Axel Amazon Web Services Enhancing Proof Stability
Tomi JanhunenJanhunen, Tomi Tampere UniversityFinland Committee Member in Program Committee within the PADL-track
Patrik JanssonJansson, Patrik Chalmers University of 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 String Solving for Verification Parikh's Theorem Made Symbolic
Ranjit JhalaJhala, Ranjit University of California at San DiegoUnited States Mechanizing Refinement Types
Limin JiaJia, Limin Carnegie Mellon University Committee Member in Program Committee within the POPL -track Automatically Enforcing Rust Trait Properties
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 A Formalization of Core Why3 in Coq Towards a Categorical Model of the Lilac Separation Logic
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 Selection Committee within the POPL Student Research Competition-track Committee Member in Program Committee within the CoqPL-track
K Robin KaarsgaardKaarsgaard, Robin University of Southern DenmarkDenmark With a Few Square Roots, Quantum Computing is as Easy as Pi Committee Member in Program Committee within the PLanQC-track
Anan KabahaKabaha, Anan Technion, Israel Institute of TechnologyIsrael Verification of Neural Networks’ Local Differential Classification Privacy
Younesse KaddarKaddar, Younesse University of OxfordUnited Kingdom Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets Declarative Languages for Safe AI
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 Automata and Complexity: Session Preview Caesar: A Verifier for Probabilistic Programs Quantitative Weakest Hyper Pre Hoare-Like Triples and Kleene Algebras with Top and Tests Belief Programming in Partially Observable Probabilistic Environments Committee Member in Program Committee within the LAFI-track
Ohad KammarKammar, Ohad University of EdinburghUnited Kingdom LGBTQ+ Host in Organizing Committee for POPL 2024 Committee Member in Diversity, Equity, and Inclusion Committee within the POPL Diversity, Equity and Inclusion-track Foundations of Type-Driven Probabilistic Modelling Committee Member in Selection Committee within the POPL Student Research Competition-track Shoggoth - A Formal Foundation for Strategic Rewriting Committee Member in Steering Committee within the LAFI-track A Denotational Approach to Release/Acquire Concurrency
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 Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs Caesar: A Verifier for 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) 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
Donnacha Oisín KidneyKidney, Donnacha 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 Proofcraft 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 Commutativity Simplifies Proofs of Parameterized Programs Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Petrification: Software Model Checking for Programs with Dynamic Thread Management
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 Productivity Verification for Functional Programs by Reduction to Termination Verification Ownership Types for Verification of Programs with Pointer Arithmetic Borrowable Fractional Ownership Types for Verification
Tomoaki KobayashiKobayashi, Tomoaki Tohoku UniversityJapan Complete Stream Fusion for Software-Defined Radio
Mark KochKoch, Mark Quantinuum Introducing BRAT GUPPY: Pythonic Quantum-Classical Programming
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 Verified Message-Passing Concurrency in Iris: Separation Logic Meets Session Types Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing Unification for Subformula Linking under Quantifiers 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 How Hard is Weak-Memory Testing? On-The-Fly Static Analysis via Dynamic Bidirected Dyck Reachability
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 Co-chair in Selection Committee within the POPL Student Research Competition-track Focusing on Refinement Typing (TOPLAS) How to Give a Talk Speaker in Speakers within the PLMW @ POPL-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 Automated Verification: Session Preview Orthologic with Axioms Session Chair of Session 8: Concurrency, Program and System Verification, Closing (part of VMCAI ) Interpolation and Quantifiers in Ortholattices
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 ) Co-chair in Program Committee within the VMCAI -track A Denotational Approach to Release/Acquire Concurrency A case against semantic dependencies
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 Generating Well-Typed Terms that are not "Useless" Session Chair of Second Session (part of PLMW @ POPL) Panel 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 Introducing BRAT GUPPY: Pythonic Quantum-Classical Programming
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 MetaCoq Tutorial Martin-Löf à la Coq
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 Toward Probabilistic Coarse-to-Fine Program Synthesis Reverse mode ADEV via YOLO: tangent estimators transpose to gradient estimators Effective Sequential Monte Carlo for Language Model Probabilistic Programs
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 String Solving for Verification Parikh's Theorem Made Symbolic Ramsey Quantifiers in Linear Arithmetics Regular Abstractions for Array Systems
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 Effect Handlers: Session Preview Session Chair of Higher-Order Effectful Programs (part of POPL ) 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 Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-Deterministic Observers Effect Semantics for Quantum Protocols
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 ) Committee Member in Program Committee within the POPL -track Towards Modular Specification and Verification of Concurrent Hypervisor-based Isolation Modularizing CPU Semantics for Virtualization
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 Toward Probabilistic Coarse-to-Fine Program Synthesis MultiSPPL: extending SPPL with multivariate leaf nodes Reverse mode ADEV via YOLO: tangent estimators transpose to gradient estimators Effective Sequential Monte Carlo for Language Model Probabilistic Programs
William ManskyMansky, William University of Illinois ChicagoUnited States Session Chair of Weak Memory and Concurrent Separation Logic (part of POPL ) An Iris Instance for Verifying CompCert C Programs Committee Member in Program Committee within the POPL -track Compositional Verification of Concurrent C Programs with Search Structure Templates
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 Pulse: Proof-oriented Programming in a Concurrent Separation Logic DSL in F* Securing Verified IO Programs Against Unverified Code 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 How Hard is Weak-Memory Testing? Coarser Equivalences for Causal Concurrency Predictive Monitoring against Pattern Regular Languages Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic Formal Methods to Save the Earth
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 Introducing BRAT Monoidal Adventures
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 ) Committee Member in Program Committee within the POPL -track Managing undergraduate research, as mentor and mentee Speaker in Speakers within the PLMW @ 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 ) Committee Member in Organizing Committee within the N40AI -track Generation of Violation Witnesses by Under-Approximating Abstract Interpretation Sound Abstract Nonexploitability Analysis
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 Short talks: Past, Present and Future of AI Session Chair of Session 2: SAT, SMT and Automated Reasoning (part of VMCAI ) Committee Member in Program Committee within the VMCAI -track Memory simulations, security and optimization in a verified compiler
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 ) Disentanglement with Futures, State, and Interaction Pipelines and Beyond: Graph Types for ADTs with Futures 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 Guaranteed Bounds for Discrete Probabilistic Programs with Loops via Generating Functions Operational Algorithmic Game Semantics 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 Committee Member in Program Committee within the POPL -track Programme Committee in Program Committee within the Dafny-track
Markus Müller-OlmMüller-Olm, Markus University of MünsterGermany Deciding Asynchronous Hyperproperties for Recursive Programs A Navigation Logic for Recursive Programs with Dynamic Thread Creation
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 Co-chair in Diversity, Equity, and Inclusion Committee within the POPL Diversity, Equity and Inclusion-track Unified Compositional Formal Methods: Exact Separation Logic and the Gillian Platform for Correctness and Incorrectness Reasoning
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 Learn 'em Dafny Colouring Flags with Dafny & Idris Work in Progress: Modelling Incorrect Programs in the Open World with Dafny On Modelling Heap Invariants for Type Systems in Dafny Object Capabilities
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 Capturing Types (TOPLAS) Inside the Scala Capture Checker
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 Deciding Asynchronous Hyperproperties for Recursive Programs A Navigation Logic for Recursive Programs with Dynamic Thread Creation
Emilia OikarinenOikarinen, Emilia University of HelsinkiFinland Committee Member in Program Committee within the PADL-track
Cyrus OmarOmar, Cyrus University of MichiganUnited States Total Type Error Localization and Recovery with Holes Toward a Live, Rich, Composable, and Collaborative Planetary Compute Engine
Moran OmerOmer, Moran Bar Ilan University, IsraelIsrael TP-DejaVu: Combining Operational and Declarative Runtime Verification
C.-H. Luke OngOng, C.-H. Luke NTU A slice sampler for the Indian Buffet Process: expressivity in nonparametric probabilistic programming Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving Guaranteed Bounds for Discrete Probabilistic Programs with Loops via Generating Functions
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 Automated Interactive Domain-Specific Conversational Agents that Understand Human Dialogs Using Logic Programming and Kernel-Grouping for Improving Interpretability of Convolutional Neural Networks
Oded PadonPadon, Oded VMware ResearchUnited States Quantum Computing: Session Preview Session Chair of Quantum Computing (part of POPL ) An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification Domesticating Automation CLOVER: Closed-Loop Verifiable Code Generation
Shankara PailoorPailoor, Shankara University of Texas at AustinUnited States Semantic Code Refactoring for Abstract Data Types
Abhinandan PalPal, Abhinandan University of BirminghamUnited Kingdom PiR (πr): Probabilistic Interpretation of Robustness Abstract Interpretation-Based Feature Importance for Support Vector Machines
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 A slice sampler for the Indian Buffet Process: expressivity in nonparametric probabilistic programming Committee Member in Program Committee within the LAFI-track Session Chair of Session 3 (part of GALOP) Committee Member in Program Committee within the GALOP-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 Concurrent Mutation must go Some things I wish I hadn’t seen Session Chair of Session 1 (part of O'Hearn Fest) Designing Wait-free Weak Reference Counting
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 ) How Hard is Weak-Memory Testing? On-The-Fly Static Analysis via Dynamic Bidirected Dyck Reachability Committee Member in Program Committee within the POPL -track
Jennifer PaykinPaykin, Jennifer Intel LabsUnited States Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the PLanQC-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 SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog Compilation A Case for Synthesis of Recursive Quantum Unitary Programs 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 Committee Member in Program Committee within the POPL -track Solving constraints during type inference Type inference for application spines
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 An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic Committee Member in Program Committee within the POPL -track CertiCoq-Wasm: Verified compilation from Coq to WebAssembly Proving capability safety in the presence of indirect sentries
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 EPFLSwitzerland Session Previews Co-Chair in Organizing Committee for POPL 2024 Session Chair of Wednesday Morning Sessions Previews (part of POPL Session Previews) Committee Member in Program Committee within the PriSC-track Incremental Proof Development in Dafny with Module-Based Induction
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 Effect Handlers for Choice-Based Learning Homomorphic Reverse Differentiation of Iteration
Andreas PodelskiPodelski, Andreas University of FreiburgGermany Commutativity Simplifies Proofs of Parameterized Programs Short talks: Past, Present and Future of AI Session Chair of Session 7: Probabilistic and Quantum Programs, Neural Networks (part of VMCAI )
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 Committee Member in Selection Committee within the POPL Student Research Competition-track Session Chair of Mechanized Proofs (part of POPL ) Nominal Recursors as Epi-Recursors The Complex(ity) Landscape of Checking Infinite Descent 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 Committee Member in Program Committee within the POPL -track Steering Committee Member in Steering Committee within the PriSC-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 Quantum and Classical Control (work-in-progress) A feasible and unitary programming language with quantum control
Pierre-Marie PédrotPédrot, Pierre-Marie INRIAFrance Committee Member in Program Committee within the POPL -track Martin-Löf à la Coq
Thibaut PéramiPérami, Thibaut University of Cambridge An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic System-level weak memory models: The need for formalisation, ISA semantics integration and model diversity
George PîrleaPîrlea, George National University of Singapore Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
Q Shaz QadeerQadeer, Shaz FacebookUnited States Scaling Verification of Concurrent Programs with the Civl Verifier
Shaz QadeerQadeer, Shaz Meta, Inc.United States Concurrency: Session Preview
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 Synthesis 1: Session Preview Session Chair of Medley (part of POPL ) Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations 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 Organizer in Organizing Committee within the Incorrectness-track Committee Member in Program Committee within the Incorrectness-track Under-approximation for Scalable Bug Detection Welcome Organizing Committee in Organizing Committee within the The Future of Weak Memory-track Introduction 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 POPL -track Committee Member in Program Committee within the VMCAI -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 Optimization of a Gradual Verifier: Lazy evaluation of Iso-recursive Predicates as Equi-recursive at Runtime Gradual Verification for Smart Contracts
Steven RamsayRamsay, Steven University of BristolUnited Kingdom Session Chair of Types 3 (part of POPL ) Ill-Typed Programs Don't Evaluate Committee Member in Program Committee within the POPL -track Ill-Typed Programs Don't Evaluate
Robert RandRand, Robert University of ChicagoUnited States Committee Member in Program Committee within the VMCAI -track Session Chair of Verification (part of PLanQC) 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 Committee Member in Organizing Committee within the N40AI -track Abstract Interpretation-Based Feature Importance for Support Vector Machines Committee Member in Program Committee within the VMCAI -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 Co-chair in Diversity, Equity, and Inclusion Committee within the POPL Diversity, Equity and Inclusion-track Pulse: Proof-oriented Programming in a Concurrent Separation Logic DSL in F*
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 Parallelism: Session Preview Session Chair of Parallelism (part of POPL )
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 Organizing Committee in Organizing Committee within the N40AI -track Session Chair of Session 6: Abstract Interpretation (part of VMCAI ) Committee Member in Program Committee within the VMCAI -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 Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs Flan: An Expressive and Efficient Datalog Compiler for Program Analysis Committee Member in Program Committee within the POPL -track Rhyme: A Data-Centric Expressive Query Language for Nested Data Structures
Neil Julien RossRoss, Neil Julien Dalhousie UniversityCanada Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the PLanQC-track Committee Member in Organizing Committee within the PLanQC-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
June RousseauRousseau, June 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 Speaker in Speakers within the PLMW @ POPL-track From Theory to Practice: Crafting Differential Privacy Systems with Haskell 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 Committee Member in Program Committee within the POPL -track Generating Executable Specification from Formal Semantics of WebAssembly
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 Solving Two-Player Games under Progress Assumptions Fair omega-Regular Games
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 MPI-SWSGermany Solving Two-Player Games under Progress Assumptions Committee Member in Program Committee within the VMCAI -track
Anne-Kathrin SchmuckSchmuck, Anne-Kathrin Max Planck Institute for Software SystemsGermany Fair omega-Regular Games
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 Co-chair in Programme Chairs within the PADL-track Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
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 An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic Committee Member in Program Committee within the POPL -track Keynote: Can we reason about the security of concurrent systems code? Session Chair of Session 1 (part of POCL ) Workshop Chair in Organizing Committee within the POCL -track Welcome Organizing Committee in Organizing Committee within the The Future of Weak Memory-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 A Lean Formalization of Cedar Integrating Dependency Building with Document Checking in Coq
Amir ShaikhhaShaikhha, Amir University of EdinburghUnited Kingdom Structured Tensor Algebra for Efficient Discrete Probabilistic Inference
Chung-chieh ShanShan, Chung-chieh Indiana UniversityUnited States Committee Member in Steering Committee within the LAFI-track
Zhong ShaoShao, Zhong Yale UniversityUnited States Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules Compositional Development of Certified System Software 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 The Essence of Generalized Algebraic Data Types Functorial Syntax for All
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 Committee Member in Program Committee within the POPL -track Abstract Interpretation for Automatic Differentiation Committee Member in Program Committee within the VMCAI -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 Program Committee within the POPL -track Committee Member in Program Committee within the PEPM-track Committee Member in Programme Committee within the PROPL-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 MetaCoq Tutorial Session with the Coq Development Team Committee Member in Program Committee within the WITS-track
Bas SpittersSpitters, Bas Aarhus UniversityDenmark Specifying Smart Contract with Hax and ConCert CertiCoq-Wasm: Verified compilation from Coq to WebAssembly A formal security analysis of Blockchain voting
Bas SpittersSpitters, Bas 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 Committee Member in Program Committee within the POPL -track Co-chair in Program Committee within the CoqPL-track
Sam StatonStaton, Sam University of OxfordUnited Kingdom Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets A slice sampler for the Indian Buffet Process: expressivity in nonparametric probabilistic programming
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 The Essence of Generalized Algebraic Data Types Decalf: A Directed, Effectful Cost-Aware Logical Framework
Michel SteuwerSteuwer, Michel TU Berlin; University of EdinburghGermany Guided Equality Saturation Shoggoth - A Formal Foundation for Strategic Rewriting
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 A Case for Synthesis of Recursive Quantum Unitary Programs Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions
Philip TascheTasche, Philip University of TwenteNetherlands Deductive Verification of Parameterized Embedded Systems modeled in SystemC
Joseph TassarottiTassarotti, Joseph NYUUnited States Asynchronous Probabilistic Couplings in Higher-Order Separation Logic 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 Program Chair in Program Chairs within the Dafny-track
Enrico TassiTassi, Enrico INRIAFrance Committee Member in Program Committee within the CoqPL-track PC Member in Program Committee within the CPP-track
Zachary TatlockTatlock, Zachary University of WashingtonUnited States Sparse Differentiation in Computer Graphics
Landon TaylorTaylor, Landon Utah State UniversityUnited States Committee Member in Artifact Evaluation Committee within the VMCAI -track
Gabriele TedeschiTedeschi, Gabriele University of Pisa, Italy Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-Deterministic Observers Effect Semantics for Quantum Protocols
Anastasios TemperekidisTemperekidis, Anastasios Aristotle University of ThessalonikiGreece TP-DejaVu: Combining Operational and Declarative Runtime Verification
Joshua B. TenenbaumTenenbaum, Joshua B. Massachusetts Institute of TechnologyUnited States Toward Probabilistic Coarse-to-Fine Program Synthesis
Tachio TerauchiTerauchi, Tachio Waseda UniversityJapan Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers
Romain TetleyTetley, Romain VsCoq 2, new foundations
K. S. ThejaswiniThejaswini, K. S. The University of Warwick Solving Two-Player Games under Progress Assumptions
René ThiemannThiemann, René University of Innsbruck Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
Ramanathan S. ThinniyamThinniyam, Ramanathan S. Uppsala University Reachability in Continuous Pushdown VASS
Andrew ThomasThomas, Andrew University of Cambridge JuliaBUGS: A Graph-Based Probabilistic Programming Language using BUGS syntax
Jiaxu TianTian, Jiaxu East China Normal UniversityChina Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training
Sarah TilscherTilscher, Sarah Technische Universität MünchenGermany Correctness Witness Validation by Abstract Interpretation
Amin TimanyTimany, Amin Aarhus UniversityDenmark Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement The Logical Essence of Well-Bracketed Control Flow Modular Denotational Semantics for Effects with Guarded Interaction Trees Committee Member in Program Committee within the POPL -track Session Chair of Business Meeting (part of CPP) Session Chair of Mechanized separation logic (part of CPP) 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 Committee Member in Program Committee within the POPL -track WALI: A thin Linux kernel interface for WebAssembly
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 Associate Chair in Program Committee within the POPL -track Improving the Stability of Type Safety Proofs in Dafny
Dmitriy TraytelTraytel, Dmitriy University of CopenhagenDenmark Session Chair of Business Meeting (part of CPP) Session Chair of Isabelle, PVS (part of CPP) 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 VMC: a Dafny Library for Verified Monte Carlo Algorithms Generation of Verified Assembly Code Using Dafny and Reinforcement Learning Randomised Testing of the Dafny Compiler Steering Committee Chair in Steering Committee within the Dafny-track Committee Member in Steering Committee within the LAFI-track PC Member in Program Committee within the CPP-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 Enriched Presheaf Model of Quantum FPC Quantum Controlled Measurements via Program Transformation
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 Committee Member in Program Committee within the POPL -track Session Chair of Session 2 (part of GALOP) Fully Abstract Normal Form Bisimulation for Call-by-Value PCF 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 Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers Committee Member in Program Committee within the POPL -track Automating Relational Verification of Infinite-State Programs
Caterina UrbanUrban, Caterina Inria & École Normale Supérieure \| Université PSLFrance Monotonicity and the Precision of Program Analysis Session Chair of Invited Talks 2 (part of N40AI ) Organizing Committee in Organizing Committee within the N40AI -track Session Chair of Session 3: Security and Privacy, Model Checking and Synthesis (part of VMCAI ) Abstract Interpretation-Based Feature Importance for Support Vector Machines
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) Higher Order Bayesian Networks, Exactly Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Invisible pebbles and the geometry of affine higher-order tree transducers
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 Types 1: Session Preview Mechanizing Refinement Types Refinement Types from Light to Deep Verification Panel 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 ) Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the Incorrectness-track Introduction 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 Efficient CHAD 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 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 Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training
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 State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of SciencesChina 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 DisLog: A Separation Logic for Disentanglement Automatic Parallelism Management Panel 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 Domain-Specific Languages: Session Preview Extraordinary Meeting: The Publicity Chairs Reflect on the Peer-Review Process 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 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
Théo WinterhalterWinterhalter, Théo INRIA SaclayFrance MetaCoq Tutorial Securing Verified IO Programs Against Unverified Code in F* The Last Yard: Foundational End-to-End Verification of High-Speed Cryptography PC Member in Program Committee within the CPP-track
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 Work in Progress: Modelling Incorrect Programs in the Open World with Dafny On Modelling Heap Invariants for Type Systems in 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 Algebraic Effects Meet Hoare Logic in Cubical Agda The Evolution of Effects Speaker in Speakers within the PLMW @ POPL-track Modular Higher-Order Effects
Xiaodi WuWu, Xiaodi University of MarylandUnited States SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog Compilation A Case for Synthesis of Recursive Quantum Unitary Programs 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 Committee Member in Selection Committee within the POPL Student Research Competition-track Effect Handlers for Choice-Based Learning 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 Probabilistic programming interfaces for random graphs: Markov categories, graphons, and nominal sets Session Chair of Session 2 (part of O'Hearn Fest) Peter's early work on parametricity, and why it still matters to me
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 Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the CoqPL-track An abstract, certified account of Operational Game Semantics Committee Member in Program Committee within the GALOP-track
Vadim ZalivaZaliva, Vadim University of Cambridge, UKUnited States CHERI C semantics Session Chair of Compiler / Program Verification (part of CPP) 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 Reachability in Continuous Pushdown VASS Ramsey Quantifiers in Linear Arithmetics Committee Member in Program Committee within the POPL -track
Stefan ZetzscheZetzsche, Stefan Amazon Web ServicesUnited Kingdom Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track 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
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 Compositional Programming with Full Iso-recursive Types VST-A: A Foundationally Sound Annotation Verifier 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 (1141)

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia