POPL 2023 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (857)

A Andreas AbelAbel, Andreas Gothenburg UniversitySweden Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the PADL-track
Coşku AcayAcay, Coşku Cornell UniversityUnited States Universally Composable Security for Program Partitioning
Reynald AffeldtAffeldt, Reynald National Institute of Advanced Industrial Science and Technology (AIST)Japan Semantics of Probabilistic Programs using S-Finite Kernels in Coq Committee Member in Program Committee within the CPP-track
Alejandro AguirreAguirre, Alejandro Aarhus UniversityDenmark Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice
Amal AhmedAhmed, Amal Northeastern University, USAUnited States Program Chair in Organizing Committee for POPL 2023 Session Chair of Welcome (part of POPL ) Session Chair of Invited Talk (part of POPL ) Introduction Semantic Intermediate Representations for Sound Language Interoperability New foundations for probabilistic separation logic Program Chair in Program Committee within the POPL -track
Benedikt AhrensAhrens, Benedikt TU Delft, The NetherlandsNetherlands Formalizing Monoidal Categories and Actions for Syntax with Binders
Mosaad Al ThokairAl Thokair, Mosaad University of Illinois at Urbana-ChampaignUnited States Dynamic Race Detection with O(1) Samples
Aws AlbarghouthiAlbarghouthi, Aws University of Wisconsin-MadisonUnited States Session Chair of Solvers (part of VMCAI) What Can Program Analysis Say About Data Bias?
Jonathan AldrichAldrich, Jonathan Carnegie Mellon UniversityUnited States Using a Proof Assistant to Teach PL Theory, Without the Overhead
Christopher AlexanderAlexander, Christopher GE Research UAV Compliance Checking using Answer Set Programming and Minimal Explanations towards Compliance (Application Paper)
Ramsha AliAli, Ramsha University of KlagenfurtAustria Flexible Job-shop Scheduling for Semiconductor Manufacturing with Hybrid Answer Set Programming (Application Paper)
Guillaume AllaisAllais, Guillaume University of St AndrewsUnited Kingdom Modular Construction of Multi-sorted Free Extensions
Xavier AllamigeonAllamigeon, Xavier Inria and Ecole Polytechnique A Formal Disproof of Hirsch Conjecture
Rajeev AlurAlur, Rajeev University of PennsylvaniaUnited States Executing Microservice Applications on Serverless, Correctly A Robust Theory of Series Parallel Graphs
Nada AminAmin, Nada Harvard UniversityUnited States Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the PEPM-track
Basavesh Ammanaghatta ShivakumarAmmanaghatta Shivakumar, Basavesh Max Planck Institute for Security and Privacy (MPI-SP)Germany Robust Constant-Time Cryptography
Cezar-Constantin AndriciAndrici, Cezar-Constantin MPI-SPGermany Securely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typed Interfaces Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Sebastian AngelAngel, Sebastian University of Pennsylvania; Microsoft ResearchUnited States Executing Microservice Applications on Serverless, Correctly
Denise AngilicaAngilica, Denise Università Della CalabriaItaly Integrating ASP-based incremental reasoning in the videogame development workflow (Application Paper)
Carlo AngiuliAngiuli, Carlo Carnegie Mellon UniversityUnited States An Order-Theoretic Analysis of Universe Polymorphism
Danil AnnenkovAnnenkov, Danil ConcordiumDenmark Formalising Decentralised Exchanges in Coq Committee Member in Program Committee within the CoqPL-track
Timos AntonopoulosAntonopoulos, Timos Yale UniversityUnited States An Algebra of Alignment for Relational Verification Committee Member in Program Committee within the ProLaLa-track
Arvind ArasuArasu, Arvind Microsoft Research FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
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 Building Information Modeling Using Constraint Logic Programming (Extended Abstract) Jury-trial Story Construction and Analysis using Goal-directed Answer Set Programming Committee Member in Program Committee within the ProLaLa-track
Luca ArnaboldiArnaboldi, Luca The University of EdinburghUnited Kingdom Formalising Criminal Law in Catala Compiling higher-order specifications to SMT solvers: how to deal with rejection constructively
Victor ArrialArrial, Victor Université Paris Cité - CNRS - IRIFFrance Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework
Kenichi AsaiAsai, Kenichi Ochanomizu UniversityJapan Towards a Reflection for Effect Handlers
David AspinallAspinall, David University of Edinburgh Formalising Criminal Law in Catala
Parsia AtaeiAtaei, Parsia Cornell University P4Cub: A Little Language for Big Routers
Mohamed Faouzi AtigAtig, Mohamed Faouzi Uppsala University, Sweden Committee Member in Program Committee within the VMCAI-track
Robert AtkeyAtkey, Robert University of Strathclyde Compiling higher-order specifications to SMT solvers: how to deal with rejection constructively Semantics II: Session Preview
Clément AubertAubert, Clément Augusta UniversityUnited States Certifying Complexity Analysis Distributing and Parallelizing Non-canonical Loops
Arthur Azevedo de AmorimAzevedo de Amorim, Arthur Boston UniversityUnited States Verified Differential Privacy for Finite Computers SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability Machine
Pedro Henrique Azevedo de AmorimAzevedo de Amorim, Pedro Henrique Cornell University Separated and Shared Effects in Higher-Order Languages Distribution Theoretic Semantics for Non-Smooth Differentiable Programming
B Anne BaanenBaanen, Anne Vrije Universiteit Amsterdam Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
Souheib BaarirBaarir, Souheib CosySEL: Improving SAT Solving Using Local Symmetries
Casper Bach PoulsenBach Poulsen, Casper Delft University of TechnologyNetherlands Session Chair of 3 talks (part of PEPM) Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects Committee Member in Program Committee within the PEPM-track
Chris BaileyBailey, Chris University of Illinois College of Law Research keynote
Chris BaileyBailey, Chris University of IllinoisUnited States Committee Member in Program Committee within the ProLaLa-track
Alan BakerBaker, Alan GoogleCanada Taking Back Control in an Intermediate Representation for GPU Computing
Mantas BakšysBakšys, Mantas University of Cambridge A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL
Marcello BalducciniBalduccini, Marcello Saint Joseph's University, USAUnited States Formalizing and Reasoning about Contracts between Agents
Musard BalliuBalliu, Musard KTH Royal Institute of TechnologySweden Committee Member in Program Committee within the PriSC-track
Stephanie BalzerBalzer, Stephanie Carnegie Mellon UniversityUnited States Session Chair of Semantics & Effects (part of POPL ) Higher-Order Leak and Deadlock Free Locks Committee Member in Program Committee within the POPL -track
Mutsunori BanbaraBanbara, Mutsunori Nagoya UniversityJapan Session Chair of Applications of Answer Set Programming (II) (part of PADL) Solving Vehicle Equipment Specification Problems with Answer Set Programming
Ansuman BanerjeeBanerjee, Ansuman SMT-Based Modeling and Verification of Spiking Neural Networks: A Case Study
Soham BanerjeeBanerjee, Soham SMT-Based Modeling and Verification of Spiking Neural Networks: A Case Study
Sorav BansalBansal, Sorav IIT Delhi and CompilerAI LabsIndia StaticPersist : Compiler Support for PMEM Programming
Mark BarboneBarbone, Mark UCSD Scalable Synthesis of Regular Expressions From Only Positive Examples
Manuel BarbosaBarbosa, Manuel HASLab - INESC TEC and FCUPPortugal Execution Time Program Verification With Tight Bounds
Sébastien BardinBardin, Sébastien CEA LIST, University Paris-SaclayFrance Session Chair of Session 3 (part of PriSC) Committee Member in Program Committee within the PriSC-track
Shraddha BarkeBarke, Shraddha University of California at San DiegoUnited States Student Volunteer Co-Chair in Organizing Committee for POPL 2023
Aurèle BarrièreBarrière, Aurèle University of Rennes; Inria; CNRS; IRISAFrance Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler
Gilles BartheBarthe, Gilles MPI-SP; IMDEA Software InstituteGermany CoqQ: Foundational Verification of Quantum Programs
Adam D. BarwellBarwell, Adam D. Imperial College London, UK Committee Member in Program Committee within the PEPM-track
Shrutarshi BasuBasu, Shrutarshi Harvard UniversityUnited States Session Chair of Session #1 (part of ProLaLa) Session Chair of Session #2 (part of ProLaLa) Session Chair of Session #4 (part of ProLaLa) Session Chair of Session #3 (part of ProLaLa)
Shrutarshi BasuBasu, Shrutarshi Middlebury College Opening comments
Shrutarshi BasuBasu, Shrutarshi Harvard UniversityUnited States Co-chair in Program Committee within the ProLaLa-track
Mako P. BatesBates, Mako P. University of Vermont πMPC: Automatic Security Proofs for MPC Protocols
Kevin BatzBatz, Kevin RWTH Aachen UniversityGermany A Calculus for Amortized Expected Runtimes
Guillaume BaudartBaudart, Guillaume InriaFrance Committee Member in Program Committee within the LAFI-track
Pascal BaumannBaumann, Pascal MPI-SWSGermany Context-Bounded Verification of Context-Free Specifications
Aaron BembenekBembenek, Aaron Harvard UniversityUnited States From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems
Josh BerdineBerdine, Josh MetaUnited Kingdom Committee Member in Program Committee within the POPL -track
Lennart BeringerBeringer, Lennart Princeton UniversityUnited States Committee Member in Steering Committee within the CPP-track
Nicolas BerthierBerthier, Nicolas OCamlProFrance Symbolic Abstract Heaps for Polymorphic Information-flow Guard Inference
Yves BertotBertot, Yves INRIAFrance Session with the Coq Development Team
Alex BestBest, Alex Vrije Universiteit AmsterdamNetherlands Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
Karthikeyan BhargavanBhargavan, Karthikeyan Inria, France Committee Member in Program Committee within the POPL -track
Abhishek BichhawatBichhawat, Abhishek Carnegie Mellon UniversityUnited States Committee Member in Program Committee within the PriSC-track
Annette BieniusaBieniusa, Annette University of Kaiserslautern-LandauGermany Committee Member in Program Committee within the PADL-track
Nicolas BiriBiri, Nicolas Input Output Global (IOG) Committee Member in Program Committee within the PEPM-track
Lars BirkedalBirkedal, Lars Aarhus UniversityDenmark Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice
Aleš BizjakBizjak, Aleš Aarhus UniversityDenmark Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Nikolaj BjørnerBjørner, Nikolaj Microsoft Research Satisfiability Modulo Custom Theories in Z3 (Tool Paper) Z3 Internals – A guide to principles, art and empirics of programming SMT solvers
Jasmin BlanchetteBlanchette, Jasmin Vrije Universiteit AmsterdamNetherlands Committee Member in Steering Committee within the CPP-track
Victor BlanchiBlanchi, Victor ENS Paris Random probability distributions as natural transformations
Roberto BlancoBlanco, Roberto MPI-SPGermany SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability Machine
Sandrine BlazyBlazy, Sandrine University of Rennes; Inria; CNRS; IRISAFrance CompCert: a journey through the landscape of mechanized semantics for verified compilation Mechanised Semantics for Gated Static Single Assignment Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler
Valentin BlotBlot, Valentin LMF, Inria, Université Paris-Saclay Compositional pre-processing for automated reasoning in dependent type theory
Rastislav BodíkBodík, Rastislav Google ResearchUnited States Grisette: Symbolic Compilation as a Functional Programming Library
Ronny BoganiBogani, Ronny University of Edinburgh Formalising Criminal Law in Catala
Filippo BonchiBonchi, Filippo University of PisaItaly Deconstructing the Calculus of Relations with Tape Diagrams
Anthony BordgBordg, Anthony University of Cambridge Encoding Dependently-Typed Constructions into Simple Type Theory
Szabolcs BorgyosBorgyos, Szabolcs GE Research UAV Compliance Checking using Answer Set Programming and Minimal Explanations towards Compliance (Application Paper)
Jay BosamiyaBosamiya, Jay Carnegie Mellon UniversityUnited States MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
Ahmed BouajjaniBouajjani, Ahmed IRIF, Université Paris DiderotFrance Committee Member in Program Committee within the VMCAI-track
Maddy BowersBowers, Maddy Massachusetts Institute of TechnologyUnited States Top-Down Synthesis for Library Learning
William J. BowmanBowman, William J. University of British ColumbiaCanada Workshops Co-Chair in Organizing Committee for POPL 2023 Committee Member in Program Committee within the PriSC-track
John BoylandBoyland, John Univeristy of Wisconsin, MilwaukeeUnited States Using a Proof Assistant to Teach PL Theory, Without the Overhead
Edwin BradyBrady, Edwin University of St Andrews, UKUnited Kingdom Session Chair of 2 online talks (part of PEPM) Wrap up PC Chair in Organizing Committee within the PEPM-track
Joachim BreitnerBreitner, Joachim Epic Games Germany Committee Member in Program Committee within the PADL-track
Linda BrodoBrodo, Linda Università di SassariItaly Session Chair of Verification (part of PADL) Dynamic slicing of Reaction Systems based on assertions and monitors
David BromanBroman, David KTH Royal Institute of TechnologySweden Static Delayed Sampling for Probabilistic Programming Languages Partial Evaluation of Forward-Mode Automatic Differentiation Statically Resolvable Ambiguity
Fraser BrownBrown, Fraser CMU FaJITa: Verifying Optimizations on Just-In-Time Programs Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers
Roberto BruniBruni, Roberto University of PisaItaly Dynamic slicing of Reaction Systems based on assertions and monitors
Matteo BusiBusi, Matteo University Ca' Foscari, VeniceItaly Session Chair of Session 4 (part of PriSC) Automated Learning and Verification of Embedded Security Architectures pi_RA: A pi-calculus for verifying protocols that use remote attestation
William E. ByrdByrd, William E. University of Alabama at Birmingham, USAUnited States Session Chair of Functional (Logic) Programming (part of PADL) Committee Member in Program Committee within the PADL-track
C Pedro CabalarCabalar, Pedro University of CorunnaSpain Committee Member in Program Committee within the PADL-track
Francesco CalimeriCalimeri, Francesco University of Calabria Committee Member in Program Committee within the PADL-track
José Pablo CambroneroCambronero, José Pablo MicrosoftUnited States FlashFill++: Scaling Programming by Example by Cutting to the Chase
Eric CampbellCampbell, Eric Cornell UniversityUnited States Session Chair of Wednesday Morning Break Session Preview (part of POPL Session Previews) Session Chair of Thursday Breakfast Session Preview (part of POPL Session Previews) P4Cub: A Little Language for Big Routers Relational & Automated Verification: Session Preview
Marco CampionCampion, Marco University of VeronaItaly Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Quentin CanuCanu, Quentin Inria and Ecole Polytechnique A Formal Disproof of Hirsch Conjecture
David CaoCao, David University of California at San DiegoUnited States babble: Learning Better Abstractions with E-Graphs and Anti-unification
Qinxiang CaoCao, Qinxiang Shanghai Jiao Tong UniversityChina Interactive Theorem Proving in Logic Education：A Coq Formalization of ZFC Set Theory for Discrete Mathematics Teaching Committee Member in Program Committee within the CoqPL-track
Michael CarbinCarbin, Michael Massachusetts Institute of TechnologyUnited States Panel: Next 50 Years of POPL
Jacques CaretteCarette, Jacques McMaster UniversityCanada Symbolic Execution of Hadamard-Toffoli Quantum Circuits
Ana Carolina SilvaCarolina Silva, Ana FCUPPortugal Execution Time Program Verification With Tight Bounds
Manuel CarroCarro, Manuel IMDEA Software Institute and T.U. of Madrid (UPM)Spain Building Information Modeling Using Constraint Logic Programming (Extended Abstract)
Giuseppe CastagnaCastagna, Giuseppe CNRS; Université de ParisFrance Committee Member in Program Committee within the POPL -track
Elias CastegrenCastegren, Elias Uppsala UniversitySweden Statically Resolvable Ambiguity
Simon CastellanCastellan, Simon University of Rennes; Inria; CNRS; IRISAFrance The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Unfolding
Jonathan CastelloCastello, Jonathan UC Santa Cruz A mechanized model for logical clocks
David Castro-PerezCastro-Perez, David University of KentUnited Kingdom Committee Member in Program Committee within the PEPM-track
Sunjay CauligiCauligi, Sunjay University of California at San Diego, USA Robust Constant-Time Cryptography
Gizem CaylakCaylak, Gizem KTH Royal Institute of Technology Static Delayed Sampling for Probabilistic Programming Languages
Ethan CecchettiCecchetti, Ethan University of Maryland, College ParkUnited States Committee Member in Program Committee within the PriSC-track
Tej ChajedChajed, Tej VMware ResearchUnited States Session Chair of Concurrency & Linearizability (part of POPL ) Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the CPP-track Co-chair in Program Committee within the CoqPL-track
Stefanos ChaliasosChaliasos, Stefanos Imperial College LondonUnited Kingdom Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Bor-Yuh Evan ChangChang, Bor-Yuh Evan University of Colorado Boulder & Amazon Committee Member in Program Committee within the VMCAI-track
Nicolas ChappeChappe, Nicolas University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIPFrance Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
Arthur CharguéraudCharguéraud, Arthur Inria; Université de Strasbourg; CNRS; ICubeFrance A High-Level Separation Logic for Heap Space under Garbage Collection Committee Member in Program Committee within the POPL -track
Kaustuv ChaudhuriChaudhuri, Kaustuv INRIA & LIX, IPP Integrating graphical proofs in Coq
Swarat ChaudhuriChaudhuri, Swarat University of Texas at AustinUnited States Neurosymbolic Programming
Jocelyn (Qiaochu) ChenChen, Jocelyn (Qiaochu) University of Texas at AustinUnited States Committee Member in Artifact Evaluation Committee within the VMCAI-track
John ChenChen, John Cornell UniversityUnited States P4Cub: A Little Language for Big Routers
Mingshuai ChenChen, Mingshuai RWTH AachenGermany Exact Probabilistic Inference Using Generating Functions
Yanju ChenChen, Yanju University of California at Santa BarbaraUnited States Committee Member in Artifact Evaluation Committee within the VMCAI-track
Yixuan ChenChen, Yixuan Yale UniversityUnited States A Compositional Theory of Linearizability
Zilin ChenChen, Zilin UNSWAustralia Dargent: A Silver Bullet for Verified Data Layout Refinement
Lidiia ChernigovskaiaChernigovskaia, Lidiia Solving Constrained Horn Clauses over Algebraic Data Types
Adam ChlipalaChlipala, Adam Massachusetts Institute of TechnologyUnited States Session Chair of Formalized Mathematics I (part of CPP) Pyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilation Fast Cryptographic Code via Partial Evaluation Committee Member in Steering Committee within the CPP-track
Hangyeol ChoCho, Hangyeol Hanyang UniversitySouth Korea Inductive Synthesis of Structurally Recursive Functional Programs from Non-recursive Expressions
Minki ChoCho, Minki Seoul National UniversitySouth Korea Conditional Contextual Refinement
Stephen ChongChong, Stephen Harvard UniversityUnited States Care and Feeding of Advisors From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems Invited Speaker in Speakers within the PLMW @ POPL-track
Jan ChristiansenChristiansen, Jan Flensburg University of Applied Sciences, GermanyGermany Embedding Functional Logic Programming in Haskell via a Compiler Plugin
Berk CirisciCirisci, Berk IRIF, University Paris Diderot and CNRS, FranceFrance A Pragmatic Approach to Stateful Partial Order Reduction
Koen ClaessenClaessen, Koen Chalmers University of TechnologySweden Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the CPP-track
Pierre ClairambaultClairambault, Pierre Université Aix-Marseille; Université de Toulon; CNRS; LISFrance The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Unfolding
Jack ClarkClark, Jack Imperial College LondonUnited Kingdom Taking Back Control in an Intermediate Representation for GPU Computing
Ranald CloustonClouston, Ranald ANUAustralia Committee Member in Program Committee within the CPP-track
Joshua CluneClune, Joshua Carnegie Mellon University A Formalized Reduction of Keller's Conjecture
Cyril CohenCohen, Cyril Inria Semantics of Probabilistic Programs using S-Finite Kernels in Coq
Luisa CollodiCollodi, Luisa University of FlorenceItaly Bayesian parameter estimation with guarantees via interval analysis and simulation
Youyou CongCong, Youyou Tokyo Institute of TechnologyJapan Towards a Reflection for Effect Handlers Committee Member in Selection Committee within the POPL Student Research Competition-track
Nirvana CoppolaCoppola, Nirvana Vrije Universiteit Amsterdam Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
Nathan CorbynCorbyn, Nathan University of OxfordUnited Kingdom Modular Construction of Multi-sorted Free Extensions
Arthur CorrensonCorrenson, Arthur École Normale Supérieure de Rennes & Saarland University What do Relational Properties Have to Say About Legal Expert Systems ?
Stefania CostantiniCostantini, Stefania Dipartimento di Ingegneria e Scienze dell'Informazione eMatematica, Univ. dell'Aquila Committee Member in Program Committee within the PADL-track
Denis CousineauCousineau, Denis Mitsubishi Electric R&D Centre Europe Compositional pre-processing for automated reasoning in dependent type theory
Enzo CranceCrance, Enzo Mitsubishi Electric R&D Centre EuropeFrance Compositional pre-processing for automated reasoning in dependent type theory
D Loris D'AntoniD'Antoni, Loris University of Wisconsin-MadisonUnited States Unrealizability Logic Committee Member in Program Committee within the POPL -track
Deepak D'SouzaD'Souza, Deepak Committee Member in Program Committee within the VMCAI-track
Pedro da Costa Abreu Juniorda Costa Abreu Junior, Pedro Purdue UniversityUnited States A Type-Based Approach to Divide-and-Conquer Recursion in Coq
Chinmaya DabralDabral, Chinmaya North Carolina State University Exploring Consequences of Privacy Policies with Narrative Generation via Answer Set Programming
Matthew L. DaggittDaggitt, Matthew L. Heriott-Watt University Compiling higher-order specifications to SMT solvers: how to deal with rejection constructively
Sander R. DahmenDahmen, Sander R. Vrije Universiteit Amsterdam Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves
Ugo Dal LagoDal Lago, Ugo University of Bologna; InriaItaly Session Chair of Quantum Computing (part of POPL ) Semantics I: Session Preview Committee Member in Program Committee within the POPL -track
Mila Dalla PredaDalla Preda, Mila University of VeronaItaly Committee Member in Program Committee within the POPL -track
Lesly-Ann DanielDaniel, Lesly-Ann CEA ListFrance Committee Member in Program Committee within the PriSC-track
Ornela DardhaDardha, Ornela University of GlasgowUnited Kingdom Committee Member in Program Committee within the POPL -track
Ankush DasDas, Ankush AmazonUnited States Probabilistic Resource-Aware Session Types
Ria DasDas, Ria Stanford UniversityUnited States Combining Functional and Automata Synthesis to Discover Causal Reactive Programs
Swaraj DashDash, Swaraj University of OxfordUnited Kingdom Affine Monads and Lazy Structures for Bayesian Programming
Cristina DavidDavid, Cristina University of BristolUnited Kingdom Committee Member in Program Committee within the PEPM-track
Joel D. DayDay, Joel D. Loughborough UniversityUnited Kingdom On the Expressive Power of String Constraints
Emanuele De AngelisDe Angelis, Emanuele CNR-IASIItaly Multiple Query Satisfiability of Constrained Horn Clauses
Leonardo de Mourade Moura, Leonardo Microsoft ResearchUnited States Committee Member in Program Committee within the CPP-track
Louise Dubois de Prisquede Prisque, Louise Dubois LMF, Inria, Université Paris-Saclay Compositional pre-processing for automated reasoning in dependent type theory
Coen De RooverDe Roover, Coen Vrije Universiteit BrusselBelgium Result Invalidation for Incremental Modular Analyses
Peter DedeckerDedecker, Peter KU LeuvenBelgium Fluo: A Domain-Specific Language for Experiments in Fluorescence Microscopy (Application Paper)
Shaleen DeepDeep, Shaleen MicrosoftUnited States The Fine-Grained Complexity of CFL Reachability
Rémy DegenneDegenne, Rémy Univ. Lille, Inria, CNRS, Centrale Lille, UMR 9198-CRIStAL, F-59000 Lille, France A formalization of Doob's martingale convergence theorems in mathlib
Benjamin DelawareDelaware, Benjamin Purdue UniversityUnited States Diversity, Equity, and Inclusion Chair in Organizing Committee for POPL 2023 Session Chair of Synthesis II (part of POPL ) A Type-Based Approach to Divide-and-Conquer Recursion in Coq Committee Member in Program Committee within the POPL -track
Germán Andrés DelbiancoDelbianco, Germán Andrés Nomadic LabsFrance Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Antoine Delignat-LavaudDelignat-Lavaud, Antoine Microsoft Research, n.n. ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER
Delphine DemangeDemange, Delphine Univ Rennes, Inria, CNRS, IRISAFrance Mechanised Semantics for Gated Static Single Assignment
Aidan DenlingerDenlinger, Aidan University of California at San DiegoUnited States MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
Farzaneh DerakhshanDerakhshan, Farzaneh Carnegie Mellon UniversityUnited States Towards End-to-End Verified TEEs via Verified Interface Conformance and Interface-Preserving Compilers
Remi DesmartinDesmartin, Remi Heriot-Watt University Formalising Criminal Law in Catala
Jo DevriendtDevriendt, Jo CosySEL: Improving SAT Solving Using Local Symmetries
Dominique DevrieseDevriese, Dominique KU LeuvenBelgium pi_RA: A pi-calculus for verifying protocols that use remote attestation Committee Member in Steering Committee within the PriSC-track
Cecilia Di FlorioDi Florio, Cecilia University of BolognaItaly Elements of Quantitative Rewriting
Alessandro Di GiorgioDi Giorgio, Alessandro University of PisaItaly Deconstructing the Calculus of Relations with Tape Diagrams
Cinzia Di GiustoDi Giusto, Cinzia Université Côte d'Azur; CNRSFrance A Partial Order View of Message-Passing Communication Models
Luca Di StefanoDi Stefano, Luca University of Gothenburg, SwedenItaly Compositional Verification of Stigmergic Collective Systems
Robert DickersonDickerson, Robert Purdue UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Rayna DimitrovaDimitrova, Rayna CISPA Helmholtz Center for Information Security Committee Member in Program Committee within the VMCAI-track
Shuo DingDing, Shuo Georgia Institute of TechnologyUnited States Witnessability of Undecidable Problems
Zeyu DingDing, Zeyu Binghamton University, USA Committee Member in Selection Committee within the POPL Student Research Competition-track
Craig DisselkoenDisselkoen, Craig University of California at San DiegoUnited States MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code Committee Member in Program Committee within the PriSC-track
Laurence DiverDiver, Laurence Vrije Universiteit BrusselBelgium Committee Member in Program Committee within the ProLaLa-track
Jenna DiVincenzo (Wise)DiVincenzo (Wise), Jenna Carnegie Mellon UniversityUnited States Committee Member in Program Committee within the PriSC-track
Mihály Dobos-KovácsDobos-Kovács, Mihály Budapest University of Technology and Economics Committee Member in Artifact Evaluation Committee within the VMCAI-track
Ryan DoengesDoenges, Ryan Cornell UniversityUnited States P4Cub: A Little Language for Big Routers
Alastair F. DonaldsonDonaldson, Alastair F. Imperial College London; GoogleUnited Kingdom Taking Back Control in an Intermediate Representation for GPU Computing Committee Member in Program Committee within the POPL -track
Pablo DonatoDonato, Pablo Ecole polytechnique Integrating graphical proofs in Coq
Rui DongDong, Rui University of MichiganUnited States Committee Member in Artifact Evaluation Committee within the VMCAI-track
Dana Drachsler CohenDrachsler Cohen, Dana TechnionIsrael Maximal Robust Neural Network Specifications via Oracle-guided Numerical Optimization
Derek DreyerDreyer, Derek MPI-SWSGermany Panel: Next 50 Years of POPL Conditional Contextual Refinement DimSum: A Decentralized Approach to Multi-language Semantics and Verification
Cezara DrăgoiDrăgoi, Cezara AWS / ENS Committee Member in Program Committee within the VMCAI-track Program Co-Chair in Organizing Committee within the VMCAI-track
Claude DutheilletDutheillet, Claude CosySEL: Improving SAT Solving Using Local Symmetries
Maxime DénèsDénès, Maxime Inria Session with the Coq Development Team
Maxime DénèsDénès, Maxime INRIA Committee Member in Program Committee within the CoqPL-track
Emanuele D’OsualdoD’Osualdo, Emanuele MPI-SWSGermany DimSum: A Decentralized Approach to Multi-language Semantics and Verification The Path to Durable Linearizability
E Chelsea EdmondsEdmonds, Chelsea University of CambridgeUnited Kingdom Session Chair of Wednesday Lunch Session Preview (part of POPL Session Previews) A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL
Thomas EhrhardEhrhard, Thomas CNRS and University Paris Diderot The Variable Elimination Algorithm as a Let-Term Rewriting
Marco EilersEilers, Marco ETH ZurichSwitzerland Committee Member in Program Committee within the PriSC-track
Richard A. EisenbergEisenberg, Richard A. Jane StreetUnited States Career Trajectories in PL Committee Member in Program Committee within the POPL -track Panelist in Panelists within the PLMW @ POPL-track
Clemens EisenhoferEisenhofer, Clemens Satisfiability Modulo Custom Theories in Z3 (Tool Paper)
Kevin EllisEllis, Kevin Cornell UniversityUnited States Top-Down Synthesis for Library Learning
Michael EmmiEmmi, Michael Amazon Web ServicesUnited States Session Chair of Keynote and best paper (part of VMCAI) Session Chair of Keynote and contribution paper (part of VMCAI) Session Chair of Keynote and contribution paper (part of VMCAI) Session Chair of Keynote and contribution paper (part of VMCAI) Committee Member in Program Committee within the VMCAI-track Program Co-Chair in Organizing Committee within the VMCAI-track
Constantin EneaEnea, Constantin Ecole Polytechnique / LIX / CNRSFrance A Pragmatic Approach to Stateful Partial Order Reduction Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the VMCAI-track
Ferhat ErataErata, Ferhat Yale UniversityUnited States Committee Member in Artifact Evaluation Committee within the VMCAI-track
Esra ErdemErdem, Esra Sabanci University, TurkeyTurkey Committee Member in Program Committee within the PADL-track
Oscar ErikssonEriksson, Oscar KTH Royal Institute of Technology Partial Evaluation of Forward-Mode Automatic Differentiation
Guilherme EspadaEspada, Guilherme University of LisbonPortugal Video Chair in Organizing Committee for POPL 2023
F Wolfgang FaberFaber, Wolfgang Alpen-Adria-Universität, Austria Session Chair of Applications of Answer Set Programming (I) (part of PADL)
Wolfgang FaberFaber, Wolfgang University of KlagenfurtAustria Using Hybrid Knowledge Bases for Meta-reasoning over OWL 2 QL
Claudia FaggianFaggian, Claudia Université de Paris & CNRS The Variable Elimination Algorithm as a Let-Term Rewriting
Moreno FalaschiFalaschi, Moreno Dipartimento di Ingegneria dell'Informazione e Scienze Matematiche, University of SienaItaly Dynamic slicing of Reaction Systems based on assertions and monitors
Xiong FanFan, Xiong Rutgers UniversityUnited States A Core Calculus for Equational Proofs of Cryptographic Protocols
Azadeh FarzanFarzan, Azadeh University of TorontoCanada A Pragmatic Approach to Stateful Partial Order Reduction Stratified Commutativity in Verification Algorithms for Concurrent Programs
Grigory FedyukovichFedyukovich, Grigory Florida State UniversityUnited States Session Chair of Neural networks and Abstract Interpretation (part of VMCAI) Solving Constrained Horn Clauses over Algebraic Data Types
Xinyu FengFeng, Xinyu Nanjing UniversityChina Committee Member in Program Committee within the CPP-track
Jerome FeretFeret, Jerome INRIA ParisFrance A generic framework to coarse-grain stochastic reaction networks by Abstract Interpretation Committee Member in Program Committee within the VMCAI-track
Jeremy FergusonFerguson, Jeremy University of California-Berkeley Synthesizing Vectorized Code via Verified Lifting
Kostas FerlesFerles, Kostas Veridise Inc.United States Web Co-Chair in Organizing Committee for POPL 2023
Davide Ferre'Ferre', Davide Université Côte d'Azur; CNRSFrance A Partial Order View of Message-Passing Communication Models
Masood Feyzbakhsh RankoohFeyzbakhsh Rankooh, Masood Tampere UniversityFinland Pruning Redundancy in Answer Set Optimization Applied to Preventive Maintenance Scheduling
Jean-Christophe FilliatreFilliatre, Jean-Christophe CNRSFrance Committee Member in Program Committee within the VMCAI-track
Robert Bruce FindlerFindler, Robert Bruce Northwestern UniversityUnited States Modern Macros Associate Chair in Program Committee within the POPL -track
Bernd FinkbeinerFinkbeiner, Bernd CISPA Helmholtz Center for Information SecurityGermany Committee Member in Program Committee within the VMCAI-track
Fabio FioravantiFioravanti, Fabio University of Chieti-PescaraItaly Multiple Query Satisfiability of Constrained Horn Clauses
Denis FirsovFirsov, Denis Tallinn University of TechnologyEstonia Committee Member in Program Committee within the CPP-track
Christopher W. FletcherFletcher, Christopher W. University of Illinois Urbana-Champaign Towards Formally Verified Path ORAM in Coq
Mario FloridoFlorido, Mario Universidade do PortoPortugal Execution Time Program Verification With Tight Bounds
Dylan FlynnFlynn, Dylan Formalizing and Reasoning about Contracts between Agents
Riccardo FocardiFocardi, Riccardo University Ca' Foscari, Venice Automated Learning and Verification of Embedded Security Architectures
Yannick ForsterForster, Yannick InriaFrance A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl) Committee Member in Program Committee within the CPP-track
Nate FosterFoster, Nate Cornell UniversityUnited States Session Preview Chair in Organizing Committee for POPL 2023 Session Chair of Wednesday Breakfast Session Preview (part of POPL Session Previews) Session Chair of Thursday Morning Break Session Preview (part of POPL Session Previews) P4Cub: A Little Language for Big Routers Synthesis II: Session Preview Panel: Next 50 Years of POPL
Cédric FournetFournet, Cédric Microsoft Research ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER
Cameron FreerFreer, Cameron Massachusetts Institute of TechnologyUnited States Steering Committee Member in Steering Committee within the LAFI-track
Aymeric FromherzFromherz, Aymeric InriaFrance FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Roy FrostigFrostig, Roy Google ResearchUnited States You Only Linearize Once: Tangents Transpose to Gradients
Peng FuFu, Peng Dalhousie UniversityCanada Proto-Quipper with Dynamic Lifting
Michael FärberFärber, Michael Universität Innsbruck, AustriaAustria Terms for Efficient Proof Checking and Parsing
Hugo FéréeFérée, Hugo Université Paris Cité / IRIFUnited Kingdom Formalizing and computing propositional quantifiers
G Marco GaboardiGaboardi, Marco Boston UniversityUnited States Verified Differential Privacy for Finite Computers
Letterio GallettaGalletta, Letterio IMT School for Advanced Studies LuccaItaly Committee Member in Program Committee within the PriSC-track
Moses GanardiGanardi, Moses MPI-SWSGermany Context-Bounded Verification of Context-Free Specifications
Joshua GancherGancher, Joshua Carnegie Mellon UniversityUnited States Universally Composable Security for Program Partitioning A Core Calculus for Equational Proofs of Cryptographic Protocols
Vijay GaneshGanesh, Vijay Georgia TechUnited States On the Expressive Power of String Constraints
Philippa GardnerGardner, Philippa Imperial College LondonUnited Kingdom Program Logics & Resources: Session Preview
Deepak GargGarg, Deepak MPI-SWSGermany DimSum: A Decentralized Approach to Multi-language Semantics and Verification Associate Chair in Program Committee within the POPL -track Committee Member in Steering Committee within the PriSC-track
Poorva GargGarg, Poorva University of California, Los Angeles Bit-Blasting Probabilistic Programs
Francesco GavazzoGavazzo, Francesco University of PisaItaly Elements of Quantitative Rewriting
Martin GebserGebser, Martin University of Klagenfurt, AustriaAustria Flexible Job-shop Scheduling for Semiconductor Manufacturing with Hybrid Answer Set Programming (Application Paper) Committee Member in Program Committee within the PADL-track
Aina Linn GeorgesGeorges, Aina Linn Aarhus UniversityDenmark SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability Machine Committee Member in Program Committee within the PriSC-track
Sumana GhoshGhosh, Sumana SMT-Based Modeling and Verification of Spiking Neural Networks: A Case Study
Matthías Páll GissurarsonGissurarson, Matthías Páll Chalmers University of Technology, SwedenSweden Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Milos GligoricGligoric, Milos University of Texas at AustinUnited States Committee Member in Program Committee within the CPP-track
Robert GlückGlück, Robert University of CopenhagenDenmark Towards Type Debugging using Partial Evaluation Committee Member in Program Committee within the PADL-track
Amir Kafshdar GoharshadyGoharshady, Amir Kafshdar IST Austria, Austria Efficient Interprocedural Data-Flow Analysis using Treedepth and Treewidth
Anitha GollamudiGollamudi, Anitha University of Massachusetts LowellUnited States Career Trajectories in PL MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code Panelist in Panelists within the PLMW @ POPL-track Committee Member in Program Committee within the PriSC-track
Hannah GommerstadtGommerstadt, Hannah Vassar College Session Chair of Session 1 (part of PLMW @ POPL) Committee Member in Organizing Committee within the PLMW @ POPL-track
Sergey GoncharovGoncharov, Sergey University of Erlangen-NurembergGermany Towards a Higher-Order Mathematical Operational Semantics
Georges GonthierGonthier, Georges InriaFrance Committee Member in Steering Committee within the CPP-track
Guido GovernatoriGovernatori, Guido Singapore Management University Defeasible Semantics for L4
Stephane Graham-LengrandGraham-Lengrand, Stephane SRIUnited States Committee Member in Program Committee within the CPP-track
Gabe GrandGrand, Gabe Session Chair of Thursday Lunch Session Preview (part of POPL Session Previews)
Gabriel GrandGrand, Gabriel Massachusetts Institute of TechnologyUnited States Top-Down Synthesis for Library Learning
Michael GreenbergGreenberg, Michael Stevens Institute of TechnologyUnited States Session Chair of Automated Verification (part of POPL ) Session Chair of Session 2 (part of PLMW @ POPL) Career Trajectories in PL From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems Automated Verification: Session Preview Committee Member in Program Committee within the POPL -track Committee Member in Organizing Committee within the PLMW @ POPL-track
Benjamin GregoireGregoire, Benjamin INRIA Practical and sound equality tests, automatically
Nathan GrewalGrewal, Nathan University of WaterlooCanada On the Expressive Power of String Constraints
Edward GrifforGriffor, Edward Formalizing and Reasoning about Contracts between Agents
James GrimmelmannGrimmelmann, James Cornell University The Structure and Legal Interpretation of Computer Programs Committee Member in Program Committee within the ProLaLa-track
Samuel GruetterGruetter, Samuel Massachusetts Institute of Technology Omnisemantics: Smooth Handling of Nondeterminism (Invited talk)
Yu GuGu, Yu University of TsukubaJapan Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification Optimal CHC Solving via Termination Proofs
Marco GuarnieriGuarnieri, Marco IMDEA Software InstituteSpain Session Chair of Session 1 (part of PriSC) Co-chair in Program Committee within the PriSC-track Committee Member in Steering Committee within the PriSC-track
Giulio GuerrieriGuerrieri, Giulio Aix Marseille Université - CNRS - LIS; Edinburgh Research Centre - Central Software Institute - HuaweiFrance Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework
Arjun GuhaGuha, Arjun Northeastern University and Roblox ResearchUnited States Formal Methods in Compilation & Implementation: Session Preview
Sumit GulwaniGulwani, Sumit MicrosoftUnited States FlashFill++: Scaling Programming by Example by Cutting to the Chase
Elsa GunterGunter, Elsa University of IllinoisUnited States Committee Member in Program Committee within the CPP-track
Gopal GuptaGupta, Gopal University of Texas at Dallas, USAUnited States Building Information Modeling Using Constraint Logic Programming (Extended Abstract) Jury-trial Story Construction and Analysis using Goal-directed Answer Set Programming Committee Member in Program Committee within the PADL-track
Denis GurchenkovGurchenkov, Denis MathWorksUnited States MATLAB Coder: Partial Evaluation in Practice
Arie GurfinkelGurfinkel, Arie University of WaterlooCanada Committee Member in Program Committee within the VMCAI-track
H Andrew HabibHabib, Andrew SnT, University of LuxembourgLuxembourg Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Liana HadareanHadarean, Liana Amazon Web ServicesUnited States Committee Member in Program Committee within the VMCAI-track
Emmanuel HainryHainry, Emmanuel Université de Lorraine; CNRS; Inria; LORIAFrance A General Noninterference Policy for Polynomial Time
Ákos HajduHajdu, Ákos MetaUnited Kingdom Committee Member in Program Committee within the VMCAI-track
Asta Halkjær FromHalkjær From, Asta Technical University of Denmark Aesop: White-Box Best-First Proof Search for Lean
Philipp HallerHaller, Philipp KTH Royal Institute of TechnologySweden Statically Resolvable Ambiguity
Michael HanusHanus, Michael Kiel UniversityGermany Session Chair of Invited Talk (part of PADL) Co-chair in Program Committee within the PADL-track Co-chair in Programme Chairs within the PADL-track
Ben HardekopfHardekopf, Ben University of California at Santa BarbaraUnited States Citrus: A Dependently Typed Framework for Pulse-Based Logic
Robert HarperHarper, Robert Carnegie Mellon UniversityUnited States Session Chair of Resource Analysis (part of POPL )
Ichiro HasuoHasuo, Ichiro National Institute of Informatics, JapanJapan Committee Member in Program Committee within the POPL -track
Chris HawblitzelHawblitzel, Chris Microsoft ResearchUnited States Committee Member in Program Committee within the CPP-track Committee Member in Program Committee within the PriSC-track
Ian J. HayesHayes, Ian J. The University of QueenslandAustralia Verifying term graph optimizations using Isabelle/HOL
Paul HeHe, Paul University of PennsylvaniaUnited States Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
Shaobo HeHe, Shaobo Amazon Web ServicesUnited States Committee Member in Program Committee within the VMCAI-track
Bastiaan HeerenHeeren, Bastiaan Open University of the Netherlands, NetherlandsNetherlands Program Synthesis Using Example Propagation
Ludovic HenrioHenrio, Ludovic University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIPFrance Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
Hugo HerbelinHerbelin, Hugo Inria Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the CoqPL-track
Yann HerklotzHerklotz, Yann Imperial College LondonUnited Kingdom Mechanised Semantics for Gated Static Single Assignment
Scott HermanHerman, Scott Conan & Herman Formalising Criminal Law in Catala
Michael HicksHicks, Michael University of Maryland; AmazonUnited States Qunity: A Unified Language for Quantum and Classical Computing Committee Member in Steering Committee within the PriSC-track
Hans-Dieter HiepHiep, Hans-Dieter Leiden Institute of Advanced Compter Science (LIACS) & Centrum Wiskunde Informatica (CWI)Netherlands Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Kesha HietalaHietala, Kesha University of MarylandUnited States FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Thomas T. HildebrandtHildebrandt, Thomas T. University of CopenhagenDenmark Session Chair of Session #2 (part of ProLaLa) DCR Graphs as Co-created Executable Models of the Law
Andrew K. HirschHirsch, Andrew K. University at Buffalo, SUNYUnited States Semantics & Effects: Session Preview Committee Member in Selection Committee within the POPL Student Research Competition-track
Jan HoffmannHoffmann, Jan Carnegie Mellon UniversityUnited States Probabilistic Resource-Aware Session Types
Steven HoltzenHoltzen, Steven Northeastern UniversityUnited States Session Chair of Probabilistic Inference (part of POPL ) Session Chair of Poster Session (part of LAFI) Session Chair of Second Session (part of LAFI) Session Chair of Third Session (part of LAFI) Session Chair of First Session (part of LAFI) Bit-Blasting Probabilistic Programs Opening Comments New foundations for probabilistic separation logic Co-chair in Organizing Committee within the LAFI-track Co-chair in Program Committee within the LAFI-track
Jaemin HongHong, Jaemin KAISTSouth Korea Semantic Transformation Framework for Rewriting Rules
Kuen-Bang Hou (Favonia)Hou (Favonia), Kuen-Bang University of MinnesotaUnited States Session Chair of Session 3 (part of PLMW @ POPL) An Order-Theoretic Analysis of Universe Polymorphism Committee Member in Organizing Committee within the PLMW @ POPL-track
Petra HozzováHozzová, Petra TU Wien Towards Synthesis in Superposition
Cătălin HriţcuHriţcu, Cătălin MPI-SPGermany Session Chair of Session 2 (part of PriSC) Securely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typed Interfaces SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability Machine Steering Committee Chair in Steering Committee within the CPP-track Steering Committee Chair in Steering Committee within the PriSC-track
Justin HsuHsu, Justin Cornell UniversityUnited States Separated and Shared Effects in Higher-Order Languages
Jason Z.S. HuHu, Jason Z.S. McGill UniversityCanada Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Zhenjiang HuHu, Zhenjiang Peking UniversityChina Committee Member in Program Committee within the POPL -track
Xuejing HuangHuang, Xuejing University of Hong KongChina Session Chair of Wednesday Evening Session Preview (part of POPL Session Previews) Making a Type Difference: Subtraction on Intersection Types as Generalized Record Operations A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈
Zunchen HuangHuang, Zunchen Committee Member in Artifact Evaluation Committee within the VMCAI-track
Alex HubersHubers, Alex University of IowaUnited States A Type-Based Approach to Divide-and-Conquer Recursion in Coq
Sebastian HuntHunt, Sebastian City University of LondonUnited Kingdom Reconciling Shannon and Scott with a Lattice of Computable Information
Mathieu HuotHuot, Mathieu University of OxfordUnited Kingdom What do posterior distributions of probabilistic programs look like? ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs
Chung-Kil HurHur, Chung-Kil Seoul National UniversitySouth Korea Concurrency & Linearizability: Session Preview Conditional Contextual Refinement Committee Member in Selection Committee within the POPL Student Research Competition-track
I Giovambattista IanniIanni, Giovambattista University of Calabria, ItalyItaly Integrating ASP-based incremental reasoning in the videogame development workflow (Application Paper)
Atsushi IgarashiIgarashi, Atsushi Kyoto UniversityJapan Committee Member in Program Committee within the PEPM-track
Daniela InclezanInclezan, Daniela Miami UniversityUnited States Session Chair of Opening & Invited Talk (part of PADL) Co-chair in Program Committee within the PADL-track Co-chair in Programme Chairs within the PADL-track
Apoorv IngleIngle, Apoorv University of IowaUnited States Virtualization Chair in Organizing Committee for POPL 2023
Katsumi InoueInoue, Katsumi NIIJapan Linear Algebraic Abduction with Partial Evaluation
Natalie IsakIsak, Natalie Microsoft P4Cub: A Little Language for Big Routers
J Vincent JacksonJackson, Vincent University of MelbourneAustralia Dargent: A Silver Bullet for Verified Data Layout Refinement
Jules JacobsJacobs, Jules Radboud University NijmegenNetherlands Fast Coalgebraic Bisimilarity Minimization Higher-Order Leak and Deadlock Free Locks
Suresh JagannathanJagannathan, Suresh Purdue UniversityUnited States Committee Member in Program Committee within the POPL -track
Felix JahnJahn, Felix Saarland University A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)
Dustin JamnerJamner, Dustin MIT CSAIL Pyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilation
Junyoung JangJang, Junyoung McGill UniversityCanada Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Tomi JanhunenJanhunen, Tomi Tampere UniversityFinland Pruning Redundancy in Answer Set Optimization Applied to Preventive Maintenance Scheduling Committee Member in Program Committee within the PADL-track
Alan JeffreyJeffrey, Alan RobloxUnited States Session Chair of Types II (part of POPL ) Committee Member in Program Committee within the POPL -track
Christa JenkinsJenkins, Christa University of IowaUnited States A Type-Based Approach to Divide-and-Conquer Recursion in Coq
Johan JeuringJeuring, Johan Utrecht University Program Synthesis Using Example Propagation
Ranjit JhalaJhala, Ranjit University of California at San DiegoUnited States Robust Constant-Time Cryptography
Limin JiaJia, Limin Carnegie Mellon University Towards End-to-End Verified TEEs via Verified Interface Conformance and Interface-Preserving Compilers Security: Session Preview
Chuan JiangJiang, Chuan Purdue UniversityUnited States Comparative Synthesis: Learning Near-Optimal Network Designs by Query
Yuchen JiangJiang, Yuchen University of Michigan Zydeco: A Stack-Based Call-By-Push-Value Language
Jerome JochemsJochems, Jerome University of BristolUnited Kingdom Higher-Order MSL Horn Constraints
Patricia JohannJohann, Patricia Appalachian State University Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the PADL-track
Evan JohnsonJohnson, Evan University of California at San Diego; ArmUnited States FaJITa: Verifying Optimizations on Just-In-Time Programs MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
Matthew J. JohnsonJohnson, Matthew J. Google ResearchUnited States You Only Linearize Once: Tangents Transpose to Gradients
Eddie JonesJones, Eddie University of BristolUnited Kingdom Higher-Order MSL Horn Constraints
Jacques-Henri JourdanJourdan, Jacques-Henri CNR, LMFFrance Committee Member in Program Committee within the POPL -track
Dejan JovanovićJovanović, Dejan SRI InternationalUnited States Committee Member in Program Committee within the VMCAI-track
Ralf JungJung, Ralf ETH ZürichSwitzerland Session Chair of Verified Compilation (part of POPL ) Committee Member in Program Committee within the POPL -track
K Anan KabahaKabaha, Anan Technion, Israel Institute of TechnologyIsrael Maximal Robust Neural Network Specifications via Oracle-guided Numerical Optimization
Younesse KaddarKaddar, Younesse University of OxfordUnited Kingdom Affine Monads and Lazy Structures for Bayesian Programming
Cezary KaliszykKaliszyk, Cezary University of Innsbruck Improved Assistance for Interactive Proof
Pankaj Kumar KalitaKalita, Pankaj Kumar IIT KanpurIndia Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Konstantinos KallasKallas, Konstantinos University of PennsylvaniaUnited States Student Volunteer Co-Chair in Organizing Committee for POPL 2023 Executing Microservice Applications on Serverless, Correctly
Yukiyoshi KameyamaKameyama, Yukiyoshi University of TsukubaJapan Generating Programs for Polynomial Multiplication with Correctness Assurance Committee Member in Program Committee within the PADL-track Committee Member in Program Committee within the PEPM-track
Benjamin Lucien KaminskiKaminski, Benjamin Lucien Saarland University; University College LondonGermany Deductive Verification of Probabilistic Programs A Calculus for Amortized Expected Runtimes
Ohad KammarKammar, Ohad University of EdinburghUnited Kingdom Modular Construction of Multi-sorted Free Extensions Towards type-driven data-science in Idris Committee Member in Program Committee within the POPL -track Steering Committee Member in Steering Committee within the LAFI-track
Gabriel KammerKammer, Gabriel MIT Pyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilation
Jeehoon KangKang, Jeehoon KAISTSouth Korea Student Research Competition Co-Chair in Organizing Committee for POPL 2023 Session Chair of SRC Poster (part of POPL Student Research Competition) Co-chair in Selection Committee within the POPL Student Research Competition-track
Joost-Pieter KatoenKatoen, Joost-Pieter RWTH Aachen UniversityGermany Session Chair of Logic & Decidability II (part of POPL ) Exact Probabilistic Inference Using Generating Functions Deductive Verification of Probabilistic Programs A Calculus for Amortized Expected Runtimes Committee Member in Program Committee within the POPL -track
Ryan KavanaghKavanagh, Ryan McGill UniversityCanada Career Trajectories in PL Panelist in Panelists within the PLMW @ POPL-track Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Chantal KellerKeller, Chantal LRI, Université Paris-SudFrance Compositional pre-processing for automated reasoning in dependent type theory
Chantal KellerKeller, Chantal Université Paris SaclayFrance Committee Member in Program Committee within the CPP-track
Gabriele KellerKeller, Gabriele Utrecht UniversityNetherlands Dargent: A Silver Bullet for Verified Data Layout Refinement
Axel KerinecKerinec, Axel Université Sorbonne Paris Nord; LIPN; CNRSFrance Why Are Proofs Relevant in Proof-Relevant Models?
Marie KerjeanKerjean, Marie CNRS, Université Sorbonne Paris NordFrance ∂ is for Dialectica: typing differentiable programming Committee Member in Program Committee within the CPP-track
Delia KesnerKesner, Delia Université Paris Cité - CNRS - IRIF; Institut Universitaire de FranceFrance Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework
Ameya KetkarKetkar, Ameya UberUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Narges KhakpourKhakpour, Narges Linnaeus University Symbolic Abstract Heaps for Polymorphic Information-flow Guard Inference
Alan KhojaKhoja, Alan University of Konstanz Formal Modeling and Analysis of Legal Contracts using ContractCheck
Siau-Cheng KhooKhoo, Siau-Cheng National University of SingaporeSingapore ARENA: Enhancing Abstract Refinement for Neural Network Verification
Jinwoo KimKim, Jinwoo University of Wisconsin-Madison; Seoul National UniversityUnited States Unrealizability Logic
Yoonseung KimKim, Yoonseung Yale UniversityUnited States Session Chair of Applications (part of CPP) Committee Member in Program Committee within the CPP-track Committee Member in Selection Committee within the POPL Student Research Competition-track
Zachary KincaidKincaid, Zachary Princeton UniversityUnited States Session Chair of Logic & Decidability I (part of POPL ) When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic Logic & Decidability I: Session Preview
Kohei KishidaKishida, Kohei University of Illinois at Urbana-ChampaignUnited States Proto-Quipper with Dynamic Lifting
Gerwin KleinKlein, Gerwin Proofcraft and UNSW SydneyAustralia Committee Member in Steering Committee within the CPP-track
Vasileios KlimisKlimis, Vasileios Imperial College LondonUnited Kingdom Taking Back Control in an Intermediate Representation for GPU Computing
Lutz KlinkenbergKlinkenberg, Lutz RWTH Aachen University Exact Probabilistic Inference Using Generating Functions
Dominik KlumppKlumpp, Dominik University of FreiburgGermany Stratified Commutativity in Verification Algorithms for Concurrent Programs
Naoki KobayashiKobayashi, Naoki University of TokyoJapan HFL(Z) Validity Checking for Automated Program Verification
Nicolas KohKoh, Nicolas Princeton UniversityUnited States When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic
Christina KohlKohl, Christina University of Innsbruck A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems
Misaki KojimaKojima, Misaki Nagoya UniversityJapan From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriting
Wen KokkeKokke, Wen University of Strathclyde Compiling higher-order specifications to SMT solvers: how to deal with rejection constructively
Michalis KokologiannakisKokologiannakis, Michalis MPI-SWSGermany Kater: Automating Weak Memory Model Metatheory and Consistency Checking
Matthew KolosickKolosick, Matthew University of California at San DiegoUnited States Robust Constant-Time Cryptography
Ekaterina KomandantskayaKomandantskaya, Ekaterina Heriot-Watt University, UKUnited Kingdom Compiling higher-order specifications to SMT solvers: how to deal with rejection constructively Committee Member in Program Committee within the ProLaLa-track
Ekaterina KomendantskayaKomendantskaya, Ekaterina Heriot-Watt University, UK Formalising Criminal Law in Catala Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the PADL-track
Joomy KorkutKorkut, Joomy Princeton University, USAUnited States Committee Member in Artifact Evaluation Committee within the VMCAI-track
Katherine KosaianKosaian, Katherine Carnegie Mellon University A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
Eric KoskinenKoskinen, Eric Stevens Institute of TechnologyUnited States Session Chair of Model Checking (part of VMCAI) Verifying, Inferring and Exploiting Code Commutativity An Algebra of Alignment for Relational Verification Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification
Paraschos KoutrisKoutris, Paraschos University of Wisconsin-MadisonUnited States The Fine-Grained Complexity of CFL Reachability
Angeliki Koutsoukou-ArgyrakiKoutsoukou-Argyraki, Angeliki University of Cambridge, Department of Computer Science and TechnologyUnited Kingdom A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL
Laura KovacsKovacs, Laura Vienna University of Technology (TU Wien)Austria Committee Member in Program Committee within the POPL -track
Laura KovácsKovács, Laura TU WienAustria Satisfiability Modulo Custom Theories in Z3 (Tool Paper)
Faustyna KrawiecKrawiec, Faustyna University of CambridgeUnited Kingdom Committee Member in Program Committee within the LAFI-track
Robbert KrebbersKrebbers, Robbert Radboud University NijmegenNetherlands Session Chair of Program Logics & Resources (part of POPL ) Session Chair of Logical Foundations (part of CPP) Session Chair of Session 4 (part of PLMW @ POPL) DimSum: A Decentralized Approach to Multi-language Semantics and Verification Committee Member in Program Committee within the POPL -track Conference Chair in Organizing Committee within the CPP-track Committee Member in Steering Committee within the CPP-track Committee Member in Organizing Committee within the PLMW @ POPL-track
Harlan KringenKringen, Harlan UC Santa Barbara Citrus: A Dependently Typed Framework for Pulse-Based Logic
Neel KrishnaswamiKrishnaswami, Neel University of CambridgeUnited Kingdom Session Chair of Semantics I (part of POPL ) Session Chair of Types I (part of POPL ) Types I: Session Preview CN: Verifying Systems C Code with Separation-Logic Refinement Types
Matthis KruseKruse, Matthis CISPA Helmholtz Center for Information SecurityGermany Blame-Preserving Secure Compilation
Burcu Kulahcioglu OzkanKulahcioglu Ozkan, Burcu Delft University of TechnologyNetherlands Committee Member in Program Committee within the VMCAI-track
Rose KunkelKunkel, Rose University of California at San DiegoUnited States babble: Learning Better Abstractions with E-Graphs and Anti-unification
Lindsey KuperKuper, Lindsey University of California at Santa Cruz Session Chair of Formal Methods in Compilation & Implementation (part of POPL ) Committee Member in Program Committee within the POPL -track
Martin KölblKölbl, Martin CertiK Formal Modeling and Analysis of Legal Contracts using ContractCheck
L Ambroise LafontLafont, Ambroise University of CambridgeUnited Kingdom Dargent: A Silver Bullet for Verified Data Layout Refinement
Ori LahavLahav, Ori Tel Aviv UniversityIsrael An Operational Approach to Library Abstraction under Relaxed Memory Concurrency Kater: Automating Weak Memory Model Metatheory and Consistency Checking
Akash LalLal, Akash Microsoft Research Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the VMCAI-track
Christopher LamLam, Christopher University of Illinois at Urbana-Champaign Distribution Theoretic Semantics for Non-Smooth Differentiable Programming
Thomas LamiauxLamiaux, Thomas University of Paris-Saclay, Ens Paris-Saclay Computing Cohomology Rings in Cubical Agda
Leonidas LampropoulosLampropoulos, Leonidas University of Maryland, College ParkGreece Artifact Evaluation Co-Chair in Organizing Committee for POPL 2023 How (not) to give a great research talk QuickChick: Combining Random Testing and Verification in Coq Invited Speaker in Speakers within the PLMW @ POPL-track Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Emiel LanckrietLanckriet, Emiel KU Leuven Short Talk: Generalising secure compilation criteria pi_RA: A pi-calculus for verifying protocols that use remote attestation
Cosimo LaneveLaneve, Cosimo University of Bologna Legal Contracts Amending in Stipula
Frederic LangLang, Frederic Compositional Verification of Stigmergic Collective Systems
Laetitia LaversaLaversa, Laetitia Université Côte d'Azur; CNRSFrance A Partial Order View of Message-Passing Communication Models
Sarah LawskyLawsky, Sarah Northwestern UniversityUnited States Committee Member in Program Committee within the ProLaLa-track
Quang Loc LeLe, Quang Loc University College LondonUnited Kingdom Incorrectness Logic and Under-approximation: Foundations of Bug Catching
Ton Chanh LeLe, Ton Chanh Stevens Institute of TechnologyUnited States An Algebra of Alignment for Relational Verification
Vu LeLe, Vu MicrosoftUnited States FlashFill++: Scaling Programming by Example by Cutting to the Chase
Dongjae LeeLee, Dongjae Seoul National UniversitySouth Korea Conditional Contextual Refinement
Wonyeol LeeLee, Wonyeol Stanford UniversityUnited States Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference
Woosuk LeeLee, Woosuk Hanyang UniversitySouth Korea Inductive Synthesis of Structurally Recursive Functional Programs from Non-recursive Expressions
Daan LeijenLeijen, Daan Microsoft ResearchUnited States Tail Recursion Modulo Context: An Equational Approach
Matthieu LemerreLemerre, Matthieu Université Paris-Saclay - CEA LISTFrance SSA Translation Is an Abstract Interpretation
Sorin LernerLerner, Sorin University of California at San DiegoUnited States FaJITa: Verifying Optimizations on Just-In-Time Programs Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers
Xavier LeroyLeroy, Xavier Collège de FranceFrance Panel: Next 50 Years of POPL Committee Member in Program Committee within the POPL -track
Mohsen LesaniLesani, Mohsen University of California at Riverside Committee Member in Program Committee within the POPL -track
Stefan LeueLeue, Stefan University of KonstanzGermany Formal Modeling and Analysis of Legal Contracts using ContractCheck
Hannah LeungLeung, Hannah University of Illinois Urbana-ChampaignUnited States Towards Formally Verified Path ORAM in Coq
Alexander K. LewLew, Alexander K. Massachusetts Institute of TechnologyUnited States Semantics of Probabilistic Program Traces What do posterior distributions of probabilistic programs look like? ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs Committee Member in Program Committee within the LAFI-track
Jianlin LiLi, Jianlin University of WaterlooCanada Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortized Probabilistic Inference
John LiLi, John Northeastern University New foundations for probabilistic separation logic
Liyi LiLi, Liyi University of MarylandUnited States Qunity: A Unified Language for Quantum and Classical Computing
Yannan LiLi, Yannan Committee Member in Artifact Evaluation Committee within the VMCAI-track
Yuanbo LiLi, Yuanbo Georgia Institute of TechnologyUnited States Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear Programming
Yue LiLi, Yue Heriot-Watt University, UKUnited Kingdom Formalising Criminal Law in Catala
Zixuan LiLi, Zixuan Purdue UniversityUnited States Comparative Synthesis: Learning Near-Optimal Network Designs by Query
Hongjin LiangLiang, Hongjin Nanjing UniversityChina Committee Member in Program Committee within the PriSC-track
Tomer LibalLibal, Tomer Designing an experiment for comparing user interfaces for legal formalization
Steven LibbyLibby, Steven University of PortlandUnited States Session Chair of Debugging (part of PADL) RICE: An Optimizing Curry Compiler
Daniel R. LicataLicata, Daniel R. Wesleyan UniversityUnited States Committee Member in Program Committee within the POPL -track
Nathan LiittschwagerLiittschwager, Nathan University of California, Santa Cruz A Formalization of Observational Equivalence in Message Passing Protocols
Jannis LimpergLimperg, Jannis Vrije Universiteit AmsterdamNetherlands Aesop: White-Box Best-First Proof Search for Lean
Anthony Widjaja LinLin, Anthony Widjaja TU Kaiserslautern; MPI-SWSGermany Committee Member in Program Committee within the VMCAI-track
Sam LindleyLindley, Sam University of EdinburghUnited Kingdom Modular Construction of Multi-sorted Free Extensions
Junyi LiuLiu, Junyi Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of SciencesChina CoqQ: Foundational Verification of Quantum Programs
Vincent LiuLiu, Vincent University of PennsylvaniaUnited States Executing Microservice Applications on Serverless, Correctly
Axel LjungströmLjungström, Axel Stockholm University Computing Cohomology Rings in Cubical Agda
Devon LoehrLoehr, Devon Princeton UniversityUnited States SwitchLog: A Logic Programming Language for Network Switches
Anton LorenzenLorenzen, Anton University of EdinburghUnited Kingdom Tail Recursion Modulo Context: An Equational Approach
Etienne LozesLozes, Etienne Université Côte d'Azur; CNRSFrance A Partial Order View of Message-Passing Communication Models
Sirui LuLu, Sirui University of WashingtonUnited States Grisette: Symbolic Compilation as a Functional Programming Library
Flaminia L. LuccioLuccio, Flaminia L. University Ca' Foscari, Venice Automated Learning and Verification of Embedded Security Architectures
Daniel LundénLundén, Daniel KTH Royal Institute of TechnologySweden Static Delayed Sampling for Probabilistic Programming Languages
Sterre LutzLutz, Sterre Utrecht University and TNO Deontic Paradoxes in Library Lending Regulations: A Case Study in Flint
Jean-Christophe LéchenetLéchenet, Jean-Christophe Université Côte d’Azur, Inria Practical and sound equality tests, automatically
M Mohammed M. S. El-KholanyM. S. El-Kholany, Mohammed University of KlagenfurtAustria Flexible Job-shop Scheduling for Semiconductor Manufacturing with Hybrid Answer Set Programming (Application Paper)
José Nuno MacedoMacedo, José Nuno University of MinhoPortugal Efficient Embedding of Strategic Attribute Grammars via Memoization
Dougal MaclaurinMaclaurin, Dougal Google ResearchUnited States You Only Linearize Once: Tangents Transpose to Gradients
Matteo MaffeiMaffei, Matteo TU Wien Committee Member in Program Committee within the POPL -track
Assia MahboubiMahboubi, Assia INRIAFrance Compositional pre-processing for automated reasoning in dependent type theory
Kenji MaillardMaillard, Kenji Inria NantesFrance Committee Member in Program Committee within the CPP-track
Geoffrey MainlandMainland, Geoffrey Drexel UniversityUnited States Committee Member in Program Committee within the PEPM-track
Haya Majid QureshiMajid Qureshi, Haya Alpen-Adria-Universität KlagenfurtAustria Using Hybrid Knowledge Bases for Meta-reasoning over OWL 2 QL
Rupak MajumdarMajumdar, Rupak MPI-SWSGermany Context-Bounded Verification of Context-Free Specifications
Dhruv C. MakwanaMakwana, Dhruv C. University of CambridgeUnited Kingdom CN: Verifying Systems C Code with Separation-Logic Refinement Types
Florin ManeaManea, Florin University of GöttingenGermany On the Expressive Power of String Constraints
Ravi MangalMangal, Ravi Carnegie Mellon UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Vikash MansinghkaMansinghka, Vikash Massachusetts Institute of Technology Semantics of Probabilistic Program Traces
Vikash K. MansinghkaMansinghka, Vikash K. Massachusetts Institute of TechnologyUnited States What do posterior distributions of probabilistic programs look like? ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs
Giulio ManzonettoManzonetto, Giulio Université Sorbonne Paris Nord; LIPN; CNRSFrance Why Are Proofs Relevant in Proof-Relevant Models?
Katarzyna MarekMarek, Katarzyna University of Edinburgh Towards type-driven data-science in Idris
Danielle MarshallMarshall, Danielle University of Kent, UKUnited Kingdom Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Chris MartensMartens, Chris Northeastern UniversityUnited States Anti-disciplinary: doing academic research when you like too many things Exploring Consequences of Privacy Policies with Narrative Generation via Answer Set Programming Towards Declarative Content Generation for Creativity Support Tools Invited Speaker in Speakers within the PLMW @ POPL-track
Patrick MassotMassot, Patrick Formalising the h-principle and sphere eversion
Isabella MastroeniMastroeni, Isabella University of Verona, ItalyItaly Committee Member in Program Committee within the POPL -track
Cristina MatacheMatache, Cristina University of Edinburgh Denotational semantics of languages for inference: semirings, monads, and tensors
Adrián Doña MateoMateo, Adrián Doña The University of Edinburgh Encoding Dependently-Typed Constructions into Simple Type Theory
Christoph MathejaMatheja, Christoph DTUDenmark Session Chair of Relational & Automated Verification (part of POPL ) Deductive Verification of Probabilistic Programs A Calculus for Amortized Expected Runtimes Committee Member in Program Committee within the POPL -track
Umang MathurMathur, Umang National University of SingaporeSingapore Session Chair of Algorithmic Verification (part of POPL ) Algorithmic Verification Dynamic Race Detection with O(1) Samples Committee Member in Program Committee within the POPL -track
Ralph MatthesMatthes, Ralph IRIT (CNRS and Univ. of Toulouse) Formalizing Monoidal Categories and Actions for Syntax with Binders
McKenna McCallMcCall, McKenna Carnegie Mellon UniversityUnited States Committee Member in Program Committee within the PriSC-track
Craig McLaughlinMcLaughlin, Craig UNSWAustralia Dargent: A Silver Bullet for Verified Data Layout Refinement
Kenneth L. McMillanMcMillan, Kenneth L. University of Texas at AustinUnited States Synthesizing History and Prophecy Variables for Symbolic Model Checking
Bhavik MehtaMehta, Bhavik University of Cambridge Formalising Sharkovsky's Theorem (Proof Pearl)
Vaibhav MehtaMehta, Vaibhav Princeton UniversityUnited States SwitchLog: A Logic Programming Language for Network Switches
Orestis MelkonianMelkonian, Orestis University of EdinburghUnited Kingdom Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Kayvan MemarianMemarian, Kayvan University of CambridgeUnited Kingdom CN: Verifying Systems C Code with Separation-Logic Refinement Types
Baoluo MengMeng, Baoluo GE ResearchUnited States UAV Compliance Checking using Answer Set Programming and Minimal Explanations towards Compliance (Application Paper)
Denis MerigouxMerigoux, Denis INRIAFrance Experience report: implementing a real-world, medium-sized program derived from a legislative specification Opening comments Co-chair in Program Committee within the ProLaLa-track
Stephen MerzMerz, Stephen Inria Nancy Committee Member in Program Committee within the VMCAI-track
Alexandra E. MichaelMichael, Alexandra E. University of California at San Diego; University of WashingtonUnited States Session Chair of Thursday Evening Session Preview (part of POPL Session Previews) MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
Kristopher MicinskiMicinski, Kristopher Syracuse UniversityUnited States Publicity Chair in Organizing Committee for POPL 2023
Aart MiddeldorpMiddeldorp, Aart University of Innsbruck A Formalization of the Development Closedness Criterion for Left-Linear Term Rewrite Systems
Stefan MiliusMilius, Stefan University of Erlangen-NurembergGermany Towards a Higher-Order Mathematical Operational Semantics
Dale MillerMiller, Dale Inria & École PolytechniqueFrance Committee Member in Steering Committee within the CPP-track
Todd MillsteinMillstein, Todd University of California at Los AngelesUnited States Bit-Blasting Probabilistic Programs Committee Member in Program Committee within the POPL -track
Anders MiltnerMiltner, Anders Simon Fraser UniversityUnited States Workshops Co-Chair in Organizing Committee for POPL 2023
Sasa MisailovicMisailovic, Sasa University of Illinois at Urbana-ChampaignUnited States Automatic Differentiation: Session Preview
Swarup MohalikMohalik, Swarup SMT-Based Modeling and Verification of Spiking Neural Networks: A Case Study
Alexandre MoineMoine, Alexandre InriaFrance Session Chair of Friday Breakfast Session Preview (part of POPL Session Previews) A High-Level Separation Logic for Heap Space under Garbage Collection
Shouvick MondalMondal, Shouvick IIT Gandhinagar, IndiaIndia Committee Member in Artifact Evaluation Committee within the VMCAI-track
J. Garrett MorrisMorris, J. Garrett University of IowaUnited States A Type-Based Approach to Divide-and-Conquer Recursion in Coq
Jason MorrisMorris, Jason Blawx: User-friendly Goal-Directed Answer Set Programming for Rules as Code
Greg MorrisettMorrisett, Greg Cornell UniversityUnited States A Core Calculus for Equational Proofs of Cryptographic Protocols
Sean MossMoss, Sean University of Oxford Denotational semantics of languages for inference: semirings, monads, and tensors
Cameron MoyMoy, Cameron Northeastern UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Sujit Kumar MuduliMuduli, Sujit Kumar IIT KanpurIndia Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Reed MullanixMullanix, Reed University of MinnesotaUnited States An Order-Theoretic Analysis of Universe Polymorphism
Niek MullenersMulleners, Niek Utrecht UniversityNetherlands Program Synthesis Using Example Propagation
Andrzej MurawskiMurawski, Andrzej University of OxfordUnited Kingdom Committee Member in Program Committee within the POPL -track
Suha Orhun MutluergilMutluergil, Suha Orhun Sabanci University, Turkey A Pragmatic Approach to Stateful Partial Order Reduction Committee Member in Program Committee within the VMCAI-track
César MuñozMuñoz, César Amazon Web ServicesUnited States Committee Member in Program Committee within the CPP-track
Andrew MyersMyers, Andrew Cornell University General Chair in Organizing Committee for POPL 2023 Session Chair of Welcome (part of POPL ) Session Chair of Panel: Next 50 Years of POPL (part of POPL ) Universally Composable Security for Program Partitioning
Anders MörtbergMörtberg, Anders Department of Mathematics, Stockholm UniversitySweden Computing Cohomology Rings in Cubical Agda
N Chasity NadeauNadeau, Chasity Formalizing and Reasoning about Contracts between Agents
Santosh NagarakatteNagarakatte, Santosh Rutgers UniversityUnited States Committee Member in Program Committee within the POPL -track Committee Member in Steering Committee within the PriSC-track
Ramana NagasamudramNagasamudram, Ramana Stevens Institute of TechnologyUnited States An Algebra of Alignment for Relational Verification Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Kedar NamjoshiNamjoshi, Kedar Nokia Bell LabsUnited States Committee Member in Program Committee within the VMCAI-track
Chandrakana NandiNandi, Chandrakana CertoraUnited States babble: Learning Better Abstractions with E-Graphs and Anti-unification
Aleksandar NanevskiNanevski, Aleksandar IMDEA Software InstituteSpain Committee Member in Program Committee within the POPL -track
Oliver NashNash, Oliver Imperial College, London Formalising the h-principle and sphere eversion
David NaumannNaumann, David Stevens Institute of TechnologyUnited States An Algebra of Alignment for Relational Verification Committee Member in Program Committee within the POPL -track
Jorge A. NavasNavas, Jorge A. Certora, inc.United States Committee Member in Program Committee within the VMCAI-track
Amirmohammad NazariNazari, Amirmohammad University of Southern California Committee Member in Artifact Evaluation Committee within the VMCAI-track
Joseph P. NearNear, Joseph P. University of VermontUnited States πMPC: Automatic Security Proofs for MPC Protocols
David NetoNeto, David GoogleCanada Taking Back Control in an Intermediate Representation for GPU Computing
Max S. NewNew, Max S. University of Michigan Session Chair of Semantics II (part of POPL ) Type Theory: Session Preview
Minh NgoNgo, Minh Stevens Institute of TechnologyUnited States An Algebra of Alignment for Relational Verification
Minh NguyenNguyen, Minh University of BristolUnited Kingdom Towards type-driven data-science in Idris
Tuan NguyenNguyen, Tuan National Institute of InformaticsJapan Linear Algebraic Abduction with Partial Evaluation
Haobin NiNi, Haobin Cornell University ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER
Eske Hoy NielsenNielsen, Eske Hoy Aarhus University Formalising Decentralised Exchanges in Coq
Tobias NipkowNipkow, Tobias Technische Universität MünchenGermany Committee Member in Program Committee within the CPP-track Committee Member in Steering Committee within the CPP-track
Naoki NishidaNishida, Naoki Nagoya UniversityJapan Session Chair of Analysis and Symbolic Methods (part of PADL) From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriting
James NobleNoble, James Research & ProgrammingNew Zealand RUST: Regions, Uniqueness, Ownership & Types
Tereza NovotnáNovotná, Tereza Masaryk university Designing an experiment for comparing user interfaces for legal formalization
O Liam O'ConnorO'Connor, Liam University of EdinburghUnited Kingdom Dargent: A Silver Bullet for Verified Data Layout Refinement
William O'HanleyO'Hanley, William Stanford CodeXCanada Visual Propositional Logic With yscript
Peter O'HearnO'Hearn, Peter Facebook Incorrectness Logic and Under-approximation: Foundations of Bug Catching
Theo X. OlaussonOlausson, Theo X. Massachusetts Institute of TechnologyUnited States Top-Down Synthesis for Library Learning
Federico OlimpieriOlimpieri, Federico University of LeedsUnited Kingdom Why Are Proofs Relevant in Proof-Relevant Models?
Arthur Oliveira ValeOliveira Vale, Arthur Yale UniversityUnited States A Compositional Theory of Linearizability
Bruno C. d. S. OliveiraOliveira, Bruno C. d. S. University of Hong KongChina Making a Type Difference: Subtraction on Intersection Types as Generalized Record Operations Recursive Subtyping for All A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈
C.-H. Luke OngOng, C.-H. Luke University of OxfordUnited Kingdom Pitfalls of Full Bayesian Inference in Universal Probabilistic Programming Exact Inference for Discrete Probabilistic Programs via Generating Functions
C.-H. Luke OngOng, C.-H. Luke NTU On the Reparameterisation Gradient for Non-Differentiable but Continuous Models
Dominic OrchardOrchard, Dominic University of Kent, UKUnited Kingdom Committee Member in Program Committee within the POPL -track
Gerardo OrtizOrtiz, Gerardo Indiana University Symbolic Execution of Hadamard-Toffoli Quantum Circuits
Klaus OstermannOstermann, Klaus University of Tübingen Committee Member in Program Committee within the POPL -track
P Francesco PacenzaPacenza, Francesco Department of Mathematics and Computer Science, University of CalabriaItaly Integrating ASP-based incremental reasoning in the videogame development workflow (Application Paper)
Oded PadonPadon, Oded VMware ResearchUnited States Committee Member in Program Committee within the POPL -track
Michele PaganiPagani, Michele IRIF - Université de Paris CitéFrance The Variable Elimination Algorithm as a Let-Term Rewriting Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the LAFI-track
Viktor PalmkvistPalmkvist, Viktor KTH Royal Institute of TechnologySweden Partial Evaluation of Forward-Mode Automatic Differentiation Statically Resolvable Ambiguity
Jens PalsbergPalsberg, Jens University of California, Los Angeles (UCLA)United States Session Chair of Keynote + 1 talk (part of PEPM) Wrap up Quantum Computing: Session Preview PC Chair in Organizing Committee within the PEPM-track
Hugo PaquetPaquet, Hugo University of OxfordUnited Kingdom Random probability distributions as natural transformations Affine Monads and Lazy Structures for Bayesian Programming
Zoe ParaskevopoulouParaskevopoulou, Zoe Northeastern UniversityUnited States Committee Member in Program Committee within the CoqPL-track
Alessandro ParentiParenti, Alessandro University of Bologna Legal Contracts Amending in Stipula
Jihee ParkPark, Jihee KAISTSouth Korea Semantic Transformation Framework for Rewriting Rules
Gennaro ParlatoParlato, Gennaro University of Molise Committee Member in Program Committee within the VMCAI-track
Bryan ParnoParno, Bryan Carnegie Mellon UniversityUnited States FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
Corina S. PasareanuPasareanu, Corina S. Carnegie Mellon University Silicon Valley, NASA Ames Research Center Committee Member in Program Committee within the VMCAI-track
Adam PaszkePaszke, Adam Google ResearchPoland Contextual source code AD transformations for sum types You Only Linearize Once: Tangents Transpose to Gradients
Marco PatrignaniPatrignani, Marco University of TrentoItaly Session Chair of Logic Programming (part of POPL ) Blame-Preserving Secure Compilation Robust Constant-Time Cryptography MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the PriSC-track
Lawrence PaulsonPaulson, Lawrence University of CambridgeUnited Kingdom Committee Member in Program Committee within the CPP-track
Hila PelegPeleg, Hila TechnionIsrael Committee Member in Program Committee within the PEPM-track
Mário PereiraPereira, Mário NOVA LINCS & DI -- Nova School of Science and Technology Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Daniel PerelmanPerelman, Daniel MicrosoftUnited States FlashFill++: Scaling Programming by Example by Cutting to the Chase
Simona PerriPerri, Simona University of Calabria, Italy Committee Member in Program Committee within the PADL-track
Elizaveta PertsevaPertseva, Elizaveta UCSD Scalable Synthesis of Regular Expressions From Only Positive Examples
Rudy PetersonPeterson, Rudy Cornell University P4Cub: A Little Language for Big Routers
Anja Petković KomelPetković Komel, Anja TU Wien, ViennaAustria Committee Member in Program Committee within the CPP-track
Tatjana PetrovPetrov, Tatjana Universität KonstanzGermany Committee Member in Program Committee within the VMCAI-track
Alberto PettorossiPettorossi, Alberto University of Rome Tor Vergata, ItalyItaly Multiple Query Satisfiability of Constrained Horn Clauses
David PichardiePichardie, David MetaFrance Session Chair of Program Analysis & Parsing (part of POPL ) Program Analysis & Parsing: Session Preview Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler Committee Member in Program Committee within the POPL -track
Robin PiedeleuPiedeleu, Robin University of Oxford On Iteration in Discrete Probabilistic Programming
Brigitte PientkaPientka, Brigitte McGill UniversityCanada Session Chair of Type Theory (part of POPL ) Session Chair of Business Meeting (part of CPP) Session Chair of Proof Search (part of CPP) Committee Member in Program Committee within the POPL -track PC Chair in Program Committee within the CPP-track PC Chair in Organizing Committee within the CPP-track Committee Member in Steering Committee within the CPP-track
Benjamin C. PiercePierce, Benjamin C. University of PennsylvaniaUnited States Session Chair of Security (part of POPL ) Imagining the Reader Types II: Session Preview Panel: Next 50 Years of POPL Committee Member in Program Committee within the POPL -track Invited Speaker in Speakers within the PLMW @ POPL-track Co-chair in Program Committee within the CoqPL-track
Elton PintoPinto, Elton Georgia Institute of Technology Neko: A quantum map-filter-reduce programming language
Ruzica PiskacPiskac, Ruzica Yale UniversityUnited States Academic keynote : A Logician and Lawyer walk into a Classroom
Clément Pit-ClaudelPit-Claudel, Clément EPFLSwitzerland Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the CPP-track Committee Member in Program Committee within the PriSC-track Committee Member in Program Committee within the CoqPL-track
Andrew M. PittsPitts, Andrew M. University of CambridgeUnited Kingdom Locally Nameless Sets
André PlatzerPlatzer, André Karlsruhe Institute of Technology A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
Gordon PlotkinPlotkin, Gordon Google Contextual source code AD transformations for sum types Committee Member in Program Committee within the LAFI-track
Andreas PodelskiPodelski, Andreas University of FreiburgGermany Stratified Commutativity in Verification Algorithms for Concurrent Programs Committee Member in Program Committee within the POPL -track
Elizabeth PolgreenPolgreen, Elizabeth University of EdinburghUnited Kingdom Committee Member in Program Committee within the PriSC-track
Nadia PolikarpovaPolikarpova, Nadia University of California at San DiegoUnited States Session Chair of Synthesis I (part of POPL ) Big Ideas in Program Synthesis Synthesis I: Session Preview babble: Learning Better Abstractions with E-Graphs and Anti-unification Panel: Next 50 Years of POPL Committee Member in Program Committee within the POPL -track Invited Speaker in Speakers within the PLMW @ POPL-track
Enrico PontelliPontelli, Enrico New Mexico State University Committee Member in Program Committee within the PADL-track
Andrei PopescuPopescu, Andrei University of SheffieldUnited Kingdom Isabelle/HOL: Foundations, Induction, and Coinduction Admissible Types-to-PERs Relativization in Higher-Order Logic Committee Member in Steering Committee within the CPP-track
Deena PostolPostol, Deena University of Maryland Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
François PottierPottier, François InriaFrance A High-Level Separation Logic for Heap Space under Garbage Collection Associate Chair in Program Committee within the POPL -track
Damien PousPous, Damien CNRS Committee Member in Program Committee within the POPL -track
Maurizio ProiettiProietti, Maurizio CNR-IASIItaly Multiple Query Satisfiability of Constrained Horn Clauses
Kai-Oliver ProttPrott, Kai-Oliver University of Kiel, GermanyGermany Embedding Functional Logic Programming in Haskell via a Compiler Plugin
Jonathan ProtzenkoProtzenko, Jonathan Microsoft Research, RedmondUnited States Session Chair of Session #1 (part of ProLaLa) Session Chair of Session #2 (part of ProLaLa) Session Chair of Session #4 (part of ProLaLa) Session Chair of Session #3 (part of ProLaLa) Opening comments Formalising Criminal Law in Catala Co-chair in Program Committee within the ProLaLa-track Committee Member in Steering Committee within the PriSC-track
Loïc PujetPujet, Loïc InriaFrance Impredicative Observational Equality
Christopher PultePulte, Christopher University of CambridgeUnited Kingdom CN: Verifying Systems C Code with Separation-Logic Refinement Types Committee Member in Program Committee within the POPL -track
Romain PéchouxPéchoux, Romain Université de Lorraine; CNRS; Inria; LORIAFrance A General Noninterference Policy for Polynomial Time
Pierre-Marie PédrotPédrot, Pierre-Marie INRIAFrance ∂ is for Dialectica: typing differentiable programming Committee Member in Program Committee within the CPP-track
Corina S. PăsăreanuPăsăreanu, Corina S. Carnegie Mellon UniversityUnited States Committee Member in Program Committee within the POPL -track
Q Xiaokang QiuQiu, Xiaokang Purdue UniversityUnited States Comparative Synthesis: Learning Near-Optimal Network Designs by Query
R Felipe R. MonteiroR. Monteiro, Felipe AmazonUnited States Committee Member in Program Committee within the VMCAI-track Committee Member in Artifact Evaluation Committee within the VMCAI-track
Azalea RaadRaad, Azalea Imperial College LondonUnited Kingdom Incorrectness Logic and Under-approximation: Foundations of Bug Catching Panel: Next 50 Years of POPL The Path to Durable Linearizability Committee Member in Program Committee within the POPL -track
Arjun RadhakrishnaRadhakrishna, Arjun MicrosoftUnited States FlashFill++: Scaling Programming by Example by Cutting to the Chase
Alexey RadulRadul, Alexey Google ResearchUnited States You Only Linearize Once: Tangents Transpose to Gradients
Mukund RaghothamanRaghothaman, Mukund University of Southern California Artifact Evaluation Co-Chair in Organizing Committee for POPL 2023
Mukund RaghothamanRaghothaman, Mukund University of Southern CaliforniaUnited States Automatic Rollback Suggestions for Incremental Datalog Evaluation
Mukund RaghothamanRaghothaman, Mukund University of Southern California Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Tom RainforthRainforth, Tom Department of Statistics, University of Oxford Pitfalls of Full Bayesian Inference in Universal Probabilistic Programming
Ravi RamamurthyRamamurthy, Ravi Microsoft Research FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Tahina RamananandroRamananandro, Tahina Microsoft ResearchUnited States ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Jan-Paul Ramos-DavilaRamos-Davila, Jan-Paul Cornell UniversityUnited States Evaluating Soundness of a Gradual Verifier with Property Based Testing
Steven RamsayRamsay, Steven University of BristolUnited Kingdom Higher-Order MSL Horn Constraints
Robert RandRand, Robert University of ChicagoUnited States Qunity: A Unified Language for Quantum and Classical Computing Committee Member in Program Committee within the POPL -track
Sanjay RaoRao, Sanjay Purdue UniversityUnited States Comparative Synthesis: Learning Near-Optimal Network Designs by Query
Aseem RastogiRastogi, Aseem Microsoft ResearchIndia FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
Rolph RectoRecto, Rolph Cornell UniversityUnited States Universally Composable Security for Program Partitioning
Baber RehmanRehman, Baber University of Hong Kong Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Tim ReicheltReichelt, Tim University of Oxford Pitfalls of Full Bayesian Inference in Universal Probabilistic Programming
John RennerRenner, John University of California at San Diego, USA Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers
Thomas RepsReps, Thomas University of Wisconsin-MadisonUnited States Unrealizability Logic Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear Programming
Tamara RezkRezk, Tamara INRIAFrance Sound Symbolic Execution via Abstract Interpretation and its Application to Security Committee Member in Steering Committee within the PriSC-track
Vivien RindisbacherRindisbacher, Vivien Boston UniversityUnited States Verified Differential Privacy for Finite Computers
Noam RinetzkyRinetzky, Noam Tel Aviv UniversityIsrael Committee Member in Program Committee within the POPL -track
Talia RingerRinger, Talia University of Illinois at Urbana-ChampaignUnited States Towards Formally Verified Path ORAM in Coq Committee Member in Program Committee within the CoqPL-track
Nick RiouxRioux, Nick University of PennsylvaniaUnited States A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈
Xavier RivalRival, Xavier Inria; ENS; CNRS; PSL UniversityFrance Session Chair of Static Analysis (part of VMCAI) Sound Symbolic Execution via Abstract Interpretation and its Application to Security Resource Analysis: Session Preview Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference
Christine RizkallahRizkallah, Christine University of MelbourneAustralia Dargent: A Silver Bullet for Verified Data Layout Refinement Committee Member in Program Committee within the CPP-track Committee Member in Program Committee within the CoqPL-track
Emanuel RodriguesRodrigues, Emanuel HASLab & INESC TEC, University of Minho Efficient Embedding of Strategic Attribute Grammars via Memoization
Neil Julien RossRoss, Neil Julien Dalhousie UniversityCanada Proto-Quipper with Dynamic Lifting
Cody RouxRoux, Cody AWSUnited States Session Chair of Languages and Compilers (part of CPP) Logic Programming: Session Preview Committee Member in Program Committee within the CPP-track
Thomas RubianoRubiano, Thomas LIPN – UMR 7030 Université Sorbonne Paris Nord Certifying Complexity Analysis Distributing and Parallelizing Non-canonical Loops
Neea RuschRusch, Neea Augusta UniversityUnited States Session Chair of Friday Morning Break Session Preview (part of POPL Session Previews) Certifying Complexity Analysis Distributing and Parallelizing Non-canonical Loops
Sukyoung RyuRyu, Sukyoung KAISTSouth Korea Session Chair of Industry presentation + 1 talk (part of PEPM) Semantic Transformation Framework for Rewriting Rules Committee Member in Program Committee within the PEPM-track
S Amr SabrySabry, Amr Indiana UniversityUnited States Symbolic Execution of Hadamard-Toffoli Quantum Circuits Committee Member in Program Committee within the POPL -track
Ayumu SaitoSaito, Ayumu Tokyo Institute of Technology Semantics of Probabilistic Programs using S-Finite Kernels in Coq
Kazuhiko SakaguchiSakaguchi, Kazuhiko InriaFrance Committee Member in Program Committee within the CPP-track
Chiaki SakamaSakama, Chiaki Wakayama UniversityJapan Linear Algebraic Abduction with Partial Evaluation
Albin SalazarSalazar, Albin INRIA/CNRS/ENS/PSL*France A generic framework to coarse-grain stochastic reaction networks by Abstract Interpretation
Elmer SalazarSalazar, Elmer The University of Texas at DallasUnited States Jury-trial Story Construction and Analysis using Goal-directed Answer Set Programming
Malavika SamakSamak, Malavika CSAIL, MITUnited States Committee Member in Program Committee within the POPL -track
Michael SammlerSammler, Michael MPI-SWSGermany Conditional Contextual Refinement DimSum: A Decentralized Approach to Multi-language Semantics and Verification Committee Member in Program Committee within the PriSC-track
Dave SandsSands, Dave Chalmers University of TechnologySweden Reconciling Shannon and Scott with a Lattice of Computable Information
Alessio SantamariaSantamaria, Alessio University of Pisa; University of SussexItaly Deconstructing the Calculus of Relations with Tape Diagrams
Sabrine SaouliSaouli, Sabrine CosySEL: Improving SAT Solving Using Local Symmetries
João SaraivaSaraiva, João Efficient Embedding of Strategic Attribute Grammars via Memoization
Giovanni SartorSartor, Giovanni University of BolognaItaly Legal Contracts Amending in Stipula
Ryosuke SatoSato, Ryosuke University of TokyoJapan HFL(Z) Validity Checking for Automated Program Verification
Burkhard SchaferSchafer, Burkhard University of Edinburgh Formalising Criminal Law in Catala
Torsten SchaubSchaub, Torsten University of PotsdamGermany Solving Vehicle Equipment Specification Problems with Answer Set Programming
Bernhard ScholzScholz, Bernhard University of SydneyAustralia Automatic Rollback Suggestions for Incremental Datalog Evaluation
Sven-Bodo ScholzScholz, Sven-Bodo Radboud UniversityNetherlands Committee Member in Program Committee within the PEPM-track
Tom SchrijversSchrijvers, Tom KU LeuvenBelgium Fluo: A Domain-Specific Language for Experiments in Fluorescence Microscopy (Application Paper) Committee Member in Program Committee within the PADL-track
Lutz SchröderSchröder, Lutz University of Erlangen-NurembergGermany Towards a Higher-Order Mathematical Operational Semantics
Daniel Schwartz-NarbonneSchwartz-Narbonne, Daniel Amazon, n.n. Committee Member in Program Committee within the VMCAI-track
Atharva SehgalSehgal, Atharva University of Texas, AustinUnited States Neurosymbolic Programming
Thomas SeillerSeiller, Thomas CNRSFrance Certifying Complexity Analysis Distributing and Parallelizing Non-canonical Loops
Taro SekiyamaSekiyama, Taro National Institute of InformaticsJapan Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations Committee Member in Program Committee within the POPL -track
Peter SelingerSelinger, Peter Dalhousie UniversityCanada Proto-Quipper with Dynamic Lifting
Viktor SenderovSenderov, Viktor Naturhistoriska riksmuseet Static Delayed Sampling for Probabilistic Programming Languages
Eli SenneshSennesh, Eli Northeastern UniversityUnited States A convenient category of tracing measure kernels Semantics of Probabilistic Program Traces Committee Member in Program Committee within the LAFI-track
Ilya SergeySergey, Ilya National University of SingaporeSingapore Industrial Relations in Organizing Committee for POPL 2023 Committee Member in Program Committee within the PEPM-track
Peter SewellSewell, Peter University of CambridgeUnited Kingdom CN: Verifying Systems C Code with Separation-Logic Refinement Types
Thomas SewellSewell, Thomas University of CambridgeUnited Kingdom CN: Verifying Systems C Code with Separation-Logic Refinement Types
Hovav ShachamShacham, Hovav University of Texas at Austin FaJITa: Verifying Optimizations on Just-In-Time Programs Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers
Chung-chieh ShanShan, Chung-chieh Indiana University, USA Steering Committee Member in Steering Committee within the LAFI-track
Jeannine ShantzShantz, Jeannine Formalizing and Reasoning about Contracts between Agents
Zhong ShaoShao, Zhong Yale UniversityUnited States A Compositional Theory of Linearizability Committee Member in Steering Committee within the CPP-track
Scott ShapiroShapiro, Scott Yale Law SchoolUnited States Academic keynote : A Logician and Lawyer walk into a Classroom
Abhishek SharmaSharma, Abhishek UC San Diego Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers
Subodh SharmaSharma, Subodh IIT DelhiIndia Committee Member in Program Committee within the VMCAI-track
Gan ShenShen, Gan University of California, Santa Cruz, USA HasChor: Choreographic Programming in Haskell
Elaine ShiShi, Elaine Carnegie Mellon UniversityUnited States A Core Calculus for Equational Proofs of Cryptographic Protocols
Pengyuan ShiShi, Pengyuan University of WaterlooCanada Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortized Probabilistic Inference
Qingkai ShiShi, Qingkai Purdue UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Shweta ShindeShinde, Shweta ETH ZurichSwitzerland Co-chair in Program Committee within the PriSC-track Committee Member in Steering Committee within the PriSC-track
Sharon ShohamShoham, Sharon Tel Aviv UniversityIsrael Towards a Theoretical Understanding of Property-Directed Reachability Panel: Next 50 Years of POPL
Calvin ShyuShyu, Calvin Cornell University P4Cub: A Little Language for Big Routers
Mihaela SighireanuSighireanu, Mihaela IRIF, Université Paris Diderot, FranceFrance Committee Member in Program Committee within the VMCAI-track
Georges-André SilberSilber, Georges-André Mines Paris, PSL UniversityFrance Towards an Automatic Consolidation of French Law
Giovanni SilenoSileno, Giovanni University of Amsterdam Committee Member in Program Committee within the ProLaLa-track
Alexandra SilvaSilva, Alexandra Cornell UniversityUnited States On Iteration in Discrete Probabilistic Programming Probabilistic Inference: Session Preview
Lucas SilverSilver, Lucas University of PennsylvaniaUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Clint SimonSimon, Clint MicrosoftUnited States FlashFill++: Scaling Programming by Example by Cutting to the Chase
Abhishek Kr SinghSingh, Abhishek Kr Tel Aviv UniversityIsrael An Operational Approach to Library Abstraction under Relaxed Memory Concurrency
Satnam SinghSingh, Satnam GroqUnited States Committee Member in Program Committee within the PEPM-track
Kartik SinghalSinghal, Kartik University of ChicagoUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Jeffrey Mark SiskindSiskind, Jeffrey Mark Elmore Family School of Electrical and Computer Engineering, Purdue UniversityUnited States Steering Committee Member in Steering Committee within the LAFI-track
Anna SlobodovaSlobodova, Anna IntelUnited States Committee Member in Program Committee within the CPP-track
Tom SmedingSmeding, Tom Utrecht UniversityNetherlands Efficient Dual-Numbers Reverse AD via Well-Known Program Transformations
Fred SmithSmith, Fred MathWorksUnited States MATLAB Coder: Partial Evaluation in Practice
Michael SmithSmith, Michael UC San DiegoUnited States FaJITa: Verifying Optimizations on Just-In-Time Programs Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers
Gert SmolkaSmolka, Gert Saarland University A Computational Cantor-Bernstein and Myhill’s Isomorphism Theorem in Constructive Type Theory (Proof Pearl)
Kristina SojakovaSojakova, Kristina InriaFrance A Core Calculus for Equational Proofs of Cryptographic Protocols
Armando Solar-LezamaSolar-Lezama, Armando Massachusetts Institute of TechnologyUnited States Neurosymbolic Programming Combining Functional and Automata Synthesis to Discover Causal Reactive Programs Top-Down Synthesis for Library Learning
Tran Cao SonSon, Tran Cao New Mexico State UniversityUnited States Formalizing and Reasoning about Contracts between Agents
John SonchackSonchack, John University of Pennsylvania, USA SwitchLog: A Logic Programming Language for Network Switches
Youngju SongSong, Youngju Seoul National University; MPI-SWSSouth Korea Conditional Contextual Refinement DimSum: A Decentralized Approach to Multi-language Semantics and Verification
Simon SpiesSpies, Simon MPI-SWSGermany DimSum: A Decentralized Approach to Multi-language Semantics and Verification
Bas SpittersSpitters, Bas Concordium Blockchain Research Center, Aarhus University Formalising Decentralised Exchanges in Coq
Mandayam SrivasSrivas, Mandayam Chennai Mathematical Institute Committee Member in Program Committee within the VMCAI-track
Caleb StanfordStanford, Caleb University of California, San Diego; University of California, DavisUnited States A Robust Theory of Series Parallel Graphs Logic & Decidability II: Session Preview
Sam StatonStaton, Sam University of OxfordUnited Kingdom Denotational semantics of languages for inference: semirings, monads, and tensors What do posterior distributions of probabilistic programs look like? ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs Affine Monads and Lazy Structures for Bayesian Programming
Deian StefanStefan, Deian University of California at San DiegoUnited States FaJITa: Verifying Optimizations on Just-In-Time Programs Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers Robust Constant-Time Cryptography Verified Compilation: Session Preview MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code Committee Member in Steering Committee within the PriSC-track
Dario SteinStein, Dario University of Oxford Committee Member in Program Committee within the LAFI-track
Jonathan SterlingSterling, Jonathan Aarhus UniversityDenmark Committee Member in Program Committee within the POPL -track
Michel SteuwerSteuwer, Michel University of EdinburghUnited Kingdom Towards type-driven data-science in Idris
J. Ryan StinnettStinnett, J. Ryan King's College LondonUnited Kingdom Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Quentin StiévenartStiévenart, Quentin Vrije Universiteit BrusselBelgium Result Invalidation for Incremental Modular Analyses
Pierre-Yves StrubStrub, Pierre-Yves MetaFrance A Formal Disproof of Hirsch Conjecture CoqQ: Foundational Verification of Quantum Programs
Sandro StuckiStucki, Sandro Amazon Prime VideoSweden Reconciling Shannon and Scott with a Lattice of Computable Information
Aaron StumpStump, Aaron University of IowaUnited States A Type-Based Approach to Divide-and-Conquer Recursion in Coq Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the CPP-track
Pavle SuboticSubotic, Pavle Microsoft AzureSerbia Automatic Rollback Suggestions for Incremental Datalog Evaluation
Eijiro SumiiSumii, Eijiro Tohoku UniversityJapan Committee Member in Program Committee within the POPL -track
Ariadne Si SuoSuo, Ariadne Si University of Oxford Denotational semantics of languages for inference: semirings, monads, and tensors
Nikhil SwamySwamy, Nikhil Microsoft ResearchUnited States ASN1*: Provably Correct, Non-Malleable Parsing for ASN.1 DER FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores
T Quang-Trung TaTa, Quang-Trung National University of SingaporeSingapore ARENA: Enhancing Abstract Refinement for Neural Network Verification
Nicolas TabareauTabareau, Nicolas InriaFrance Impredicative Observational Equality Committee Member in Program Committee within the POPL -track
Raito TakeuchiTakeuchi, Raito Nagoya UniversityJapan Solving Vehicle Equipment Specification Problems with Answer Set Programming
Naoyuki TamuraTamura, Naoyuki Kobe University, JAPANJapan Solving Vehicle Equipment Specification Problems with Answer Set Programming
Yong Kiam TanTan, Yong Kiam Carnegie Mellon University A First Complete Algorithm for Real Quantifier Elimination in Isabelle/HOL
Kento TanahashiTanahashi, Kento University of TokyoJapan HFL(Z) Validity Checking for Automated Program Verification
Éric TanterTanter, Éric University of Chile Committee Member in Program Committee within the POPL -track
Paul TarauTarau, Paul University of North TexasUnited States Committee Member in Program Committee within the PADL-track
Joseph TassarottiTassarotti, Joseph NYUUnited States Career Trajectories in PL Committee Member in Program Committee within the POPL -track Panelist in Panelists within the PLMW @ POPL-track
Enrico TassiTassi, Enrico INRIAFrance Practical and sound equality tests, automatically
Christine TassonTasson, Christine Sorbonne Université — LIP6France Session Chair of Second Session (part of LAFI) Session Chair of Third Session (part of LAFI) Session Chair of First Session (part of LAFI) Opening Comments Co-chair in Organizing Committee within the LAFI-track Co-chair in Program Committee within the LAFI-track
Zachary TatlockTatlock, Zachary University of WashingtonUnited States babble: Learning Better Abstractions with E-Graphs and Anti-unification
Zenna TavaresTavares, Zenna Basis; Columbia UniversityUnited States Combining Functional and Automata Synthesis to Discover Causal Reactive Programs
Finn TeegenTeegen, Finn University of Kiel, GermanyGermany Embedding Functional Logic Programming in Haskell via a Compiler Plugin
Joshua B. TenenbaumTenenbaum, Joshua B. Massachusetts Institute of TechnologyUnited States Combining Functional and Automata Synthesis to Discover Causal Reactive Programs Top-Down Synthesis for Library Learning
Tachio TerauchiTerauchi, Tachio Waseda UniversityJapan Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification
Jérémy ThibaultThibault, Jérémy MPI-SPGermany SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability Machine Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Peter ThiemannThiemann, Peter University of Freiburg, Germany Session Types Meet Polymorphism and Dependent Types Committee Member in Program Committee within the PADL-track Invited Speaker in Speakers within the PLMW @ POPL-track
René ThiemannThiemann, René University of InnsbruckAustria Committee Member in Program Committee within the CPP-track
David ThienThien, David UC San Diego FaJITa: Verifying Optimizations on Just-In-Time Programs Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers
Ramanathan S. ThinniyamThinniyam, Ramanathan S. MPI-SWSGermany Context-Bounded Verification of Context-Free Specifications
Amin TimanyTimany, Amin Aarhus UniversityDenmark Committee Member in Program Committee within the CPP-track
Ignacio TiraboschiTiraboschi, Ignacio Inria, France / ENS, FranceArgentina Sound Symbolic Execution via Abstract Interpretation and its Application to Security
Abhishek TiwariTiwari, Abhishek University of Passau, GermanyGermany Committee Member in Artifact Evaluation Committee within the VMCAI-track
Ashish TiwariTiwari, Ashish MicrosoftUnited States FlashFill++: Scaling Programming by Example by Cutting to the Chase
Saeid Tizpaz-NiariTizpaz-Niari, Saeid University of Texas at El PasoUnited States Committee Member in Program Committee within the ProLaLa-track
Sam Tobin-HochstadtTobin-Hochstadt, Sam Indiana University Committee Member in Program Committee within the POPL -track
Ryo TokudaTokuda, Ryo University of Tsukuba Generating Programs for Polynomial Multiplication with Correctness Assurance
Andrew TolmachTolmach, Andrew Portland State UniversityUnited States SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability Machine Committee Member in Program Committee within the POPL -track
Paulo TorrensTorrens, Paulo University of Kent On the metatheory of IRs and the CPS-calculus
Mateo Torres-RuizTorres-Ruiz, Mateo On Iteration in Discrete Probabilistic Programming
Emma ToschTosch, Emma Northeastern University, USA Session Chair of Session #3 (part of ProLaLa) Exploring Consequences of Privacy Policies with Narrative Generation via Answer Set Programming Committee Member in Program Committee within the ProLaLa-track
James TownsendTownsend, James University of Amsterdam Verified Reversible Programming for Verified Lossless Compression
Dmitriy TraytelTraytel, Dmitriy University of CopenhagenDenmark Session Chair of Practical Proving (part of CPP) Isabelle/HOL: Foundations, Induction, and Coinduction Admissible Types-to-PERs Relativization in Higher-Order Logic Conference Chair in Organizing Committee within the CPP-track Committee Member in Steering Committee within the CPP-track
Jean-Baptiste TristanTristan, Jean-Baptiste Amazon Web ServicesUnited States Steering Committee Member in Steering Committee within the LAFI-track
Stelios TsampasTsampas, Stelios University of Erlangen-NurembergGermany Towards a Higher-Order Mathematical Operational Semantics Committee Member in Program Committee within the PriSC-track
Takeshi TsukadaTsukada, Takeshi Chiba UniversityJapan HFL(Z) Validity Checking for Automated Program Verification Optimal CHC Solving via Termination Proofs
Kanae TsushimaTsushima, Kanae National Institute of Informatics, JapanJapan Towards Type Debugging using Partial Evaluation
Hünkar Can TunçTunç, Hünkar Can Aarhus UniversityDenmark Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Julia TurcottiTurcotti, Julia MIT-CSAIL Wisening Assertions: A live Bayesian reasoning system for probabilistic correctness
Seppo TörmäTörmä, Seppo VisuaLynk Oy, Finland Building Information Modeling Using Constraint Logic Programming (Extended Abstract)
U Hiroshi UnnoUnno, Hiroshi University of Tsukuba; RIKEN AIPJapan Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification Optimal CHC Solving via Termination Proofs
Josef UrbanUrban, Josef Czech Technical University in PragueCzechia Committee Member in Program Committee within the CPP-track
Henning UrbatUrbat, Henning University of Erlangen-NurembergGermany Towards a Higher-Order Mathematical Operational Semantics
Mark UttingUtting, Mark The University of QueenslandAustralia Verifying term graph optimizations using Isabelle/HOL
V Viktor VafeiadisVafeiadis, Viktor MPI-SWSGermany Session Chair of Formalized Mathematics II (part of CPP) Kater: Automating Weak Memory Model Metatheory and Consistency Checking Principles of Persistent Programming The Path to Durable Linearizability Committee Member in Program Committee within the CPP-track
Nachiappan ValliappanValliappan, Nachiappan Chalmers University of TechnologySweden Modular Construction of Multi-sorted Free Extensions Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Jan-Willem Van De MeentVan De Meent, Jan-Willem University of Amsterdam A convenient category of tracing measure kernels Verified Reversible Programming for Verified Lossless Compression Semantics of Probabilistic Program Traces
Birthe van den Bergvan den Berg, Birthe KU LeuvenBelgium Fluo: A Domain-Specific Language for Experiments in Fluorescence Microscopy (Application Paper)
Guy Van den BroeckVan den Broeck, Guy University of California at Los Angeles Bit-Blasting Probabilistic Programs
Jens Van der PlasVan der Plas, Jens Software Languages Lab, Vrije Universiteit BrusselBelgium Result Invalidation for Incremental Modular Analyses
Cas van der Restvan der Rest, Cas Delft University of TechnologyNetherlands Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects
Floris van Doornvan Doorn, Floris University of PittsburghUnited States Formalising the h-principle and sphere eversion
Sam van Goolvan Gool, Sam Université Paris Cité / IRIF Formalizing and computing propositional quantifiers
Peter Van RoyVan Roy, Peter Université catholique de LouvainBelgium Committee Member in Program Committee within the PADL-track
Julien VanegueVanegue, Julien Bloomberg, USAUnited States Incorrectness Logic and Under-approximation: Foundations of Bug Catching
Sarat Chandra VaranasiVaranasi, Sarat Chandra The University of Texas at Dallas, General Electric ResearchUnited States Session Chair of Domain Specific Languages (part of PADL) UAV Compliance Checking using Answer Set Programming and Minimal Explanations towards Compliance (Application Paper) Jury-trial Story Construction and Analysis using Goal-directed Answer Set Programming
Lisa VasilenkoVasilenko, Lisa IMDEA Software InstituteSpain Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Marco VassenaVassena, Marco Utrecht UniversityNetherlands Robust Constant-Time Cryptography MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code Committee Member in Program Committee within the POPL -track
Amit VasudevanVasudevan, Amit Carnegie Mellon University Towards End-to-End Verified TEEs via Verified Interface Conformance and Interface-Preserving Compilers
Leni VenVen, Leni University of WaterlooCanada Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortized Probabilistic Inference
Hristo VenevVenev, Hristo INSAITBulgaria Compiling and Running High-level Quantum Programs
Abhinav VermaVerma, Abhinav The Pennsylvania State University Committee Member in Selection Committee within the POPL Student Research Competition-track
Lena VerschtVerscht, Lena RWTH Aachen UniversityGermany A Calculus for Amortized Expected Runtimes
Pierre VialVial, Pierre Inria Compositional pre-processing for automated reasoning in dependent type theory
Cole VickVick, Cole Synthesizing History and Prophecy Variables for Symbolic Model Checking
Marcos VieraViera, Marcos University of the Republic, Uruguay Efficient Embedding of Strategic Attribute Grammars via Memoization
Mahesh ViswanathanViswanathan, Mahesh University of Illinois at Urbana-ChampaignUnited States Dynamic Race Detection with O(1) Samples
Finn VoichickVoichick, Finn University of MarylandUnited States Qunity: A Unified Language for Quantum and Classical Computing
Janis VoigtländerVoigtländer, Janis University of Duisburg-Essen Committee Member in Program Committee within the PADL-track
Matthijs VákárVákár, Matthijs Utrecht UniversityNetherlands Efficient Dual-Numbers Reverse AD via Well-Known Program Transformations
W Dominik WagnerWagner, Dominik University of Oxford On the Reparameterisation Gradient for Non-Differentiable but Continuous Models
David WalkerWalker, David Princeton UniversityUnited States SwitchLog: A Logic Programming Language for Network Switches Committee Member in Program Committee within the POPL -track
Jacob WaltersWalters, Jacob University of Edinburgh Towards type-driven data-science in Idris
Xinyi WanWan, Xinyi Shanghai Jiao Tong University Interactive Theorem Proving in Logic Education：A Coq Formalization of ZFC Set Theory for Discrete Mathematics Teaching
Chao WangWang, Chao University of Southern CaliforniaUnited States Differential Verification of Deep Neural Networks
Di WangWang, Di Peking UniversityChina Probabilistic Resource-Aware Session Types
Jingbo WangWang, Jingbo University of Southern California Artifact Evaluation Chair in Organizing Committee within the VMCAI-track
Yanjun WangWang, Yanjun Amazon Web Services, USAUnited States Comparative Synthesis: Learning Near-Optimal Network Designs by Query
Yuepeng WangWang, Yuepeng Simon Fraser UniversityCanada Web Co-Chair in Organizing Committee for POPL 2023 Committee Member in Selection Committee within the POPL Student Research Competition-track
Yuke WangWang, Yuke UC Santa BarbaraUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Yuting WangWang, Yuting Shanghai Jiao Tong UniversityChina Committee Member in Program Committee within the CPP-track
Chris WatsonWatson, Chris University of PennsylvaniaUnited States A Robust Theory of Series Parallel Graphs
Conrad WattWatt, Conrad University of CambridgeUnited Kingdom MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code Committee Member in Program Committee within the POPL -track
Brae J. WebbWebb, Brae J. The University of QueenslandAustralia Verifying term graph optimizations using Isabelle/HOL
Tjark WeberWeber, Tjark Uppsala UniversitySweden Committee Member in Program Committee within the CPP-track
Guannan WeiWei, Guannan Purdue UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Benjamin WernerWerner, Benjamin LIX, IPP Integrating graphical proofs in Coq
John WickersonWickerson, John Imperial College LondonUnited Kingdom Taking Back Control in an Intermediate Representation for GPU Computing
Rüdiger WilhelmiWilhelmi, Rüdiger University of Konstanz Formal Modeling and Analysis of Legal Contracts using ContractCheck
Max WillseyWillsey, Max University of WashingtonUnited States babble: Learning Better Abstractions with E-Graphs and Anti-unification
Tobias WinklerWinkler, Tobias RWTH Aachen UniversityGermany Exact Probabilistic Inference Using Generating Functions
Théo WinterhalterWinterhalter, Théo INRIA SaclayFrance Securely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typed Interfaces Committee Member in Program Committee within the POPL -track
Thorsten WissmannWissmann, Thorsten Radboud University NijmegenNetherlands Fast Coalgebraic Bisimilarity Minimization
Lionel WongWong, Lionel Massachusetts Institute of TechnologyUnited States Top-Down Synthesis for Library Learning
Meng Weng WongWong, Meng Weng Singapore Management UniversitySingapore Defeasible Semantics for L4
Robert WrightWright, Robert The University of Edinburgh, UK Towards type-driven data-science in Idris
Tobias WrigstadWrigstad, Tobias Uppsala University, SwedenSweden RUST: Regions, Uniqueness, Ownership & Types
Kobe WullaertWullaert, Kobe Technical University Delft Formalizing Monoidal Categories and Actions for Syntax with Binders
X Anxhelo XhebrajXhebraj, Anxhelo Purdue UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Ningning XieXie, Ningning University of TorontoCanada Session Chair of Automatic Differentiation (part of POPL ) Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the PADL-track
Han XuXu, Han Peking UniversityChina Making a Type Difference: Subtraction on Intersection Types as Generalized Record Operations
Zesheng XuXu, Zesheng The University of Texas at DallasUnited States Jury-trial Story Construction and Analysis using Goal-directed Answer Set Programming
Runze XueXue, Runze CSE Department at the University of Michigan Zydeco: A Stack-Based Call-By-Push-Value Language
Y Jeremy YallopYallop, Jeremy University of CambridgeUnited Kingdom Modular Construction of Multi-sorted Free Extensions
Hongseok YangYang, Hongseok KAIST; IBSSouth Korea Introduction to the tensor-programs framework, a PL approach that helps analyse theoretical properties of deep learning. Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference
Kexing YingYing, Kexing University of Cambridge A formalization of Doob's martingale convergence theorems in mathlib
Mingsheng YingYing, Mingsheng Institute of Software at Chinese Academy of Sciences; Tsinghua UniversityChina CoqQ: Foundational Verification of Quantum Programs
Anssi Yli-JyräYli-Jyrä, Anssi Tampere UniversityFinland Session Chair of Reasoning (part of PADL) Pruning Redundancy in Answer Set Optimization Applied to Preventive Maintenance Scheduling
Neringa YoungYoung, Neringa Lithuania Treasurer & Conference Manager in Organizing Committee for POPL 2023
Charles YuanYuan, Charles Massachusetts Institute of TechnologyUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Yongwei YuanYuan, Yongwei Purdue University Trace-Guided Inductive Synthesis of Recursive Functional Programs
Z Ahmed Khaled ZaherZaher, Ahmed Khaled HKUSTEgypt Efficient Interprocedural Data-Flow Analysis using Treedepth and Treewidth
Fabian ZaiserZaiser, Fabian University of Oxford Exact Inference for Discrete Probabilistic Programs via Generating Functions
Yannick ZakowskiZakowski, Yannick University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIPFrance Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
Fabio ZanasiZanasi, Fabio University College London On Iteration in Discrete Probabilistic Programming
Jessica ZangariZangari, Jessica Università della CalabriaItaly Integrating ASP-based incremental reasoning in the videogame development workflow (Application Paper)
Francesco Zappa NardelliZappa Nardelli, Francesco MetaFrance Committee Member in Program Committee within the POPL -track
Lucas ZavaliaZavalia, Lucas Florida State University TallahasseeUnited States Solving Constrained Horn Clauses over Algebraic Data Types
Steve ZdancewicZdancewic, Steve University of PennsylvaniaUnited States Session Chair of CompCert and Beyond (part of CPP) Session Chair of Business Meeting (part of CPP) A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈ Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq PC Chair in Program Committee within the CPP-track PC Chair in Organizing Committee within the CPP-track Committee Member in Steering Committee within the CPP-track
Georg ZetzscheZetzsche, Georg MPI-SWSGermany Context-Bounded Verification of Context-Free Specifications
Danfeng ZhangZhang, Danfeng Pennsylvania State UniversityUnited States Student Research Competition Co-Chair in Organizing Committee for POPL 2023 Session Chair of SRC Poster (part of POPL Student Research Competition) Co-chair in Selection Committee within the POPL Student Research Competition-track
Haoran ZhangZhang, Haoran University of PennsylvaniaUnited States Executing Microservice Applications on Serverless, Correctly
Minjian ZhangZhang, Minjian University of Illinois at Urbana-ChampaignUnited States Dynamic Race Detection with O(1) Samples Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Qirun ZhangZhang, Qirun Georgia Institute of TechnologyUnited States Witnessability of Undecidable Problems Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear Programming
Yizhou ZhangZhang, Yizhou University of WaterlooCanada Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortized Probabilistic Inference
Zhen ZhangZhang, Zhen Utah State UniversityUnited States Committee Member in Program Committee within the VMCAI-track
Zichao ZhangZhang, Zichao Carnegie Mellon UniversityUnited States Towards End-to-End Verified TEEs via Verified Interface Conformance and Interface-Preserving Compilers Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
David ZhaoZhao, David The University of SydneyAustralia Automatic Rollback Suggestions for Incremental Datalog Evaluation
Yuyi ZhongZhong, Yuyi ARENA: Enhancing Abstract Refinement for Neural Network Verification
Li ZhouZhou, Li MPI-SP; Institute of Software at Chinese Academy of SciencesGermany CoqQ: Foundational Verification of Quantum Programs
Litao ZhouZhou, Litao University of Hong KongChina Recursive Subtyping for All
Yaoda ZhouZhou, Yaoda University of Hong KongChina Recursive Subtyping for All Committee Member in Artifact Evaluation Committee within the VMCAI-track
Shaowei ZhuZhu, Shaowei Princeton UniversityUnited States When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic
Elena ZuccaZucca, Elena University of GenoaItaly Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the PEPM-track
Florian ZulegerZuleger, Florian TU ViennaAustria Committee Member in Program Committee within the VMCAI-track

POPL 2023 Contributors

Results (857)

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia