POPL 2023 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (582)

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 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 Program Chair in Program Committee within the POPL -track
Mosaad Al ThokairAl Thokair, Mosaad Saudi AramcoSaudi Arabia Dynamic Race Detection With O(1) Samples
Jonathan AldrichAldrich, Jonathan Carnegie Mellon University Using a Proof Assistant to Teach PL Theory, Without the Overhead
Rajeev AlurAlur, Rajeev University of Pennsylvania 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 Research Executing Microservice Applications on Serverless, Correctly
Carlo AngiuliAngiuli, Carlo Carnegie Mellon University An Order-Theoretic Analysis of Universe Polymorphism
Danil AnnenkovAnnenkov, Danil Department of Computer Science, University of Copenhagen Committee Member in Program Committee within the CoqPL-track
Timos AntonopoulosAntonopoulos, Timos Yale University An algebra of alignment for relational verification Committee Member in Program Committee within the ProLaLa-track
Jaime AriasArias, Jaime CNRS, LIPN, Université Sorbonne Paris NordFrance Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Joaquín AriasArias, Joaquín Universidad Rey Juan CarlosSpain Building Information Modeling Using Constraint Logic Programming (Extended Abstract) Committee Member in Program Committee within the ProLaLa-track
Luca ArnaboldiArnaboldi, Luca The University of EdinburghUnited Kingdom Formalising Criminal Law in Catala
Victor ArrialArrial, Victor IRIF- Université Paris CitéFrance Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework
David AspinallAspinall, David University of Edinburgh Formalising Criminal Law in Catala
Mohamed Faouzi AtigAtig, Mohamed Faouzi Uppsala University, Sweden Committee Member in Program Committee within the VMCAI-track
Arthur Azevedo de AmorimAzevedo de Amorim, Arthur Boston UniversityUnited States SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability Machine
B Casper Bach PoulsenBach Poulsen, Casper Delft University of TechnologyNetherlands Hefty Algebras for Higher-Order Algebraic Operations Committee Member in Program Committee within the PEPM-track
Chris BaileyBailey, Chris University of IllinoisUnited States Committee Member in Program Committee within the ProLaLa-track
Alan BakerBaker, Alan Google Taking Back Control in an Intermediate Representation for GPU Computing
Musard BalliuBalliu, Musard KTH Royal Institute of TechnologySweden Committee Member in Program Committee within the PriSC-track
Stephanie BalzerBalzer, Stephanie Carnegie Mellon UniversityUnited States Higher-Order Leak and Deadlock Free Locks Committee Member in Program Committee within the POPL -track
Sébastien BardinBardin, Sébastien CEA LIST, University Paris-SaclayFrance 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 Univ Rennes, IRISAFrance Formally Verified Native Code Generation in an Effectful JIT - or: Turning the CompCert backend into a formally verified JIT compiler
Gilles BartheBarthe, Gilles MPI-SP, Germany / IMDEA Software Institute, Spain 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 Co-chair in Program Committee within the ProLaLa-track
Kevin BatzBatz, Kevin RWTH Aachen University 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 University 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
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 Technische Universität KaiserslauternGermany 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 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
Roberto BlancoBlanco, Roberto Max Planck Institute for Security and Privacy (MPI-SP) SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability Machine
Sandrine BlazyBlazy, Sandrine Univ Rennes, IRISAFrance Formally Verified Native Code Generation in an Effectful JIT - or: Turning the CompCert backend into a formally verified JIT compiler
Rastislav BodikBodik, Rastislav Google Research Grisette: Symbolic Compilation as a Functional Programming Library
Ronny BoganiBogani, Ronny University of Edinburgh Formalising Criminal Law in Catala
Filippo BonchiBonchi, Filippo University of Pisa Deconstructing the Calculus of Relations with Tape Diagrams
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
Matt BowersBowers, Matt MIT-CSAILUnited 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 PC Chair in Organizing Committee within the PEPM-track
Joachim BreitnerBreitner, Joachim Epic Games Germany Committee Member in Program Committee within the PADL-track
David BromanBroman, David KTH Royal Institute of TechnologySweden Statically Resolvable Ambiguity
Fraser BrownBrown, Fraser Stanford University, USA FaJITa: Verifying Optimizations on Just-In-Time Programs Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers
Matteo BusiBusi, Matteo Università di Pisa - Dipartimento di InformaticaItaly 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 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 Under Approximation for Efficient Programming-by-Example
Marco CampionCampion, Marco University of VeronaItaly Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
David CaoCao, David University of California, San Diego babble: Learning Better Abstractions with E-Graphs and Anti-Unification
Qinxiang CaoCao, Qinxiang Shanghai Jiao Tong UniversityChina Committee Member in Program Committee within the CoqPL-track
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 University, SwedenSweden Statically Resolvable Ambiguity
Simon CastellanCastellan, Simon INRIA The Geometry of Causality : Multi-Token Geometry of Interaction and its Causal Unfolding
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
Ethan CecchettiCecchetti, Ethan University of Maryland, College ParkUnited States Committee Member in Program Committee within the PriSC-track
Tej ChajedChajed, Tej VMware ResearchUnited States 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 ENS de Lyon Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
Arthur CharguéraudCharguéraud, Arthur InriaFrance A High-Level Separation Logic for Heap Space under Garbage Collection Committee Member in Program Committee within the POPL -track
Swarat ChaudhuriChaudhuri, Swarat University of Texas at AustinUnited States Neurosymbolic Programming
Qiaochu ChenChen, Qiaochu University of Texas at AustinUnited States Committee Member in Artifact Evaluation Committee within the VMCAI-track
Yanju ChenChen, Yanju University of California at Santa BarbaraUnited States Committee Member in Artifact Evaluation Committee within the VMCAI-track
Yixuan ChenChen, Yixuan Yale University, USA A Compositional Theory of Linearizability
Zilin ChenChen, Zilin UNSW SydneyAustralia Dargent: A Silver Bullet for Data Layout Refinement
Adam ChlipalaChlipala, Adam Massachusetts Institute of TechnologyUnited States Committee Member in Steering Committee within the CPP-track
Hangyeol ChoCho, Hangyeol Hanyang University Inductive Synthesis of Recursive Functional Programs with Trace-based Pruning
Minki ChoCho, Minki Seoul National UniversitySouth Korea Conditional Contextual Refinement
Stephen ChongChong, Stephen Harvard UniversityUnited States From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems Invited Speaker in Speakers within the PLMW @ POPL-track
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 CNRS & Université Aix-MarseilleFrance 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
Youyou CongCong, Youyou Tokyo Institute of TechnologyJapan Committee Member in Selection Committee within the POPL Student Research Competition-track
Arthur CorrensonCorrenson, Arthur École Normale Supérieure de Rennes & Saarland University What do Hyper 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
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 University 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
Ugo Dal LagoDal Lago, Ugo University of Bologna; InriaItaly 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 Amazon Probabilistic Resource-Aware Session Types
Ria DasDas, Ria Massachusetts Institute of Technology Combining Functional and Automata Synthesis to Discover Causal Reactive Programs
Swaraj DashDash, Swaraj University of Oxford 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 University On the Expressive Power of String Constraints
Leonardo de Mourade Moura, Leonardo Microsoft ResearchUnited States Committee Member in Program Committee within the CPP-track
Shaleen DeepDeep, Shaleen Microsoft The Fine-Grained Complexity of CFL Reachability
Benjamin DelawareDelaware, Benjamin Purdue UniversityUnited States Diversity, Equity, and Inclusion Chair in Organizing Committee for POPL 2023 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
Aidan DenlingerDenlinger, Aidan University of California, San Diego 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
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 Bologna Elements of Quantitative Rewriting
Alessandro Di GiorgioDi Giorgio, Alessandro University of Pisa Deconstructing the Calculus of Relations with Tape Diagrams
Cinzia Di GiustoDi Giusto, Cinzia Laboratoire I3S A non-sequential hierarchy of message-passing models
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
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
Alastair F. DonaldsonDonaldson, Alastair F. Imperial College LondonUnited Kingdom Taking Back Control in an Intermediate Representation for GPU Computing Committee Member in Program Committee within the POPL -track
Rui DongDong, Rui University of MichiganUnited States Committee Member in Artifact Evaluation Committee within the VMCAI-track
Derek DreyerDreyer, Derek MPI-SWSGermany Conditional Contextual Refinement DimSum: A Decentralized Approach to Multi-language Semantics and Verification
Cezara DrăgoiDrăgoi, Cezara Inria / ENS / Informal Systems Committee Member in Program Committee within the VMCAI-track Program Co-Chair in Organizing Committee within the VMCAI-track
Maxime DénèsDénès, Maxime INRIA Committee Member in Program Committee within the CoqPL-track
Emanuele D’OsualdoD’Osualdo, Emanuele MPI-SWSGermany The Path to Durable Linearizability DimSum: A Decentralized Approach to Multi-language Semantics and Verification
E Marco EilersEilers, Marco ETH ZurichSwitzerland Committee Member in Program Committee within the PriSC-track
Richard A. EisenbergEisenberg, Richard A. Jane StreetUnited States Committee Member in Program Committee within the POPL -track
Kevin EllisEllis, Kevin Cornell UniversityUnited States Top-Down Synthesis For Library Learning
Michael EmmiEmmi, Michael Amazon Web ServicesUnited States 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 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
Guilherme EspadaEspada, Guilherme LASIGE, Faculdade de Ciências, Universidade de LisboaPortugal Video Chair in Organizing Committee for POPL 2023
F Xiong FanFan, Xiong Rutgers University A Core Calculus for Equational Proofs of Cryptographic Protocols
Azadeh FarzanFarzan, Azadeh University of TorontoCanada Stratified Commutativity in Verification Algorithms for Concurrent Programs
Xinyu FengFeng, Xinyu Nanjing UniversityChina Committee Member in Program Committee within the CPP-track
Jerome FeretFeret, Jerome INRIA ParisFrance Committee Member in Program Committee within the VMCAI-track
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, CNRS, I3S A non-sequential hierarchy of message-passing models
Jean-Christophe FilliatreFilliatre, Jean-Christophe CNRSFrance Committee Member in Program Committee within the VMCAI-track
Robby FindlerFindler, Robby Northwestern UniversityUnited States 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
Denis FirsovFirsov, Denis Tallinn University of TechnologyEstonia Committee Member in Program Committee within the CPP-track
Riccardo FocardiFocardi, Riccardo University Ca' Foscari, Venice Automated Learning and Verification of Embedded Security Architectures
Yannick ForsterForster, Yannick InriaFrance Committee Member in Program Committee within the CPP-track
Cameron FreerFreer, Cameron Massachusetts Institute of TechnologyUnited States Steering Committee Member in Steering Committee within the LAFI-track
Roy FrostigFrostig, Roy Google Research You Only Linearize Once: Tangents Transpose to Gradients
Peng FuFu, Peng Dalhousie University Proto-Quipper with dynamic lifting
G Letterio GallettaGalletta, Letterio IMT School for Advanced Studies LuccaItaly Committee Member in Program Committee within the PriSC-track
Moses GanardiGanardi, Moses Max Planck Institute for Software Systems (MPI-SWS) Context-Bounded Verification of Context-Free Specifications
Joshua GancherGancher, Joshua Cornell University Universally Composable Security for Program Partitioning A Core Calculus for Equational Proofs of Cryptographic Protocols
Vijay GaneshGanesh, Vijay University of WaterlooCanada On the Expressive Power of String Constraints
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
Francesco GavazzoGavazzo, Francesco University of Pisa Elements of Quantitative Rewriting
Martin GebserGebser, Martin University of Klagenfurt, AustriaAustria 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
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 Committee Member in Program Committee within the PADL-track
Anitha GollamudiGollamudi, Anitha University of Massachusetts Lowell MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code Committee Member in Program Committee within the PriSC-track
Hannah GommerstadtGommerstadt, Hannah Vassar College Committee Member in Organizing Committee within the PLMW @ POPL-track
Sergey GoncharovGoncharov, Sergey FAU Erlangen-Nürnberg, Lehrstuhl 8Germany 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
Gabriel GrandGrand, Gabriel MIT Top-Down Synthesis For Library Learning
Michael GreenbergGreenberg, Michael Stevens Institute of TechnologyUnited States From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems Committee Member in Program Committee within the POPL -track Committee Member in Organizing Committee within the PLMW @ POPL-track
Nathan GrewalGrewal, Nathan University of Waterloo On the Expressive Power of String Constraints
James GrimmelmannGrimmelmann, James Cornell University The Structure and Legal Interpretation of Computer Programs Committee Member in Program Committee within the ProLaLa-track
Yu GuGu, Yu University of Tsukuba Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification Optimal CHC Solving via Termination Proofs
Marco GuarnieriGuarnieri, Marco IMDEA Software InstituteSpain Co-chair in Program Committee within the PriSC-track Committee Member in Steering Committee within the PriSC-track
Giulio GuerrieriGuerrieri, Giulio Huawei Edinburgh Research CentreUnited Kingdom Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework
Sumit GulwaniGulwani, Sumit MicrosoftUnited States Under Approximation for Efficient Programming-by-Example
Elsa GunterGunter, Elsa University of IllinoisUnited States Committee Member in Program Committee within the CPP-track
Gopal GuptaGupta, Gopal University of Texas at Dallas, USA Building Information Modeling Using Constraint Logic Programming (Extended Abstract) Committee Member in Program Committee within the PADL-track
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 Inria & Université de Lorraine A general noninterference policy for polynomial time
Ákos HajduHajdu, Ákos MetaUnited Kingdom Committee Member in Program Committee within the VMCAI-track
Philipp HallerHaller, Philipp KTHSweden Statically Resolvable Ambiguity
Michael HanusHanus, Michael Kiel UniversityGermany Co-chair in Program Committee within the PADL-track Co-chair in Programme Chairs within the PADL-track
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
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
Ludovic HenrioHenrio, Ludovic CNRSFrance 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
Scott HermanHerman, Scott Conan & Herman Formalising Criminal Law in Catala
Michael HicksHicks, Michael Amazon and University of MarylandUnited 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
Thomas T. HildebrandtHildebrandt, Thomas T. University of CopenhagenDenmark DCR Graphs as Co-created Executable Models of the Law
Andrew K. HirschHirsch, Andrew K. University at Buffalo, SUNYUnited States 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 Co-chair in Organizing Committee within the LAFI-track
Kuen-Bang Hou (Favonia)Hou (Favonia), Kuen-Bang University of MinnesotaUnited States An Order-Theoretic Analysis of Universe Polymorphism Committee Member in Organizing Committee within the PLMW @ POPL-track
Cătălin HriţcuHriţcu, Cătălin MPI-SPGermany SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability Machine Securely Compiling F* Programs With IO and Then Linking Them Against Weakly-Typed Interfaces Steering Committee Chair in Steering Committee within the CPP-track Steering Committee Chair in Steering Committee within the PriSC-track
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 The University of Hong Kong 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 The University of Iowa A Type-Based Approach to Divide-And-Conquer Recursion in Coq
Sebastian HuntHunt, Sebastian City, University of London Reconciling Shannon and Scott with a Lattice of Computable Information
Mathieu HuotHuot, Mathieu Oxford University ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs
Chung-Kil HurHur, Chung-Kil Seoul National UniversitySouth Korea Conditional Contextual Refinement
I Atsushi IgarashiIgarashi, Atsushi Kyoto University, JapanJapan Committee Member in Program Committee within the PEPM-track
Daniela InclezanInclezan, Daniela Miami UniversityUnited States 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
J Vincent JacksonJackson, Vincent University of Melbourne Dargent: A Silver Bullet for Data Layout Refinement
Jules JacobsJacobs, Jules Radboud University Higher-Order Leak and Deadlock Free Locks Fast Coalgebraic Bisimilarity Minimization
Suresh JagannathanJagannathan, Suresh Purdue UniversityUnited States Committee Member in Program Committee within the POPL -track
Junyoung JangJang, Junyoung McGill UniversityCanada Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Tomi JanhunenJanhunen, Tomi Tampere UniversityFinland Committee Member in Program Committee within the PADL-track
Alan JeffreyJeffrey, Alan RobloxUnited States Committee Member in Program Committee within the POPL -track
Christa JenkinsJenkins, Christa The University of Iowa A Type-Based Approach to Divide-And-Conquer Recursion in Coq
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
Chuan JiangJiang, Chuan Purdue University Comparative Synthesis: Learning Near-Optimal Network Designs by Query
Jerome JochemsJochems, Jerome University of Bristol 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 DiegoUnited States FaJITa: Verifying Optimizations on Just-In-Time Programs
Matthew JohnsonJohnson, Matthew Google BrainUnited 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 MPI-SWSGermany Committee Member in Program Committee within the POPL -track
K Younesse KaddarKaddar, Younesse University of Oxford, UKUnited Kingdom Affine monads and lazy structures for Bayesian programming
Pankaj Kumar KalitaKalita, Pankaj Kumar IIT KanpurIndia Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Konstantinos KallasKallas, Konstantinos University of Pennsylvania Student Volunteer Co-Chair in Organizing Committee for POPL 2023 Executing Microservice Applications on Serverless, Correctly
Yukiyoshi KameyamaKameyama, Yukiyoshi University of TsukubaJapan 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 and University College LondonGermany A Calculus for Amortized Expected Runtimes Deductive Verification of Probabilistic Programs
Ohad KammarKammar, Ohad University of EdinburghUnited Kingdom Committee Member in Program Committee within the POPL -track Steering Committee Member in Steering Committee within the LAFI-track
Jeehoon KangKang, Jeehoon KAISTSouth Korea Student Research Competition Co-Chair in Organizing Committee for POPL 2023 Co-chair in Selection Committee within the POPL Student Research Competition-track
Joost-Pieter KatoenKatoen, Joost-Pieter RWTH Aachen UniversityGermany A Calculus for Amortized Expected Runtimes Deductive Verification of Probabilistic Programs Committee Member in Program Committee within the POPL -track
Ryan KavanaghKavanagh, Ryan McGill UniversityCanada Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
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 Data Layout Refinement
Axel KerinecKerinec, Axel Université Sorbonne Paris Nord Why are proofs relevant in proof-relevant models?
Marie KerjeanKerjean, Marie CNRS, Université Sorbonne Paris NordFrance Committee Member in Program Committee within the CPP-track
Delia KesnerKesner, Delia Université de Paris; 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
Alan KhojaKhoja, Alan University of Konstanz Formal Modeling and Analysis of Legal Contracts using ContractCheck
Jinwoo KimKim, Jinwoo University of Wisconsin-Madison Unrealizability Logic
Yoonseung KimKim, Yoonseung Yale UniversityUnited States 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 University, USA When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic
Kohei KishidaKishida, Kohei University of Illinois Urbana-Champaign Proto-Quipper with dynamic lifting
Gerwin KleinKlein, Gerwin CSIRO's Data61 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
Dominik KlumppKlumpp, Dominik University of FreiburgGermany Stratified Commutativity in Verification Algorithms for Concurrent Programs
Naoki KobayashiKobayashi, Naoki University of Tokyo, JapanJapan HFL(Z) Validity Checking for Automated Program Verification
Nicolas KohKoh, Nicolas Princeton University When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic
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 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
Eric KoskinenKoskinen, Eric Stevens Institute of TechnologyUnited States Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification An algebra of alignment for relational verification
Paraschos KoutrisKoutris, Paraschos University of Wisconsin-Madison, USA The Fine-Grained Complexity of CFL Reachability
Laura KovacsKovacs, Laura Vienna University of Technology (TU Wien)Austria Committee Member in Program Committee within the POPL -track
Faustyna KrawiecKrawiec, Faustyna University of CambridgeUnited Kingdom Committee Member in Program Committee within the LAFI-track
Robbert KrebbersKrebbers, Robbert Radboud University NijmegenNetherlands 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
Neel KrishnaswamiKrishnaswami, Neel University of CambridgeUnited Kingdom 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, San Diego babble: Learning Better Abstractions with E-Graphs and Anti-Unification
Lindsey KuperKuper, Lindsey University of California at Santa Cruz 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 Cambridge Dargent: A Silver Bullet for Data Layout Refinement
Ori LahavLahav, Ori Tel Aviv UniversityIsrael Kater: Automating Weak Memory Model Metatheory and Consistency Checking An Operational Approach to Library Abstraction under Relaxed Memory Concurrency
Akash LalLal, Akash Microsoft Research Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the VMCAI-track
Leonidas LampropoulosLampropoulos, Leonidas University of Maryland, College ParkGreece Artifact Evaluation Co-Chair in Organizing Committee for POPL 2023 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 pi_RA: A pi-calculus for verifying protocols that use remote attestation
Cosimo LaneveLaneve, Cosimo University of Bologna Legal Contracts Amending in Stipula
Laetitia LaversaLaversa, Laetitia Université Côte d'Azur, CNRS, I3S A non-sequential hierarchy of message-passing 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 Technology An algebra of alignment for relational verification
Vu LeLe, Vu MicrosoftUnited States Under Approximation for Efficient Programming-by-Example
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 Recursive Functional Programs with Trace-based Pruning
Daan LeijenLeijen, Daan Microsoft ResearchUnited States Tail Recursion Modulo Context -- An Equational Approach
Matthieu LemerreLemerre, Matthieu CEA LIST, FranceFrance 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 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
Alexander K. LewLew, Alexander K. Massachusetts Institute of Technology, USAUnited States ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs Committee Member in Program Committee within the LAFI-track
Jianlin LiLi, Jianlin University of Waterloo Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortized Probabilistic Inference
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, UKChina Formalising Criminal Law in Catala
Zixuan LiLi, Zixuan Purdue University 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
Dan LicataLicata, Dan Wesleyan UniversityUnited States Committee Member in Program Committee within the POPL -track
Anthony Widjaja LinLin, Anthony Widjaja TU Kaiserslautern; MPI-SWSGermany Committee Member in Program Committee within the VMCAI-track
Junyi LiuLiu, Junyi State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China CoqQ: Foundational Verification of Quantum Programs
Vincent LiuLiu, Vincent University of Pennsylvania Executing Microservice Applications on Serverless, Correctly
Anton LorenzenLorenzen, Anton University of Edinburgh Tail Recursion Modulo Context -- An Equational Approach
Etienne LozesLozes, Etienne Université Côte d'Azur, CNRS, I3S A non-sequential hierarchy of message-passing 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
Sterre LutzLutz, Sterre Utrecht University and TNO Deontic Paradoxes in Library Lending Regulations: A Case Study in Flint
M Dougal MaclaurinMaclaurin, Dougal Google Research You Only Linearize Once: Tangents Transpose to Gradients
Matteo MaffeiMaffei, Matteo TU Wien Committee Member in Program Committee within the POPL -track
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
Rupak MajumdarMajumdar, Rupak MPI-SWSGermany Context-Bounded Verification of Context-Free Specifications
Dhruv C. MakwanaMakwana, Dhruv C. University of Cambridge CN: Verifying systems C code with separation-logic refinement types
Florin ManeaManea, Florin University of Göttingen 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 K. MansinghkaMansinghka, Vikash K. MIT ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs
Giulio ManzonettoManzonetto, Giulio Université Sorbonne Paris Nord Why are proofs relevant in proof-relevant models?
Daniel MarshallMarshall, Daniel University of Kent, UKUnited Kingdom Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Chris MartensMartens, Chris North Carolina State UniversityUnited States Exploring Consequences of Privacy Policies with Narrative Generation via Answer Set Programming Invited Speaker in Speakers within the PLMW @ POPL-track
Isabella MastroeniMastroeni, Isabella University of Verona, ItalyItaly Committee Member in Program Committee within the POPL -track
Christoph MathejaMatheja, Christoph Technical University of DenmarkDenmark A Calculus for Amortized Expected Runtimes Deductive Verification of Probabilistic Programs Committee Member in Program Committee within the POPL -track
Umang MathurMathur, Umang National University of SingaporeSingapore Dynamic Race Detection With O(1) Samples Committee Member in Program Committee within the POPL -track
McKenna McCallMcCall, McKenna Carnegie Mellon UniversityUnited States Committee Member in Program Committee within the PriSC-track
Craig McLaughlinMcLaughlin, Craig UNSW Sydney Dargent: A Silver Bullet for Data Layout Refinement
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
Denis MerigouxMerigoux, Denis INRIAFrance Experience report: implementing a real-world, medium-sized program derived from a legislative specification 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 Washington, SeattleUnited States MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
Kristopher MicinskiMicinski, Kristopher Syracuse UniversityUnited States Publicity Chair in Organizing Committee for POPL 2023
Stefan MiliusMilius, Stefan Friedrich-Alexander-Universität Erlangen-Nürnberg 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 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
Alexandre MoineMoine, Alexandre InriaFrance A High-Level Separation Logic for Heap Space under Garbage Collection
Shouvick MondalMondal, Shouvick Concordia University, Montreal, CanadaCanada Committee Member in Artifact Evaluation Committee within the VMCAI-track
J. Garrett MorrisMorris, J. Garrett The University of IowaUnited States A Type-Based Approach to Divide-And-Conquer Recursion in Coq
Jason MorrisMorris, Jason Service Canada, Lexpedite Legal Technology Blawx: User-friendly Goal-Directed Answer Set Programming for Rules as Code
Greg MorrisettMorrisett, Greg Cornell TechUnited States A Core Calculus for Equational Proofs of Cryptographic Protocols
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 Minnesota An Order-Theoretic Analysis of Universe Polymorphism
Andrzej MurawskiMurawski, Andrzej University of OxfordUnited Kingdom Committee Member in Program Committee within the POPL -track
Suha Orhun MutluergilMutluergil, Suha Orhun IRIF, France / University Paris Diderot, France / CNRS, France 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 C. MyersMyers, Andrew C. Cornell University General Chair in Organizing Committee for POPL 2023 Universally Composable Security for Program Partitioning
N 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 Technology 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 Certora, inc.United 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
David NaumannNaumann, David Stevens Institute of Technology 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
David NetoNeto, David GoogleCanada Taking Back Control in an Intermediate Representation for GPU Computing
Minh NgoNgo, Minh Stevens Institute of Technology An algebra of alignment for relational verification
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
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 Data Layout Refinement
William O'HanleyO'Hanley, William Stanford CodeX 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. MIT Top-Down Synthesis For Library Learning
Federico OlimpieriOlimpieri, Federico University of Leeds Why are proofs relevant in proof-relevant models?
Arthur Oliveira ValeOliveira Vale, Arthur Yale University A Compositional Theory of Linearizability
Bruno C. d. S. OliveiraOliveira, Bruno C. d. S. University of Hong KongChina Recursive Subtyping for All 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⋈
Dominic OrchardOrchard, Dominic University of Kent, UKUnited Kingdom Committee Member in Program Committee within the POPL -track
Klaus OstermannOstermann, Klaus University of Tübingen Committee Member in Program Committee within the POPL -track
P Oded PadonPadon, Oded VMware ResearchUnited States Committee Member in Program Committee within the POPL -track
Michele PaganiPagani, Michele IRIF - Université de Paris CitéFrance Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the LAFI-track
Viktor PalmkvistPalmkvist, Viktor KTHSweden Statically Resolvable Ambiguity
Jens PalsbergPalsberg, Jens University of California at Los AngelesUnited States PC Chair in Organizing Committee within the PEPM-track
Hugo PaquetPaquet, Hugo University of Oxford 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
Gennaro ParlatoParlato, Gennaro University of Molise Committee Member in Program Committee within the VMCAI-track
Bryan ParnoParno, Bryan Carnegie Mellon University, USA 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 ResearchGermany You Only Linearize Once: Tangents Transpose to Gradients
Marco PatrignaniPatrignani, Marco University of TrentoItaly Robust Constant-Time Cryptography Blame-Preserving Secure Compilation 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 Microsoft Corporation Under Approximation for Efficient Programming-by-Example
Simona PerriPerri, Simona University of Calabria, Italy Committee Member in Program Committee within the PADL-track
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
David PichardiePichardie, David MetaFrance Formally Verified Native Code Generation in an Effectful JIT - or: Turning the CompCert backend into a formally verified JIT compiler Committee Member in Program Committee within the POPL -track
Brigitte PientkaPientka, Brigitte McGill UniversityCanada 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
Benjamin C. PiercePierce, Benjamin C. University of PennsylvaniaUnited States 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
Clément Pit-ClaudelPit-Claudel, Clément EPFL / AWSUnited States 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 PittsPitts, Andrew University of CambridgeUnited Kingdom Locally Nameless Sets
Gordon PlotkinPlotkin, Gordon Google Committee Member in Program Committee within the LAFI-track
Andreas PodelskiPodelski, Andreas University of Freiburg, GermanyGermany 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 babble: Learning Better Abstractions with E-Graphs and Anti-Unification 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 Admissible Types-To-PERs Relativization in Higher-Order Logic Isabelle/HOL: Foundations, Induction, and Coinduction 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
Jonathan ProtzenkoProtzenko, Jonathan Microsoft Research, RedmondUnited States 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 Cambridge, UK CN: Verifying systems C code with separation-logic refinement types Committee Member in Program Committee within the POPL -track
Romain PéchouxPéchoux, Romain INRIA / LORIAFrance A general noninterference policy for polynomial time
Pierre-Marie PédrotPédrot, Pierre-Marie INRIAFrance 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 University, USA 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 The Path to Durable Linearizability Incorrectness Logic and Under-approximation: Foundations of Bug Catching Committee Member in Program Committee within the POPL -track
Arjun RadhakrishnaRadhakrishna, Arjun MicrosoftUnited States Under Approximation for Efficient Programming-by-Example
Alexey RadulRadul, Alexey Google Research 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 Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
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 University Comparative Synthesis: Learning Near-Optimal Network Designs by Query
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
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 Committee Member in Steering Committee within the PriSC-track
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 Committee Member in Program Committee within the CoqPL-track
Nick RiouxRioux, Nick University of Pennsylvania A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈
Xavier RivalRival, Xavier INRIA/CNRS/ENS ParisFrance Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference
Christine RizkallahRizkallah, Christine University of MelbourneAustralia Dargent: A Silver Bullet for Data Layout Refinement Committee Member in Program Committee within the CPP-track Committee Member in Program Committee within the CoqPL-track
Neil Julien RossRoss, Neil Julien Dalhousie UniversityCanada Proto-Quipper with dynamic lifting
Cody RouxRoux, Cody AWSUnited States Committee Member in Program Committee within the CPP-track
Sukyoung RyuRyu, Sukyoung KAISTSouth Korea Committee Member in Program Committee within the PEPM-track
S Amr SabrySabry, Amr Indiana UniversityUnited States Committee Member in Program Committee within the POPL -track
Kazuhiko SakaguchiSakaguchi, Kazuhiko InriaFrance Committee Member in Program Committee within the CPP-track
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 ChalmersSweden Reconciling Shannon and Scott with a Lattice of Computable Information
Alessio SantamariaSantamaria, Alessio University of Pisa, University of Sussex Deconstructing the Calculus of Relations with Tape Diagrams
Giovanni SartorSartor, Giovanni University of BolognaItaly Legal Contracts Amending in Stipula
Ryosuke SatoSato, Ryosuke University of Tokyo, JapanJapan HFL(Z) Validity Checking for Automated Program Verification
Burkhard SchaferSchafer, Burkhard University of Edinburgh Formalising Criminal Law in Catala
Sven-Bodo ScholzScholz, Sven-Bodo Radboud UniversityNetherlands Committee Member in Program Committee within the PEPM-track
Tom SchrijversSchrijvers, Tom KU LeuvenBelgium Committee Member in Program Committee within the PADL-track
Daniel Schwartz-NarbonneSchwartz-Narbonne, Daniel Amazon, n.n. Committee Member in Program Committee within the VMCAI-track
Lutz SchöderSchöder, Lutz FAU Erlangen-Nürnberg, Lehrstuhl 8 Towards a Higher-Order Mathematical Operational Semantics
Atharva SehgalSehgal, Atharva University of Texas, AustinUnited States Neurosymbolic Programming
Taro SekiyamaSekiyama, Taro National Institute of InformaticsJapan Temporal Verification with Answer-Effect Modification Committee Member in Program Committee within the POPL -track
Peter SelingerSelinger, Peter Dalhousie University Proto-Quipper with dynamic lifting
Eli SenneshSennesh, Eli Northeastern UniversityUnited States 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 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
Zhong ShaoShao, Zhong Yale UniversityUnited States A Compositional Theory of Linearizability Committee Member in Steering Committee within the CPP-track
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
Elaine ShiShi, Elaine CMU A Core Calculus for Equational Proofs of Cryptographic Protocols
Pengyuan ShiShi, Pengyuan University of Waterloo 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
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 University Towards an Automatic Consolidation of French Law
Giovanni SilenoSileno, Giovanni University of Amsterdam Committee Member in Program Committee within the ProLaLa-track
Lucas SilverSilver, Lucas University of PennsylvaniaUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Clint SimonSimon, Clint Microsoft Under Approximation for Efficient Programming-by-Example
Abhishek Kr SinghSingh, Abhishek Kr Tata Institute of Fundamental Research MumbaiIndia 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
Michael SmithSmith, Michael UCSD FaJITa: Verifying Optimizations on Just-In-Time Programs Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers
Kristina SojakovaSojakova, Kristina INRIA ParisFrance A Core Calculus for Equational Proofs of Cryptographic Protocols
Armando Solar-LezamaSolar-Lezama, Armando Massachusetts Institute of Technology Top-Down Synthesis For Library Learning Combining Functional and Automata Synthesis to Discover Causal Reactive Programs
Youngju SongSong, Youngju Seoul National UniversitySouth Korea Conditional Contextual Refinement DimSum: A Decentralized Approach to Multi-language Semantics and Verification
Simon SpiesSpies, Simon MPI-SWS & Saarland UniversityGermany DimSum: A Decentralized Approach to Multi-language Semantics and Verification
Mandayam SrivasSrivas, Mandayam Chennai Mathematical Institute Committee Member in Program Committee within the VMCAI-track
Caleb StanfordStanford, Caleb University of California, Davis A Robust Theory of Series Parallel Graphs
Sam StatonStaton, Sam University of Oxford 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 Robust Constant-Time Cryptography Cachet: A Domain-Specific Language for Trustworthy Just-In-Time Compilers 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
J. Ryan StinnettStinnett, J. Ryan King's College LondonUnited Kingdom Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Pierre-Yves StrubStrub, Pierre-Yves MetaFrance 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 The University of Iowa, USAUnited 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
Eijiro SumiiSumii, Eijiro Tohoku UniversityJapan Committee Member in Program Committee within the POPL -track
Jennifer SunSun, Jennifer California Institute of TechnologyUnited States Neurosymbolic Programming
T Nicolas TabareauTabareau, Nicolas InriaFrance Impredicative Observational Equality Committee Member in Program Committee within the POPL -track
Kento TanahashiTanahashi, Kento The University of Tokyo 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 Committee Member in Program Committee within the POPL -track
Christine TassonTasson, Christine Sorbonne Université — LIP6France Co-chair in Organizing 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 Research Institute / Columbia University Combining Functional and Automata Synthesis to Discover Causal Reactive Programs
Joshua B. TenenbaumTenenbaum, Joshua B. MIT Top-Down Synthesis For Library Learning Combining Functional and Automata Synthesis to Discover Causal Reactive Programs
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 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
Abhishek TiwariTiwari, Abhishek University of Passau, GermanyGermany Committee Member in Artifact Evaluation Committee within the VMCAI-track
Ashish TiwariTiwari, Ashish MicrosoftUnited States Under Approximation for Efficient Programming-by-Example
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
Andrew TolmachTolmach, Andrew Portland State University SECOMP2CHERI: Securely Compiling Compartments from CompCert C to a Capability Machine Committee Member in Program Committee within the POPL -track
Emma ToschTosch, Emma University of Vermont Exploring Consequences of Privacy Policies with Narrative Generation via Answer Set Programming Committee Member in Program Committee within the ProLaLa-track
Dmitriy TraytelTraytel, Dmitriy University of CopenhagenDenmark Admissible Types-To-PERs Relativization in Higher-Order Logic Isabelle/HOL: Foundations, Induction, and Coinduction Conference Chair in Organizing 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 Friedrich-Alexander-Universität Erlangen-Nürnberg (FAU)Germany 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
Hünkar Can TunçTunç, Hünkar Can Aarhus UniversityDenmark Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
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 Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification Optimal CHC Solving via Termination Proofs
Josef UrbanUrban, Josef Czech Technical University in PragueCzech Republic Committee Member in Program Committee within the CPP-track
Henning UrbatUrbat, Henning Friedrich-Alexander-Universität Erlangen-Nürnberg Towards a Higher-Order Mathematical Operational Semantics
V Viktor VafeiadisVafeiadis, Viktor MPI-SWSGermany Kater: Automating Weak Memory Model Metatheory and Consistency Checking The Path to Durable Linearizability Committee Member in Program Committee within the CPP-track
Nachiappan ValliappanValliappan, Nachiappan Chalmers University of TechnologySweden Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Peter Van RoyVan Roy, Peter Université catholique de LouvainBelgium Committee Member in Program Committee within the PADL-track
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 Waterloo Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortized Probabilistic Inference
Abhinav VermaVerma, Abhinav The Pennsylvania State University Committee Member in Selection Committee within the POPL Student Research Competition-track
Lena VerschtVerscht, Lena RWTH Aachen University A Calculus for Amortized Expected Runtimes
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 University Efficient Dual-Numbers Reverse AD via Well-Known Program Transformations
W David WalkerWalker, David Princeton UniversityUnited States Committee Member in Program Committee within the POPL -track
Di WangWang, Di Carnegie Mellon UniversityUnited States 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 Purdue University, USA 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
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
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
Theo WinterhalterWinterhalter, Theo 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
Jenna Wise (DiVincenzo)Wise (DiVincenzo), Jenna Carnegie Mellon UniversityUnited States Committee Member in Program Committee within the PriSC-track
Thorsten WissmannWissmann, Thorsten Radboud University Fast Coalgebraic Bisimilarity Minimization
Catherine WongWong, Catherine Massachusetts Institute of TechnologyUnited States Top-Down Synthesis For Library Learning
Meng Weng WongWong, Meng Weng Singapore Management UniversitySingapore Defeasible Semantics for L4
Tobias WrigstadWrigstad, Tobias Uppsala University, SwedenSweden RUST: Regions, Uniqueness, Ownership & Types
X Anxhelo XhebrajXhebraj, Anxhelo Purdue UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Ningning XieXie, Ningning Google Brain / University of TorontoUnited Kingdom Committee Member in Program Committee within the POPL -track Committee Member in Program Committee within the PADL-track
Han XuXu, Han Peking University Making a Type Difference: Subtraction on Intersection Types as Generalized Record Operations
Y Hongseok YangYang, Hongseok KAISTSouth Korea Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference
Mingsheng YingYing, Mingsheng University of Technology Sydney / Institute of Software at Chinese Academy of Sciences / Tsinghua University CoqQ: Foundational Verification of Quantum Programs
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
yisong yueyue, yisong Caltech Neurosymbolic Programming
Z Yannick ZakowskiZakowski, Yannick InriaFrance Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
Francesco Zappa NardelliZappa Nardelli, Francesco MetaFrance Committee Member in Program Committee within the POPL -track
Steve ZdancewicZdancewic, Steve University of PennsylvaniaUnited States Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈ 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 Co-chair in Selection Committee within the POPL Student Research Competition-track
Haoran ZhangZhang, Haoran University of Pennsylvania 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 Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear Programming Witnessability of Undecidable Problems
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
Li ZhouZhou, Li Max Planck Institute for Security and Privacy CoqQ: Foundational Verification of Quantum Programs
Litao ZhouZhou, Litao The 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 (582)

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia