POPL 2018 Contributors

Filter

Role Type

Contributing to

Number of Roles

Country

Results (699)

A Andreas AbelAbel, Andreas Gothenburg University Decidability of Conversion for Type Theory in Type Theory Decidability of Conversion for Type Theory in Type Theory
Ittai AbrahamAbraham, Ittai VMWare Research Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
Sara AchourAchour, Sara MITUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Weronika T. AdrianAdrian, Weronika T. Navigating Online Semantic Resources for Entity Set Expansion
Reynald AffeldtAffeldt, Reynald National Institute of Advanced Industrial Science and Technology (AIST), Japan Committee Member in Program Committee within the CPP -track
Sheshansh AgrawalAgrawal, Sheshansh IIT Bombay Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs
Danel AhmanAhman, Danel Inria ParisEstonia Handling fibred algebraic effects Recalling a Witness: Foundations and Applications of Monotonic State Recalling a Witness: Foundations and Applications of Monotonic State
Amal AhmedAhmed, Amal Northeastern University, USAUnited States Session Chair of Session 1 (part of PriSC) On Compositional Compiler Correctness and Fully Abstract Compilation Correctness of Speculative Optimizations with Dynamic Deoptimization Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible Committee Member in Program Committee within the PriSC-track Organizer in Organizing Committee within the PriSC-track
Alex AikenAiken, Alex Stanford University Challenges in the Design and Compilation of Programming Languages for Exascale Machines (Invited Talk) On Automatically Proving the Correctness of math.h Implementations
Mahmudul Faisal Al AmeenAl Ameen, Mahmudul Faisal National University of Singapore A Logical System for Modular Information Flow Verification
Aws AlbarghouthiAlbarghouthi, Aws University of Wisconsin-Madison Panel I: Technical Trends in Programming Languages Research Synthesizing Coupling Proofs of Differential Privacy Committee Member in Panelists within the PLMW-track
Jonathan AldrichAldrich, Jonathan Carnegie Mellon UniversityUnited States Gradual Program Verification
Jade AlglaveAlglave, Jade University College LondonFrance Committee Member in Program Committee within the VMCAI-track
Thorsten AltenkirchAltenkirch, Thorsten University of Nottingham Session Chair of Types (part of POPL Research Papers) Session Chair of Type Theory, Set Theory, and Formalized Mathematics (part of CPP ) Committee Member in Program Committee within the POPL Research Papers-track
Sidney AmaniAmani, Sidney UNSW, Australia Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
Nada AminAmin, Nada University of CambridgeUnited Kingdom Collapsing Towers of Interpreters Collapsing Towers of Interpreters Committee Member in Programme Committee within the PEPM-track Committee Member in Program Committee within the POPL Research Papers-track
Benjamin AminofAminof, Benjamin Vienna University of Technology Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction
Shengwei AnAn, Shengwei Robust Example-based Synthesis
Abhishek AnandAnand, Abhishek Cornell UniversityUnited States Revisiting Parametricity: Inductives and Uniformity of Propositions Typed Template Coq
Kritika AnandAnand, Kritika An Automated Detection of Inconsistencies in SBVR-based Business Rules using Many-sorted Logic
June AndronickAndronick, June Data61,CSIRO (formerly NICTA) and UNSWAustralia Session Chair of Invited Talk by René Thiemann (part of CPP ) Program Co-Chair in Program Committee within the CPP -track
Carlo AngiuliAngiuli, Carlo Carnegie Mellon University Computational Higher Type Theory
Andrew W. AppelAppel, Andrew W. Princeton Committee Member in Program Committee within the CoqPL-track
Alasdair ArmstrongArmstrong, Alasdair Brunel University On abstraction and compositionality for weak-memory linearisability
Kenichi AsaiAsai, Kenichi Ochanomizu UniversityJapan Session Chair of Session 1-2 (part of PEPM) Selective CPS Transformation for Shift and Reset Steering Committee Chair in Steering Committee within the PEPM-track
Robert AtkeyAtkey, Robert University of Strathclyde General Chair in Organizing Committee within the Off the Beaten Track-track
Mahdi AzarafroozAzarafrooz, Mahdi Cylance Deep Amortized Inference for Probabilistic Programs using Adversarial Compilation
Arthur Azevedo de AmorimAzevedo de Amorim, Arthur Carnegie Mellon University, USAUnited States Formally Secure Compilation of Unsafe Low-Level Components Short talk: The Meaning of Memory Safety
B Giorgio BacciBacci, Giorgio Aalborg University Comparing the speed of probabilistic processes
Casper Bach PoulsenBach Poulsen, Casper Delft University of Technology Intrinsically-Typed Definitional Interpreters Intrinsically-Typed Definitional Interpreters for Imperative Languages
Johannes BaderBader, Johannes MicrosoftUnited States Gradual Program Verification
Thomas BallBall, Thomas Microsoft ResearchUnited States Panel II: Life in Grad School (and Beyond) Committee Member in Panelists within the PLMW-track
Sorav BansalBansal, Sorav Automatic Verification of Intermittent Systems
Wenlei BaoBao, Wenlei Ohio State UniversityUnited States Analytical Modeling of Cache Behavior for Affine Programs
Joachim BardBard, Joachim Saarland University, Germany Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq
Gilles BartheBarthe, Gilles IMDEA Software Institute Proving Expected Sensitivity of Probabilistic Programs Proving expected sensitivity of probabilistic programs Monadic refinements for relational cost analysis Committee Member in Program Committee within the POPL Research Papers-track
Mark BattyBatty, Mark University of KentUnited Kingdom Committee Member in Program Committee within the POPL Research Papers-track
Cedric BaumannBaumann, Cedric ETH Zurich Automatic Verification of RMA Programs via Abstraction Extrapolation
Andrew BedfordBedford, Andrew Laval UniversityCanada Coqatoo: Generating Natural Language Versions of Coq Proofs Generating Information-Flow Control Mechanisms from Programming Language Specifications
Lennart BeringerBeringer, Lennart Princeton UniversityUnited States Committee Member in Program Committee within the CPP -track
Jean-Philippe BernardyBernardy, Jean-Philippe University of Gothenburg Linear Haskell: practical linearity in a higher-order polymorphic language Linear Haskell: practical linearity in a higher-order polymorphic language
Yves BertotBertot, Yves INRIAFrance Session Chair of Keynote (part of CoqPL) Session with the Coq Development Team Programme Co-Chair in Organizing Committee within the CoqPL-track Programme Co-Chair in Program Committee within the CoqPL-track
Jan BessaiBessai, Jan Technical University Dortmund Towards Language-independent Code Synthesis (Poster/Demo Talk)
Aggelos BiboudisBiboudis, Aggelos Ecole Polytechnique Federale de LausanneSwitzerland Simplicitly: Foundations and Applications of Implicit Function Types Simplicitly: Foundations and Applications of Implicit Function Types
Florian BiermannBiermann, Florian IT University of CopenhagenDenmark Rewriting High-Level Spreadsheet Structures into Higher-Order Functional Programs
Dariusz BiernackiBiernacki, Dariusz University of Wrocław A Coq Formalization of Normalization by Evaluation for Martin-Löf Type Theory Handle with Care: Relational Interpretation of Algebraic Effects and Handlers Handle with Care: Relational Interpretation of Algebraic Effects and Handlers
Fabrizio BiondiBiondi, Fabrizio CentraleSupelec Rennes Scalable Approximation of Quantitative Information Flow in Programs
Lars BirkedalBirkedal, Lars Aarhus University Session Chair of Probability (part of POPL Research Papers) Session Chair of Outside the box (part of POPL Research Papers) Session Chair of Session 3 (part of PriSC) Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST Committee Member in Program Committee within the PriSC-track Committee Member in Program Committee within the POPL Research Papers-track
Aleš BizjakBizjak, Aleš Aarhus UniversityDenmark Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Jasmin BlanchetteBlanchette, Jasmin Vrije Universiteit AmsterdamNetherlands A Verified SAT Solver with Watched Literals Using Imperative HOL Committee Member in Program Committee within the CPP -track
Olivier BlanvillainBlanvillain, Olivier EPFL Simplicitly: Foundations and Applications of Implicit Function Types Simplicitly: Foundations and Applications of Implicit Function Types
Sandrine BlazyBlazy, Sandrine IRISA, University of Rennes 1France Committee Member in Program Committee within the CPP -track
Roderick BloemBloem, Roderick Institute of Software Technology, Graz University of Technology Committee Member in Program Committee within the VMCAI-track
Martin BodinBodin, Martin CMM A Coq Formalisation of a Core of R
Rastislav BodíkBodík, Rastislav University of Washington Committee Member in Steering Committee for POPL 2018 Bonsai: Synthesis-Based Reasoning for Type Systems Bonsai: Synthesis-Based Reasoning for Type Systems
Mathieu BoespflugBoespflug, Mathieu Tweag I/O Linear Haskell: practical linearity in a higher-order polymorphic language Linear Haskell: practical linearity in a higher-order polymorphic language
Sylvie BoldoBoldo, Sylvie Inria and Université Paris-SaclayFrance Committee Member in Program Committee within the CPP -track
Maria Paola BonacinaBonacina, Maria Paola University of Verona, Italy Proofs in Conflict-Driven Theory Combination
Johannes BorgströmBorgström, Johannes Uppsala University, SwedenSweden Committee Member in Program Committee within the PPS-track
Maksym BortinBortin, Maksym Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
Simon BoulierBoulier, Simon Typed Template Coq
Austin BourgerieBourgerie, Austin University of Maryland Refinement Types for Ruby
William J. BowmanBowman, William J. Northeastern University, USAUnited States Short talk: Dependently Typed Assembly for Secure Linking Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible
Jason BreckBreck, Jason University of Wisconsin - Madison Non-Linear Reasoning For Invariant Synthesis Non-Linear Reasoning For Invariant Synthesis
Joachim BreitnerBreitner, Joachim University of PennsylvaniaUnited States Total Haskell is Reasonable Coq Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Eugene BrevdoBrevdo, Eugene Google TensorFlow Distributions
David BromanBroman, David KTH Royal Institute of TechnologySweden Gradually Typed Symbolic Expressions Combining static and dynamic optimizations using closed-form solutions
Matt BrownBrown, Matt UCLA Typed and Jones Optimal Self-Applicable Partial Evaluation Jones-Optimal Partial Evaluation by Specialization-Safe Normalization
Roberto BruniBruni, Roberto Dipartimento di Informatica, Universita' di Pisa Code Obfuscation Against Abstract Model Checking Attacks
Toby Cathcart BurnBurn, Toby Cathcart University of Oxford Higher-Order Constrained Horn Clauses for Verification Higher-Order Constrained Horn Clauses for Verification
Samuele BuroBuro, Samuele Università degli Studi di Verona Abstract Code Injection - A Semantic Approach Based on Abstract Non-Interference
Javier BurroniBurroni, Javier Interactive Writing and Debugging of Bayesian Probabilistic Programs
Eric ButlerButler, Eric University of Washington A Framework for Computer-Aided Design of Educational Domain Models
William E. ByrdByrd, William E. University of Alabama at Birmingham, USAUnited States Session Chair of Session 2 (part of Off the Beaten Track) One Weird Trick: Relational Interpreters for Program Synthesis. Committee Member in Program Committee within the Off the Beaten Track-track
Myriam BégelBégel, Myriam ENS Paris-Saclay, France Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
C Yufei CaiCai, Yufei University of Tuebingen Denotational validation of higher-order Bayesian inference
Francesco CalimeriCalimeri, Francesco University of Calabria LoIDE: a a web-based IDE for Logic Programming - Preliminary Report Optimizing Answer Set Computation via Heuristic-Based Decomposition
John Peter CamporaCampora, John Peter ULL Lafayette Migrating Gradual Types Migrating Gradual Types
Marco CaniniCanini, Marco KAUST Wrap Up Organizing Committee in Organizing Committee within the NetPL-track
Paolo CapriottiCapriotti, Paolo University of Nottingham Univalent Higher Categories via Complete Semi-Segal Types Univalent Higher Categories via Complete Semi-Segal Types
Michael CarbinCarbin, Michael MITUnited States Constructive probabilistic semantics with non-spatial locales
Bob CarpenterCarpenter, Bob Columbia University Committee Member in Program Committee within the PPS-track
Calin CascavalCascaval, Calin Barefoot Networks P4: A Language for Data Plane Programming
Giuseppe CastagnaCastagna, Giuseppe CNRS, France / University of Paris Diderot, FranceItaly Chair in Steering Committee for POPL 2018
Gelsomina CatalanoCatalano, Gelsomina A REST-based Development Framework for ASP: Tools and Application
Sunjay CauligiCauligi, Sunjay UCSD Constant-time WebAssembly
Pavol CernyCerny, Pavol University of Colorado BoulderSlovakia Committee Member in Program Committee within the POPL Research Papers-track
Marek ChalupaChalupa, Marek Masaryk University Data-centric Dynamic Partial Order Reduction
Kartik ChandraChandra, Kartik Stanford UniversityUnited States Bonsai: Synthesis-Based Reasoning for Type Systems Bonsai: Synthesis-Based Reasoning for Type Systems
Stephen ChangChang, Stephen Northeastern University Symbolic Types for Lenient Symbolic Execution Symbolic Types for Lenient Symbolic Execution
Krishnendu ChatterjeeChatterjee, Krishnendu IST Austria Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs Optimal Dyck Reachability for Data-dependence and Alias Analysis Optimal Dyck Reachability for Data-dependence and Alias Analysis Data-centric Dynamic Partial Order Reduction Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs
Kaustuv ChaudhuriChaudhuri, Kaustuv Inria, FranceFrance A Two-Level Logic Perspective on (Simultaneous) Substitutions
Sheng ChenChen, Sheng University of Louisiana at LafayetteUnited States Migrating Gradual Types Migrating Gradual Types
Taolue ChenChen, Taolue Birkbeck, University of London What's Decidable About String Constraints with ReplaceAll Function?
Yan ChenChen, Yan State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences & University of Chinese Academy of Sciences What's Decidable About String Constraints with ReplaceAll Function?
James CheneyCheney, James University of Edinburgh, UKUnited States Committee Member in Program Committee within the POPL Research Papers-track Committee Member in Program Committee within the CPP -track
Annie CherkaevCherkaev, Annie University of Utah SweetPea: A Language for Designing Experiments
Shigeru ChibaChiba, Shigeru University of Tokyo, JapanJapan Committee Member in Programme Committee within the PEPM-track
Wei-Ngan ChinChin, Wei-Ngan National University of Singapore Session Chair of Potpourri (part of VMCAI) A Logical System for Modular Information Flow Verification Automated Lemma Synthesis in Symbolic-Heap Separation Logic Automated Lemma Synthesis in Symbolic-Heap Separation Logic Committee Member in Program Committee within the VMCAI-track
Pavan Kumar ChittimalliChittimalli, Pavan Kumar An Automated Detection of Inconsistencies in SBVR-based Business Rules using Many-sorted Logic
Bhavya ChoudharyChoudhary, Bhavya IIT Bombay Optimal Dyck Reachability for Data-dependence and Alias Analysis Optimal Dyck Reachability for Data-dependence and Alias Analysis
Vikraman ChoudhuryChoudhury, Vikraman Refinement Reflection: Complete Verification with SMT Refinement Reflection: Complete Verification with SMT
Maria ChristakisChristakis, Maria MPI-SWSGermany Committee Member in Program Committee within the VMCAI-track
Jan ChristiansenChristiansen, Jan Flensburg University of Applied Sciences, Germany Probabilistic Functional Logic Programming
Luke ChurchChurch, Luke Committee Member in Program Committee within the Off the Beaten Track-track
Stefan CiobacaCiobaca, Stefan Alexandru Ioan Cuza University of Iasi Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Koen ClaessenClaessen, Koen Chalmers University of Technology Committee Member in Program Committee within the POPL Research Papers-track
Pierre ClairambaultClairambault, Pierre CNRS & ENS Lyon Linearity in Higher-Order Recursion Schemes
Andrew CobbCobb, Andrew Northeastern University Contextual Equivalence for a Probabilistic Language with Continuous Random Variables and Recursion
Michael CoblenzCoblenz, Michael Carnegie Mellon UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Jonathan CohenCohen, Jonathan Princeton University SweetPea: A Language for Designing Experiments
Youyou CongCong, Youyou Ochanomizu University, JapanJapan Combining Control Operators and Dependent Types Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible
William CookCook, William University of Texas at Austin Verifying Equivalence of Database-Driven Applications Committee Member in Program Committee within the POPL Research Papers-track
Patrick CousotCousot, Patrick Session Chair of Abstract Interpretation (part of VMCAI) Committee Member in Program Committee within the VMCAI-track
Karl CraryCrary, Karl Carnegie Mellon University Session Chair of Dependent Types (part of POPL Research Papers) Hygienic Source-Code Generation Using Functors Committee Member in Program Committee within the POPL Research Papers-track
Santiago CuellarCuellar, Santiago PrincetonColombia Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Ryan CulpepperCulpepper, Ryan Northeastern University Contextual Equivalence for a Probabilistic Language with Continuous Random Variables and Recursion
Marco Cusumano-TownerCusumano-Towner, Marco MIT-CSAIL Using probabilistic programs as proposals
John CyphertCyphert, John University of Wisconsin - Madison Non-Linear Reasoning For Invariant Synthesis Non-Linear Reasoning For Invariant Synthesis
Lukasz CzajkaCzajka, Lukasz University of Innsbruck CoqHammer: Strong Automation for Program Verification
D Loris D'AntoniD'Antoni, Loris University of Wisconsin–MadisonItaly Committee Member in Program Committee within the POPL Research Papers-track
Vijay D'SilvaD'Silva, Vijay Google Secure Compilation in a Production Environment
Pierre-Evariste DagandDagand, Pierre-Evariste LIP6/CNRS France Foundations of Dependent Interoperability
Manjeet DahiyaDahiya, Manjeet Automatic Verification of Intermittent Systems
Mila Dalla PredaDalla Preda, Mila University of Verona, Italy Committee Member in Program Committee within the POPL Research Papers-track
Andrei Marian DanDan, Andrei Marian ETH ZurichSwitzerland Automatic Verification of RMA Programs via Abstraction Extrapolation
Nils Anders DanielssonDanielsson, Nils Anders University of Gothenburg, Chalmers University of Technology Up-to Techniques Using Sized Types Up-to Techniques Using Sized Types
Olivier DanvyDanvy, Olivier Yale-NUS College, Singapore Committee Member in Programme Committee within the PEPM-track
Marcus Rodrigues de Araújode Araújo, Marcus Rodrigues UFMG Inference of Static Semantics for Incomplete C Programs Inference of Static Semantics for Incomplete C Programs
Will DeaconDeacon, Will ARM Ltd. Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8 Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8
Benjamin DelawareDelaware, Benjamin Purdue University Student Research Competition Chair in Organizing Committee for POPL 2018 Session Chair of Tactics and Proof Engineering (part of CoqPL) Towards Context-Aware Data Refinement SRC Awards Student Research Competition Chair in Selection Committee within the POPL Student Research Competition-track Committee Member in Program Committee within the CoqPL-track
Dominique DevrieseDevriese, Dominique KU LeuvenBelgium Session Chair of Short Talks Session (part of PriSC) Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities Linear capabilities for modular fully-abstract compilation of verified code Parametricity versus the Universal Type Committee Member in Program Committee within the PriSC-track Organizer in Organizing Committee within the PriSC-track
Işıl DilligDillig, Işıl UT Austin Session Chair of Program Analysis II (part of POPL Research Papers) Session Chair of Invited Talk by Ranjit Jhala (part of VMCAI) Session Chair of Invited Talk by Azadeh Farzan (part of VMCAI) Program Synthesis using Abstraction Refinement Verifying Equivalence of Database-Driven Applications Program Co-Chair in Program Committee within the VMCAI-track Co-chair in Organizing Committee within the VMCAI-track Committee Member in Program Committee within the POPL Research Papers-track
Joshua V. DillonDillon, Joshua V. Google TensorFlow Distributions
Jose DivasónDivasón, Jose Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
Boris DjalalDjalal, Boris INRIA A Constructive Formalisation of Semi-algebraic Sets and Functions
Christian DoczkalDoczkal, Christian CNRS, France Completeness and Decidability of Converse PDL in the Constructive Type Theory of Coq
Brijesh DongolDongol, Brijesh Brunel University London On abstraction and compositionality for weak-memory linearisability Transactions in Relaxed Memory Architectures
Wensheng DouDou, Wensheng Institute of Software, Chinese Academy of Sciences, ChinaChina Rewriting High-Level Spreadsheet Structures into Higher-Order Functional Programs
Derek DreyerDreyer, Derek MPI-SWS How to Give Talks That People Can Follow Milner Award Lecture: The Type Soundness Theorem That You Really Want to Prove (and Now You Can) RustBelt: Securing the Foundations of the Rust Programming Language RustBelt: Securing the Foundations of the Rust Programming Language Committee Member in Speakers within the PLMW-track
Sophia DrossopoulouDrossopoulou, Sophia Committee Member in Program Committee within the POPL Research Papers-track
Catherine DuboisDubois, Catherine ENSIIE Paris-Evry Keynote: Programming and proving with FoCaLiZe: a tour from computer algebra to interoperability applications
Dominic DugganDuggan, Dominic Dataflow Metaprogramming (Poster/Demo Talk)
Sandra DylusDylus, Sandra University of Kiel, GermanyGermany Probabilistic Functional Logic Programming
Maxime DénèsDénès, Maxime INRIA Session with the Coq Development Team
Boris DüdderDüdder, Boris University of Copenhagen Towards Language-independent Code Synthesis (Poster/Demo Talk)
E Harley D. Eades IIIEades III, Harley D. Augusta University Explaining Type Errors
Thomas EhrhardEhrhard, Thomas CNRS and University Paris Diderot Stable, measurable functions and probabilistic programs Measurable cones and stable, measurable functions
Richard A. EisenbergEisenberg, Richard A. Bryn Mawr College, USAUnited States Explaining Type Errors
Conal ElliottElliott, Conal Target, USAUnited States The Simple Essence of Automatic Differentiation (Invited Talk)
Michael EmmiEmmi, Michael Nokia Bell Labs Sound, Complete, and Tractable Linearizability Monitoring for Concurrent Collections
Constantin EneaEnea, Constantin Université Paris DiderotFrance Session Chair of Termination (part of POPL Research Papers) Panel I: Technical Trends in Programming Languages Research Sound, Complete, and Tractable Linearizability Monitoring for Concurrent Collections Committee Member in Panelists within the PLMW-track Committee Member in Program Committee within the POPL Research Papers-track
Mike EnescuEnescu, Mike INRIA Scalable Approximation of Quantitative Information Flow in Programs
Martin ErwigErwig, Martin Oregon State UniversityUnited States Migrating Gradual Types Migrating Gradual Types Committee Member in Steering Committee within the PEPM-track
Thomas EspitauEspitau, Thomas Universite Pierre et Marie Curie Proving Expected Sensitivity of Probabilistic Programs Proving expected sensitivity of probabilistic programs
Patrick EugsterEugster, Patrick Purdue University Co-Design and Verification of an Available File System
Ana Nora EvansEvans, Ana Nora University of Virginia, USAUnited States Formally Secure Compilation of Unsafe Low-Level Components Software Fault Isolation for Robust Compilation
F Guglielmo FachiniFachini, Guglielmo Inria Paris Formally Secure Compilation of Unsafe Low-Level Components
Azadeh FarzanFarzan, Azadeh University of TorontoCanada Session Chair of Memory and Concurrency (part of POPL Research Papers) Panel II: Life in Grad School (and Beyond) Rethinking Compositionality for Concurrent Program Proofs Strategy Synthesis for Linear Arithmetic Games Strategy Synthesis for Linear Arithmetic Games Invited Speaker in Invited Speakers within the VMCAI-track Committee Member in Panelists within the PLMW-track Committee Member in Program Committee within the POPL Research Papers-track
Stefan FehrenbachFehrenbach, Stefan University of Edinburgh Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Marco A. FeliuFeliu, Marco A. National Institute of Aerospace An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs
Amy FeltyFelty, Amy University of OttawaCanada Session Chair of Invited Talk by Brigitte Pientka (part of CPP ) Program Co-Chair in Program Committee within the CPP -track
Xinyu FengFeng, Xinyu University of Science and Technology of ChinaChina Session Chair of Consistency (part of POPL Research Papers) Progress of Concurrent Objects with Partial Methods Committee Member in Program Committee within the CoqPL-track Committee Member in Program Committee within the POPL Research Papers-track
Yu FengFeng, Yu University of Texas at Austin, USAChina Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Tomas FiedorFiedor, Tomas VUT Brno From Shapes to Amortized Complexity
Nathanaël FijalkowFijalkow, Nathanaël Alan Turing Institute Comparing the speed of probabilistic processes
Denis FirsovFirsov, Denis University of Iowa, USA Generic Derivation of Induction for Impredicative Encodings in Cedille
Kathleen FisherFisher, Kathleen Tufts UniversityUnited States Synthesizing Bijective Lenses Synthesizing Bijective Lenses
Matthew FlattFlatt, Matthew University of UtahUnited States SweetPea: A Language for Designing Experiments
Mathias FleuryFleury, Mathias MPI-INFGermany A Verified SAT Solver with Watched Literals Using Imperative HOL Programming and Reasoning with Infinite Data in Isabelle/HOL.
Shaked FlurFlur, Shaked University of Cambridge Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8 Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8
Olivier FlückigerFlückiger, Olivier Northeastern University, USA Correctness of Speculative Optimizations with Dynamic Deoptimization
Jeffrey S. FosterFoster, Jeffrey S. University of Maryland, College ParkUnited States Session Chair of Verification (part of VMCAI) Refinement Types for Ruby
Nate FosterFoster, Nate Cornell UniversityUnited States Wrap Up Panel Probabilistic Program Equivalence for NetKAT Organizing Committee in Organizing Committee within the NetPL-track
Cédric FournetFournet, Cédric Microsoft Research Building Secure SGX Enclaves using F*, C/C++ and X64 A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations Recalling a Witness: Foundations and Applications of Monotonic State Recalling a Witness: Foundations and Applications of Monotonic State Committee Member in Program Committee within the PriSC-track
Cameron FreerFreer, Cameron Remine and BorelianUnited States Session Chair of SESSION III (invited tutorial + 1 talk) (part of PPS) Co-chair in Program Committee within the PPS-track
Jon FrenchFrench, Jon University of Cambridge Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8 Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8
Dan FruminFrumin, Dan Radboud University A calculus for logical refinements in separation logic Finite Sets in Homotopy Type Theory
Davide FuscàFuscà, Davide Optimizing Answer Set Computation via Heuristic-Based Decomposition
Hugo FéréeFérée, Hugo University of Kent, UKUnited Kingdom Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
G Marco GaboardiGaboardi, Marco University at Buffalo, SUNYUnited States Associated Events Chair in Organizing Committee for POPL 2018 Probabilistic Programming for Robotics Monadic refinements for relational cost analysis Organizing Chair in Organizers within the POPL TutorialFest-track Committee Member in Selection Committee within the POPL Workshops-track
Ronald GarciaGarcia, Ronald University of British Columbia Committee Member in Programme Committee within the PEPM-track
Philippa GardnerGardner, Philippa Imperial College London JaVerT: JavaScript Verification using Separation Logic JaVerT: JavaScript Verification Toolchain
Deepak GargGarg, Deepak Max Planck Institute for Software SystemsGermany Robust Hyperproperty Preservation for Secure Compilation Monadic refinements for relational cost analysis Committee Member in Program Committee within the PriSC-track Organizer in Organizing Committee within the PriSC-track
Simon J. GayGay, Simon J. University of Glasgow, UK Committee Member in Programme Committee within the PEPM-track
Paul GazzilloGazzillo, Paul Stevens Institute of TechnologyUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Stefano GermanoGermano, Stefano LoIDE: a a web-based IDE for Logic Programming - Preliminary Report
Herman GeuversGeuvers, Herman Radboud University Nijmegen, Netherlands Finite Sets in Homotopy Type Theory
Zoubin GhahramaniGhahramani, Zoubin University of Cambridge Denotational validation of higher-order Bayesian inference
Roberto GiacobazziGiacobazzi, Roberto University of Verona and IMDEA Software InstituteItaly Code Obfuscation Against Abstract Model Checking Attacks Code Obfuscation - A Hacking view on program analysis and understanding.
Theophilos GiannakopoulosGiannakopoulos, Theophilos BAE Systems, Inc. Contextual Equivalence for a Probabilistic Language with Continuous Random Variables and Recursion
Nick GiannarakisGiannarakis, Nick Princeton University Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Jeremy GibbonsGibbons, Jeremy Department of Computer Science, University of OxfordUnited Kingdom Committee Member in Steering Committee for POPL 2018
Andy GillGill, Andy University of Kansas, USA Committee Member in Programme Committee within the PEPM-track
Thomas GilrayGilray, Thomas University of Maryland Soft Contract Verification for Higher-order Stateful Programs Soft Contract Verification for Higher-order Stateful Programs
Klaus GleissenthallGleissenthall, Klaus University of California, San Diego Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Aviral GoelGoel, Aviral Northeastern UniversityUnited States Correctness of Speculative Optimizations with Dynamic Deoptimization
Guy Golan-GuetaGolan-Gueta, Guy Yahoo LabsUnited States Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
Anitha GollamudiGollamudi, Anitha Building Secure SGX Enclaves using F*, C/C++ and X64
Léon GondelmanGondelman, Léon LRI, Université Paris-Sud Finite Sets in Homotopy Type Theory
Laure GonnordGonnord, Laure University of Lyon & LIP, FranceFrance Committee Member in Program Committee within the VMCAI-track
Andrew D. GordonGordon, Andrew D. Microsoft Research and University of EdinburghUnited Kingdom Committee Member in Steering Committee for POPL 2018 Session Chair of SESSION I (invited talk) (part of PPS) SlicStan: Improving Probabilistic Programming using Information Flow Analysis Co-chair in Program Committee within the PPS-track
Colin GordonGordon, Colin Drexel UniversityUnited States Synthesizing Program-Specific Static Analyses
Roberta GoriGori, Roberta Dipartimento di Informatica, Universita' di Pisa Code Obfuscation Against Abstract Model Checking Attacks
Maria I. GorinovaGorinova, Maria I. The University of Edinburgh SlicStan: Improving Probabilistic Programming using Information Flow Analysis
Stéphane Graham-LengrandGraham-Lengrand, Stéphane CNRS, France Proofs in Conflict-Driven Theory Combination
Michael GreenbergGreenberg, Michael Pomona College Remote Participation Chair in Organizing Committee for POPL 2018 Session Chair of Keynote (part of Off the Beaten Track) Program Chair in Organizing Committee within the Off the Beaten Track-track
Ben GreenmanGreenman, Ben Northeastern UniversityUnited States On the Cost of Type-Tag Soundness
Benjamin GregoireGregoire, Benjamin INRIA Proving Expected Sensitivity of Probabilistic Programs Proving expected sensitivity of probabilistic programs
Charles GrelloisGrellois, Charles INRIA Sophia Antipolis & Aix-Marseille UniversitéFrance Linearity in Higher-Order Recursion Schemes
Radu GrigoreGrigore, Radu University of KentUnited Kingdom Maximum Satisfiability in Program Analysis: Applications and Techniques
Niklas GrimmGrimm, Niklas Vienna University of Technology, Austria A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Dan GrossmanGrossman, Dan University of WashingtonUnited States Adapting Proof Automation to Adapt Proofs Œuf: Minimizing the Coq Extraction TCB
Shelly GrossmanGrossman, Shelly Tel Aviv UniversityIsrael Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
Guy GuetaGueta, Guy VMWare Research Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
Arjun GuhaGuha, Arjun University of Massachusetts, Amherst Interactive Writing and Debugging of Bayesian Probabilistic Programs
Elsa GunterGunter, Elsa University of IllinoisUnited States Committee Member in Program Committee within the CPP -track
H Matthew HagueHague, Matthew Royal Holloway, University of London What's Decidable About String Constraints with ReplaceAll Function?
Stefan HallerstedeHallerstede, Stefan Three is a crowd: SAT, SMT and CLP on a chessboard
Matthew HammerHammer, Matthew University of Colorado, BoulderUnited States Committee Member in Selection Committee within the POPL Student Research Competition-track
Robert HarperHarper, Robert Carnegie Mellon UniversityUnited States Computational Higher Type Theory
Miran HasanagicHasanagic, Miran Three is a crowd: SAT, SMT and CLP on a chessboard
Kyle HeadleyHeadley, Kyle University of Colorado BoulderUnited States Simplifying incremental code with IODyn
George HeinemanHeineman, George Worcester Polytechnic Institute Towards Language-independent Code Synthesis (Poster/Demo Talk)
Fritz HengleinHenglein, Fritz DIKU, Denmark Session Chair of Session 2-1 (part of PEPM) POPL 2019 Preview Programme Co-Chair in Programme Committee within the PEPM-track
Hugo HerbelinHerbelin, Hugo INRIAFrance Committee Member in Program Committee within the CoqPL-track
Manuel HermenegildoHermenegildo, Manuel IMDEA Software Institute and T.U. of Madrid (UPM) Exploiting Term Hiding to Reduce Run-time Checking Overhead
Chris HeunenHeunen, Chris University of Edinburgh The semantic structure of quasi-Borel spaces: algebra, logic, and recursion Denotational validation of higher-order Bayesian inference
Annelie HeuserHeuser, Annelie CNRS/IRISA Scalable Approximation of Quantitative Information Flow in Programs
Michael HicksHicks, Michael University of Maryland, College ParkUnited States Committee Member in Steering Committee for POPL 2018 SIGPLAN Town Hall
Torsten HoeflerHoefler, Torsten ETH ZurichSwitzerland Automatic Verification of RMA Programs via Abstraction Extrapolation
Jochen HoenickeHoenicke, Jochen Universität FreiburgGermany Reducing Liveness to Safety in First-Order Logic Reducing Liveness to Safety in First-Order Logic
Matt HoffmanHoffman, Matt Google TensorFlow Distributions
Steven HoltzenHoltzen, Steven University of California, Los AngelesUnited States Probabilistic Program Inference With Abstractions
Lukáš HolíkHolík, Lukáš Brno University of Technology From Shapes to Amortized Complexity String Constraints with Concatenation and Transducers Solved Efficiently String Constraints with Concatenation and Transducers Solved Efficiently
Rudi HornHorn, Rudi University of Edinburgh Modelling Microcontroller Hardware using Typestate
Cătălin HriţcuHriţcu, Cătălin Inria Paris Artifact Evaluation Co-Chair in Organizing Committee for POPL 2018 Session Chair of Welcome and Invited Talk (part of PriSC) PriSC Welcome Formally Secure Compilation of Unsafe Low-Level Components Robust Hyperproperty Preservation for Secure Compilation Short talk: The Meaning of Memory Safety A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations Recalling a Witness: Foundations and Applications of Monotonic State Recalling a Witness: Foundations and Applications of Monotonic State Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Program Chair in Program Committee within the PriSC-track Organizer in Organizing Committee within the PriSC-track
Justin HsuHsu, Justin University College LondonUnited States Synthesizing Coupling Proofs of Differential Privacy Proving Expected Sensitivity of Probabilistic Programs Proving expected sensitivity of probabilistic programs
Zhenjiang HuHu, Zhenjiang National Institute of InformaticsJapan An Axiomatic Basis for Bidirectional Programming An Axiomatic Basis for Bidirectional Programming
Marieke HuismanHuisman, Marieke University of TwenteNetherlands Committee Member in Program Committee within the CPP -track
Andreas HumenbergerHumenberger, Andreas Vienna University of Technology Invariant Generation for Multi-Path Loops with Polynomial Assignments
Warren HuntHunt, Warren University of Texas AustinUnited States Committee Member in Program Committee within the CPP -track
Samuel HymHym, Samuel University of Lille, France Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
Reiner HähnleHähnle, Reiner Technical University of DarmstadtGermany Committee Member in Program Committee within the CPP -track
I Atsushi IgarashiIgarashi, Atsushi Kyoto University, JapanJapan Session Chair of Interpretation and Evaluation (part of POPL Research Papers) A Guess-and-Assume Approach to Loop Fusion for Program Verification Committee Member in Program Committee within the POPL Research Papers-track
Akifumi ImanishiImanishi, Akifumi Kyoto University Towards Proof Synthesis by Neural Machine Translation A Guess-and-Assume Approach to Loop Fusion for Program Verification
Jeevana Priya InalaInala, Jeevana Priya MIT WebRelate: Integrating Web Data with Spreadsheets using Examples WebRelate: Integrating Web Data with Spreadsheets using Examples
Shachar ItzhakyItzhaky, Shachar Technion, IsraelIsrael Abstraction-Based Interaction Model for Synthesis
Anastasia IzmaylovaIzmaylova, Anastasia Centrum Wiskunde & Informatica Committee Member in Programme Committee within the PEPM-track
J Swen JacobsJacobs, Swen Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity
Radha JagadeesanJagadeesan, Radha DePaul University On abstraction and compositionality for weak-memory linearisability Transactions in Relaxed Memory Architectures
Suresh JagannathanJagannathan, Suresh Purdue University Alone Together: Compositional Reasoning and Inference for Weak Isolation
Petr JankůJanků, Petr Brno University of Technology String Constraints with Concatenation and Transducers Solved Efficiently String Constraints with Concatenation and Transducers Solved Efficiently
Maximilian JaroschekJaroschek, Maximilian Vienna University of Technology Invariant Generation for Multi-Path Loops with Polynomial Assignments
Barry JayJay, Barry University of Technology Sydney Session Chair of Session 2-3 (part of PEPM) Recursive Programs in Normal Form (Short Paper)
David JensenJensen, David University of Massachusetts Amherst Interactive Writing and Debugging of Bayesian Probabilistic Programs
Johan JeuringJeuring, Johan Committee Member in Programme Committee within the PEPM-track
Ranjit JhalaJhala, Ranjit University of California, San DiegoUnited States General Chair in Organizing Committee for POPL 2018 Committee Member in Steering Committee for POPL 2018 Session Chair of Business Meeting (part of POPL Research Papers) Session Chair of Awards & Keynote-I (part of POPL Research Papers) Reasoning about Functions Chairs' Report Welcome to POPL 2018 Refinement Reflection: Complete Verification with SMT Refinement Reflection: Complete Verification with SMT Invited Speaker in Invited Speakers within the VMCAI-track Committee Member in Selection Committee within the POPL Workshops-track
Sebastiaan JoostenJoosten, Sebastiaan Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
Jacques-Henri JourdanJourdan, Jacques-Henri CNRS, LRI, Université Paris-SudFrance Iris - A Modular Foundation for Higher-Order Concurrent Separation Logic. RustBelt: Securing the Foundations of the Rust Programming Language RustBelt: Securing the Foundations of the Rust Programming Language
Dejan JovanovićJovanović, Dejan SRI InternationalUnited States Selfless Interpolation for Infinite-State Model Checking
Ralf JungJung, Ralf MPI-SWSGermany RustBelt: Securing the Foundations of the Rust Programming Language RustBelt: Securing the Foundations of the Rust Programming Language
K David KahnKahn, David Cornell University Probabilistic Program Equivalence for NetKAT
Jan-Oliver KaiserKaiser, Jan-Oliver MPI-SWS A “destruct” Tactic for Mtac2
Jonas KaiserKaiser, Jonas Binder Aware Recursion over Well-Scoped de Bruijn Syntax
Gowtham KakiKaki, Gowtham Purdue University Alone Together: Compositional Reasoning and Inference for Weak Isolation
Cezary KaliszykKaliszyk, Cezary University of Innsbruck CoqHammer: Strong Automation for Program Verification Formal Microeconomic Foundations and the First Welfare Theorem
Yukiyoshi KameyamaKameyama, Yukiyoshi University of Tsukuba, JapanJapan Program Generation for ML Modules (Short Paper)
Benjamin Lucien KaminskiKaminski, Benjamin Lucien RWTH Aachen University; University College London A new proof rule for almost-sure termination
Ohad KammarKammar, Ohad University of OxfordUnited Kingdom Partially Static Data as Free Extension of Algebras (Short Paper) The semantic structure of quasi-Borel spaces: algebra, logic, and recursion Denotational validation of higher-order Bayesian inference Committee Member in Program Committee within the PPS-track
Joost-Pieter KatoenKatoen, Joost-Pieter RWTH Aachen University A new proof rule for almost-sure termination
Peyman KazemianKazemian, Peyman Forward Networks Understand and verify your network using Header Space Analysis
Milod KazerounianKazerounian, Milod Refinement Types for Ruby
Chantal KellerKeller, Chantal LRI, Université Paris-SudFrance Committee Member in Program Committee within the CoqPL-track Committee Member in Program Committee within the Off the Beaten Track-track
Gabriele KellerKeller, Gabriele Data61,CSIRO (formerly NICTA) and UNSWAustralia Committee Member in Programme Committee within the PEPM-track
Siau-Cheng KhooKhoo, Siau-Cheng National University of Singapore Automated Lemma Synthesis in Symbolic-Heap Separation Logic Automated Lemma Synthesis in Symbolic-Heap Separation Logic
Steven KiddKidd, Steven Purdue University Towards Context-Aware Data Refinement
Zachary KincaidKincaid, Zachary Princeton UniversityUnited States Non-Linear Reasoning For Invariant Synthesis Non-Linear Reasoning For Invariant Synthesis Introduction to Algebraic Program analysis. Strategy Synthesis for Linear Arithmetic Games Strategy Synthesis for Linear Arithmetic Games Committee Member in Program Committee within the Off the Beaten Track-track
Johannes KinderKinder, Johannes Royal Holloway, University of London Checking Cryptographic API Usage with Composable Annotations (Short Paper)
Dominik KirstKirst, Dominik Saarland UniversityGermany Large Model Constructions for Second-Order ZF in Dependent Type Theory
Oleg KiselyovKiselyov, Oleg Committee Member in Programme Committee within the PEPM-track
Fredrik KjolstadKjolstad, Fredrik MIT CSAIL Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Alex KnauthKnauth, Alex Northeastern UniversityUnited States Symbolic Types for Lenient Symbolic Execution Symbolic Types for Lenient Symbolic Execution
Hsiang-Shang ‘Josh’ KoKo, Hsiang-Shang ‘Josh’ National Institute of Informatics, JapanTaiwan Session Chair of Session 1-1 (part of PEPM) An Axiomatic Basis for Bidirectional Programming An Axiomatic Basis for Bidirectional Programming Programme Co-Chair in Programme Committee within the PEPM-track
Christoph E. KochKoch, Christoph E. EPFL Unifying Analytic and Statically-Typed Quasiquotes Unifying Analytic and Statically-Typed Quasiquotes
Philipp KoernerKoerner, Philipp Three is a crowd: SAT, SMT and CLP on a chessboard
Michalis KokologiannakisKokologiannakis, Michalis National Technical University of Athens, GreeceGreece Effective Stateless Model Checking for C/C++ Concurrency Effective Stateless Model Checking for C/C++ Concurrency
Ekaterina KomendantskayaKomendantskaya, Ekaterina Heriot-Watt UniversityUnited Kingdom Committee Member in Program Committee within the CoqPL-track
Eric KoskinenKoskinen, Eric Stevens Institute of Technology Committee Member in Program Committee within the VMCAI-track
Laura KovacsKovacs, Laura Chalmers University of Technology Invariant Generation for Multi-Path Loops with Polynomial Assignments Committee Member in Program Committee within the VMCAI-track Committee Member in Program Committee within the POPL Research Papers-track
Dexter KozenKozen, Dexter Probabilistic Program Equivalence for NetKAT
Bernhard KraglKragl, Bernhard IST AustriaAustria Synchronous Proofs for Asynchronous Programs
Julian KranzKranz, Julian Technical University of Munich Modular Analysis of Executables using On-Demand Heyting Completion
Nicolai KrausKraus, Nicolai University of NottinghamUnited Kingdom Univalent Higher Categories via Complete Semi-Segal Types Univalent Higher Categories via Complete Semi-Segal Types
Anastasiya Kravchuk-KirilyukKravchuk-Kirilyuk, Anastasiya University of Pennsylvania Locally Nameless at Scale
Robbert KrebbersKrebbers, Robbert Delft University of TechnologyNetherlands A calculus for logical refinements in separation logic Intrinsically-Typed Definitional Interpreters Iris - A Modular Foundation for Higher-Order Concurrent Separation Logic. Intrinsically-Typed Definitional Interpreters for Imperative Languages RustBelt: Securing the Foundations of the Rust Programming Language RustBelt: Securing the Foundations of the Rust Programming Language
Sebastian KringsKrings, Sebastian Three is a crowd: SAT, SMT and CLP on a chessboard
Siddharth KrishnaKrishna, Siddharth New York UniversityUnited States Go with the Flow: Compositional Abstractions for Concurrent Data Structures
Sriram KrishnamoorthyKrishnamoorthy, Sriram Pacific Northwest National Laboratories Analytical Modeling of Cache Behavior for Affine Programs
Paddy KrishnanKrishnan, Paddy Committee Member in Program Committee within the VMCAI-track
Neel KrishnaswamiKrishnaswami, Neel Computer Laboratory, University of Cambridge Session Chair of Types and Effects (part of POPL Research Papers) Session Chair of Types for State (part of POPL Research Papers) Committee Member in Program Committee within the POPL Research Papers-track
Morten Krogh-JespersenKrogh-Jespersen, Morten Aarhus University A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST
Paul KrogmeierKrogmeier, Paul Purdue University Towards Context-Aware Data Refinement
Praveen KumarKumar, Praveen Cornell UniversityUnited States Probabilistic Program Equivalence for NetKAT
William KunkelKunkel, William Comparing Liquid Haskell and Coq: Evaluating the Great Expectations of “A Tale of Two Provers”
Ondřej KunčarKunčar, Ondřej Technische Universität München, Germany Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper) Safety and Conservativity of Definitions in HOL and Isabelle/HOL
L Giovanni LaboccettaLaboccetta, Giovanni A REST-based Development Framework for ASP: Tools and Application
Ralf LaemmelLaemmel, Ralf University of Koblenz-Landau, Germany Committee Member in Programme Committee within the PEPM-track
Ori LahavLahav, Ori Tel Aviv University, IsraelIsrael Effective Stateless Model Checking for C/C++ Concurrency Effective Stateless Model Checking for C/C++ Concurrency
Shuvendu K. LahiriLahiri, Shuvendu K. Microsoft Research Verifying Equivalence of Database-Driven Applications
Peter LammichLammich, Peter Technische Universität München A Verified SAT Solver with Watched Literals Using Imperative HOL
Leonidas LampropoulosLampropoulos, Leonidas University of PennsylvaniaGreece Generating Good Generators for Inductive Relations Generating Good Generators for Inductive Relations
Ian LangmoreLangmore, Ian Google TensorFlow Distributions
Kim LarsenLarsen, Kim Aalborg UniversityDenmark Comparing the speed of probabilistic processes
Théo LaurentLaurent, Théo Formally Secure Compilation of Unsafe Low-Level Components
Julia LawallLawall, Julia Inria/LIP6 Committee Member in Programme Committee within the PEPM-track
Sarah LawskyLawsky, Sarah Northwestern UniversityUnited States Formal Methods and the Law
Ton Chanh LeLe, Ton Chanh National University of SingaporeSingapore Automated Lemma Synthesis in Symbolic-Heap Separation Logic Automated Lemma Synthesis in Symbolic-Heap Separation Logic
Benedict LeeLee, Benedict National University of Singapore A Logical System for Modular Information Flow Verification
Wonyeol LeeLee, Wonyeol Stanford UniversityUnited States On Automatically Proving the Correctness of math.h Implementations
Axel LegayLegay, Axel Scalable Approximation of Quantitative Information Flow in Programs
K. Rustan M. LeinoLeino, K. Rustan M. AmazonUnited States Session Chair of Verified Applications (part of CPP ) Session Chair of Synthesis (part of VMCAI) Dafny Overview Committee Member in Speakers within the PLMW-track Committee Member in Program Committee within the CPP -track
Logan LelandLeland, Logan Snaarkl: Somewhat Practical, Pretty Much Declarative Verifiable Computing in Haskell
Sergueï LengletLenglet, Sergueï University of Lorraine, France HOpi in Coq
John LeoLeo, John Halfaya ResearchUnited States Adapting Proof Automation to Adapt Proofs
Sorin LernerLerner, Sorin University of California, San Diego Committee Member in Program Committee within the POPL Research Papers-track
Xavier LeroyLeroy, Xavier Inria Committee Member in Program Committee within the PriSC-track Committee Member in Program Committee within the POPL Research Papers-track
Michael LeuschelLeuschel, Michael University of Düsseldorf Three is a crowd: SAT, SMT and CLP on a chessboard
Ondřej LhotákLhoták, Ondřej University of Waterloo, Canada Committee Member in Program Committee within the VMCAI-track
Yangjia LiLi, Yangjia Institute of Software, Chinese Academy of Sciences Algorithmic Analysis of Termination Problems for Quantum Programs
Yong LiLi, Yong Institute of Software, Chinese Academy of Sciences Learning to Complement Büchi Automata
Hongjin LiangLiang, Hongjin University of Science and Technology of China Progress of Concurrent Objects with Partial Methods
Kevin LiaoLiao, Kevin How to Make Your Programs Very Safe: A Review of Practical Applications of Dependent Types
Anthony Widjaja LinLin, Anthony Widjaja Oxford UniversityUnited Kingdom What's Decidable About String Constraints with ReplaceAll Function? String Constraints with Concatenation and Transducers Solved Efficiently String Constraints with Concatenation and Transducers Solved Efficiently
Fengyun LiuLiu, Fengyun EPFL, SwitzerlandSwitzerland Simplicitly: Foundations and Applications of Implicit Function Types Simplicitly: Foundations and Applications of Implicit Function Types
Andreas LochbihlerLochbihler, Andreas Programming and Reasoning with Infinite Data in Isabelle/HOL.
Blake LoringLoring, Blake Checking Cryptographic API Usage with Composable Annotations (Short Paper)
Giuliano LosaLosa, Giuliano University of California at Los Angeles, USA Reducing Liveness to Safety in First-Order Logic Reducing Liveness to Safety in First-Order Logic
Daniel LundénLundén, Daniel KTH Royal Institute of TechnologySweden Combining static and dynamic optimizations using closed-form solutions
Christof LödingLöding, Christof RWTH Aachen University Foundations for Natural Proofs and Quantifier Instantiation Foundations for Natural Proofs and Quantifier Instantiation
M P. MadhusudanMadhusudan, P. University of Illinois at Urbana-ChampaignUnited States Foundations for Natural Proofs and Quantifier Instantiation Foundations for Natural Proofs and Quantifier Instantiation
Matteo MaffeiMaffei, Matteo Saarland University A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Stephen MagillMagill, Stephen Committee Member in Selection Committee within the POPL Student Research Competition-track
Assia MahboubiMahboubi, Assia INRIAFrance Committee Member in Program Committee within the CPP -track
Kenji MaillardMaillard, Kenji Inria Paris and ENS Paris A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations Recalling a Witness: Foundations and Applications of Monotonic State Recalling a Witness: Foundations and Applications of Monotonic State
Rupak MajumdarMajumdar, Rupak MPI-SWS Committee Member in Steering Committee for POPL 2018 Why is Random Testing Effective for Partition Tolerance Bugs?
Petar MaksimovićMaksimović, Petar Imperial College LondonUnited Kingdom JaVerT: JavaScript Verification using Separation Logic JaVerT: JavaScript Verification Toolchain
Cyprien ManginMangin, Cyprien Equations: From Clauses to Splittings to Functions (Poster/Demo Talk)
Marco MannaManna, Marco University of CalabriaItaly Navigating Online Semantic Resources for Entity Set Expansion Publicity and Web Chair in Publicity Chair within the PADL-track
Vikash MansinghkaMansinghka, Vikash Massachusetts Institute of Technology Using probabilistic programs as proposals
William ManskyMansky, William Princeton UniversityUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Radu MardareMardare, Radu Aalborg UniversityDenmark Comparing the speed of probabilistic processes Committee Member in Program Committee within the PPS-track
Ruben MartinsMartins, Ruben Carnegie Mellon UniversityPortugal Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Committee Member in Program Committee within the VMCAI-track
Isabella MastroeniMastroeni, Isabella University of Verona, ItalyItaly Abstract Code Injection - A Semantic Approach Based on Abstract Non-Interference
Micaela MayeroMayero, Micaela Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
Damiano MazzaMazza, Damiano CNRSFrance Polyadic Approximations, Fibrations and Intersection Types
Conor McBrideMcBride, Conor Committee Member in Program Committee within the POPL Research Papers-track
Jedidiah McClurgMcClurg, Jedidiah University of Colorado BoulderUnited States Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Annabelle McIverMcIver, Annabelle Macquarie University A new proof rule for almost-sure termination Committee Member in Program Committee within the PPS-track
James McKinnaMcKinna, James Triangulating Context Lemmas
Craig McLaughlinMcLaughlin, Craig The University of Edinburgh Triangulating Context Lemmas
Kenneth L. McMillanMcMillan, Kenneth L. Microsoft ResearchUnited States Session Chair of Model Checking (part of VMCAI) How to Stay Decidable P5: Planner-less Proofs of Probabilistic Parameterized Protocols Committee Member in Program Committee within the VMCAI-track Invited Speaker in Invited Speakers within the VMCAI-track
Kuldeep S. MeelMeel, Kuldeep S. National University of Singapore Scalable Approximation of Quantitative Information Flow in Programs
Erik MeijerMeijer, Erik Session Chair of SESSION II (3 talks) (part of PPS) Software is eating the world, but ML is going to eat software
Christopher MeiklejohnMeiklejohn, Christopher Université catholique de LouvainUnited States Towards A Systems Approach To Distributed Programming
Leandro T. C. MeloMelo, Leandro T. C. UFMG Inference of Static Semantics for Incomplete C Programs Inference of Static Semantics for Incomplete C Programs
Samuel MertenMerten, Samuel Snaarkl: Somewhat Practical, Pretty Much Declarative Verifiable Computing in Haskell
Yuri MeshmanMeshman, Yuri IMDEA Automatic Verification of RMA Programs via Abstraction Extrapolation
Mira MeziniMezini, Mira TU DarmstadtGermany Committee Member in Program Committee within the POPL Research Papers-track
Yan MichalevskyMichalevsky, Yan Stanford University Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
Jan MidtgaardMidtgaard, Jan University of Southern DenmarkDenmark Developments in Property-Based Testing (Invited Talk)
Zeina MigeedMigeed, Zeina University of California, Los Angeles On the Cost of Type-Tag Soundness
Matthew MightMight, Matthew University of Utah, USAUnited States Committee Member in Program Committee within the POPL Research Papers-track
Heather MillerMiller, Heather Ecole Polytechnique Federale de Lausanne Simplicitly: Foundations and Applications of Implicit Function Types Simplicitly: Foundations and Applications of Implicit Function Types Committee Member in Program Committee within the Off the Beaten Track-track
Todd MillsteinMillstein, Todd University of California, Los Angeles Wrap Up INVITED TALK: ``Safe'' Languages Require Sequential Consistency
Todd MillsteinMillstein, Todd University of California, Los Angeles Probabilistic Program Inference With Abstractions
Todd MillsteinMillstein, Todd University of California, Los Angeles Organizing Committee in Organizing Committee within the NetPL-track
Anders MiltnerMiltner, Anders Princeton University Synthesizing Bijective Lenses Synthesizing Bijective Lenses
Duncan MitchellMitchell, Duncan Royal Holloway, University of London Checking Cryptographic API Usage with Composable Annotations (Short Paper)
Andres Molina-MarkhamMolina-Markham, Andres The MITRE Corporation Probabilistic Models for Assured Position, Navigation and Timing
Alberto MomiglianoMomigliano, Alberto Università degli Studi di Milano Committee Member in Program Committee within the CPP -track
Dave MooreMoore, Dave Google TensorFlow Distributions
José MoralesMorales, José IMDEA Software Institute Exploiting Term Hiding to Reduce Run-time Checking Overhead
Carroll MorganMorgan, Carroll University of New South Wales; Data 61 A new proof rule for almost-sure termination
Greg MorrisettMorrisett, Greg Cornell University Revisiting Parametricity: Inductives and Uniformity of Propositions
Mariano MoscatoMoscato, Mariano National Institute of Aerospace An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs
Sean MossMoss, Sean University of Oxford The semantic structure of quasi-Borel spaces: algebra, logic, and recursion Denotational validation of higher-order Bayesian inference
Sergio MoverMover, Sergio University of Colorado Boulder Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Jean-Yves MoyenMoyen, Jean-Yves University of Copenhagen, Denmark Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
Eric MullenMullen, Eric University of Washington Œuf: Minimizing the Coq Extraction TCB
Cesar MunozMunoz, Cesar NASA An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs
Andrzej MurawskiMurawski, Andrzej University of OxfordUnited Kingdom Linearity in Higher-Order Recursion Schemes
Lawrence M. MurrayMurray, Lawrence M. Uppsala University Combining static and dynamic optimizations using closed-form solutions
Sebastian MusslickMusslick, Sebastian Princeton University SweetPea: A Language for Designing Experiments
Andrew MyersMyers, Andrew Cornell UniversityUnited States Program Chair in Organizing Committee for POPL 2018 Committee Member in Steering Committee for POPL 2018 Session Chair of Keynote-III (part of POPL Research Papers) Session Chair of Business Meeting (part of POPL Research Papers) Session Chair of Keynote-II (part of POPL Research Papers) Work-Life Balance? Panel I: Technical Trends in Programming Languages Research Chairs' Report Welcome to POPL 2018 Committee Member in Speakers within the PLMW-track Committee Member in Selection Committee within the POPL Workshops-track Program Chair in Program Committee within the POPL Research Papers-track
Magnus O. MyreenMyreen, Magnus O. Chalmers University of Technology, SwedenSweden Committee Member in Program Committee within the CPP -track
Peter MüllerMüller, Peter ETH ZurichSwitzerland Committee Member in Program Committee within the POPL Research Papers-track
N Kartik NagarNagar, Kartik Purdue University Alone Together: Compositional Reasoning and Inference for Weak Isolation
Santosh NagarakatteNagarakatte, Santosh Rutgers University, USAUnited States Session Chair of Testing and Verification (part of POPL Research Papers) Short talk: Compiler Optimizations with Retrofitting Transformations: Is there a Semantic Mismatch? Committee Member in Program Committee within the POPL Research Papers-track
Mayur NaikNaik, Mayur University of Pennsylvania Maximum Satisfiability in Program Analysis: Applications and Techniques Committee Member in Invited Tutorial within the VMCAI-track
Ravindra NaikNaik, Ravindra An Automated Detection of Inconsistencies in SBVR-based Business Rules using Many-sorted Logic
Mahsa NajafzadehNajafzadeh, Mahsa Purdue University Co-Design and Verification of an Available File System Alone Together: Compositional Reasoning and Inference for Weak Isolation
Aleksandar NanevskiNanevski, Aleksandar IMDEA Software InstituteSpain Committee Member in Program Committee within the POPL Research Papers-track
Nils NappNapp, Nils SUNY at Buffalo Probabilistic Programming for Robotics
Praveen NarayananNarayanan, Praveen Indiana University, USA More support for symbolic disintegration
Daiva NaudžiūnienėNaudžiūnienė, Daiva Imperial College London JaVerT: JavaScript Verification using Separation Logic JaVerT: JavaScript Verification Toolchain
David NaumannNaumann, David Stevens Institute of Technology Session Chair of Session 2 (part of PriSC) Committee Member in Program Committee within the PriSC-track
Daniel NeiderNeider, Daniel Max Planck Institute for Software SystemsGermany Committee Member in Program Committee within the VMCAI-track
Ryan R. NewtonNewton, Ryan R. Indiana UniversityUnited States Refinement Reflection: Complete Verification with SMT Refinement Reflection: Complete Verification with SMT Linear Haskell: practical linearity in a higher-order polymorphic language Linear Haskell: practical linearity in a higher-order polymorphic language
Thanh NguyenNguyen, Thanh Automatic Web Services Composition for Phylotastic
Phúc C. NguyễnNguyễn, Phúc C. University of Maryland Soft Contract Verification for Higher-order Stateful Programs Soft Contract Verification for Higher-order Stateful Programs
Olivier NicoleNicole, Olivier Modular Macros (Poster/Demo Talk)
Vivek NigamNigam, Vivek Federal University of Paraiba / fortissGermany Committee Member in Program Committee within the CPP -track
Filip NiksicNiksic, Filip MPI-SWSGermany Why is Random Testing Effective for Partition Tolerance Bugs?
Tobias NipkowNipkow, Tobias Technical University MunichGermany Committee Member in Program Committee within the CPP -track
Petr NovotnýNovotný, Petr IST AustriaAustria Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs
David NowakNowak, David CNRS, France Formal Proof of Polynomial-Time Complexity with Quasi-Interpretations
O Martin OderskyOdersky, Martin EPFL, SwitzerlandSwitzerland Simplicitly: Foundations and Applications of Implicit Function Types Simplicitly: Foundations and Applications of Implicit Function Types
C.-H. Luke OngOng, C.-H. Luke University of OxfordUnited Kingdom Game Semantics for Probabilistic Programs Higher-Order Constrained Horn Clauses for Verification Higher-Order Constrained Horn Clauses for Verification
Klaus OstermannOstermann, Klaus University of TuebingenGermany Denotational validation of higher-order Bayesian inference Committee Member in Program Committee within the POPL Research Papers-track
Divesh OtwaniOtwani, Divesh United States Finite Maps At The Type Level
P Oded PadonPadon, Oded Tel Aviv UniversityIsrael Reducing Liveness to Safety in First-Order Logic Reducing Liveness to Safety in First-Order Logic
Michele PaganiPagani, Michele University Paris DiderotFrance Stable, measurable functions and probabilistic programs Measurable cones and stable, measurable functions
Eliana PalermitiPalermiti, Eliana LoIDE: a a web-based IDE for Logic Programming - Preliminary Report
Jens PalsbergPalsberg, Jens University of California, Los Angeles (UCLA) Session Chair of Invited Tutorial by Mayur Naik (part of VMCAI) Typed and Jones Optimal Self-Applicable Partial Evaluation Jones-Optimal Partial Evaluation by Specialization-Safe Normalization Program Co-Chair in Program Committee within the VMCAI-track Co-chair in Organizing Committee within the VMCAI-track
Zoe ParaskevopoulouParaskevopoulou, Zoe Princeton UniversityUnited States Generating Good Generators for Inductive Relations Generating Good Generators for Inductive Relations
Daejun ParkPark, Daejun University of Illinois at Urbana-Champaign Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Lionel ParreauxParreaux, Lionel EPFLSwitzerland Unifying Analytic and Statically-Typed Quasiquotes Unifying Analytic and Statically-Typed Quasiquotes
Julian ParsertParsert, Julian University of Innsbruck, Austria Formal Microeconomic Foundations and the First Welfare Theorem
Marco PatrignaniPatrignani, Marco Saarland University, CISPAGermany Robust Hyperproperty Preservation for Secure Compilation Parametricity versus the Universal Type Committee Member in Program Committee within the PriSC-track Organizer in Organizing Committee within the PriSC-track
Daniel PattersonPatterson, Daniel Northeastern UniversityUnited States On Compositional Compiler Correctness and Fully Abstract Compilation
Brian PattonPatton, Brian Google TensorFlow Distributions
Andreas PavlogiannisPavlogiannis, Andreas IST Austria Optimal Dyck Reachability for Data-dependence and Alias Analysis Optimal Dyck Reachability for Data-dependence and Alias Analysis Data-centric Dynamic Partial Order Reduction
Mathias PayerPayer, Mathias Purdue UniversityUnited States Challenges For Compiler-backed Security: From Sanitizer to Mitigation (Invited Talk)
Jennifer PaykinPaykin, Jennifer University of PennsylvaniaUnited States Panel II: Life in Grad School (and Beyond) Phantom Types for Quantum Programs Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Committee Member in Panelists within the PLMW-track
Mathias Ruggaard PedersenPedersen, Mathias Ruggaard Aalborg University Comparing the speed of probabilistic processes
Hila PelegPeleg, Hila Generating Tests by Example Abstraction-Based Interaction Model for Synthesis
Luc PellissierPellissier, Luc Polyadic Approximations, Fibrations and Intersection Types
Fernando Magno Quintão PereiraPereira, Fernando Magno Quintão UFMGBrazil Inference of Static Semantics for Incomplete C Programs Inference of Static Semantics for Incomplete C Programs
Stuart PernsteinerPernsteiner, Stuart University of Washington, USA Œuf: Minimizing the Coq Extraction TCB
Simona PerriPerri, Simona Optimizing Answer Set Computation via Heuristic-Based Decomposition
Simon Peyton JonesPeyton Jones, Simon Microsoft Research Linear Haskell: practical linearity in a higher-order polymorphic language Linear Haskell: practical linearity in a higher-order polymorphic language Committee Member in Programme Committee within the PEPM-track
Lucas PeñaPeña, Lucas University of Illinois at Urbana-Champaign Foundations for Natural Proofs and Quantifier Instantiation Foundations for Natural Proofs and Quantifier Instantiation
Avi PfefferPfeffer, Avi Charles River Analytics Using Reinforcement Learning for Probabilistic Program Inference The Support Method of Computing Expectations
Frank PfenningPfenning, Frank Carnegie Mellon University, USAUnited States Session Chair of Session 1-3 (part of PEPM) Message-Passing Concurrency and Substructural Logics Committee Member in Programme Committee within the PEPM-track
Brigitte PientkaPientka, Brigitte McGill University Committee Member in Steering Committee for POPL 2018 Session Chair of Formalizing Meta-Theory (part of CPP ) POPLMark Reloaded: Mechanizing Logical Relations Proofs (Invited Talk) Committee Member in Program Committee within the Off the Beaten Track-track
Benjamin C. PiercePierce, Benjamin C. University of PennsylvaniaUnited States The Curse of Knowledge Formally Secure Compilation of Unsafe Low-Level Components Short talk: The Meaning of Memory Safety Synthesizing Bijective Lenses SIGPLAN Town Hall Synthesizing Bijective Lenses Generating Good Generators for Inductive Relations Generating Good Generators for Inductive Relations Committee Member in Speakers within the PLMW-track
Frank PiessensPiessens, Frank KU Leuven Linear capabilities for modular fully-abstract compilation of verified code Parametricity versus the Universal Type Committee Member in Program Committee within the PriSC-track
Maciej PirógPiróg, Maciej University of WrocławPoland Handle with Care: Relational Interpretation of Algebraic Effects and Handlers Handle with Care: Relational Interpretation of Algebraic Effects and Handlers
Ruzica PiskacPiskac, Ruzica Yale University Chair in Travel Grants within the VMCAI-track Committee Member in Program Committee within the POPL Research Papers-track
Clément Pit-ClaudelPit-Claudel, Clément MIT CSAIL Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Gordon PlotkinPlotkin, Gordon University of Edinburgh, UKUnited Kingdom Some Principles of Differential Programming Languages
Andreas PodelskiPodelski, Andreas University of Freiburg, GermanyGermany Reducing Liveness to Safety in First-Order Logic Reducing Liveness to Safety in First-Order Logic Committee Member in Program Committee within the VMCAI-track
Piotr PolesiukPolesiuk, Piotr University of Wrocław Handle with Care: Relational Interpretation of Algebraic Effects and Handlers Handle with Care: Relational Interpretation of Algebraic Effects and Handlers
Nadia PolikarpovaPolikarpova, Nadia University of California, San DiegoUnited States Session Chair of Synthesis (part of POPL Research Papers) Committee Member in Selection Committee within the POPL Student Research Competition-track Committee Member in Organizers within the PLMW-track Committee Member in Program Committee within the POPL Research Papers-track
Enrico PontelliPontelli, Enrico Automatic Web Services Composition for Phylotastic
Andrei PopescuPopescu, Andrei Middlesex University, LondonUnited Kingdom Safety and Conservativity of Definitions in HOL and Isabelle/HOL Programming and Reasoning with Infinite Data in Isabelle/HOL.
Zoran PopovicPopovic, Zoran University of Washington A Framework for Computer-Aided Design of Educational Domain Models
Louis-Noël PouchetPouchet, Louis-Noël Colorado State University Analytical Modeling of Cache Behavior for Affine Programs
Adi PrabawaPrabawa, Adi National University of Singapore A Logical System for Modular Information Flow Verification
Jonathan ProtzenkoProtzenko, Jonathan Microsoft Research, n.n.United States Short Talk: Secure compilation from F* to WebAssembly A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Christopher PultePulte, Christopher University of Cambridge Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8 Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8
George PîrleaPîrlea, George University College LondonUnited Kingdom Mechanising Blockchain Consensus
Markus PüschelPüschel, Markus ETH ZürichSwitzerland A Practical Construction for Decomposing Numerical Abstract Domains A Practical Construction for Decomposing Numerical Abstract Domains
Corina S. PăsăreanuPăsăreanu, Corina S. NASA Ames Research Center Committee Member in Program Committee within the VMCAI-track
Q Xiaokang QiuQiu, Xiaokang Purdue UniversityUnited States Committee Member in Program Committee within the VMCAI-track
Weihao QuQu, Weihao University at Buffalo, SUNY Relational Cost Analysis with State
Jean QuilbeufQuilbeuf, Jean INRIA Scalable Approximation of Quantitative Information Flow in Programs
R Ivan RadicekRadicek, Ivan TU Vienna Monadic refinements for relational cost analysis
Barath RaghavanRaghavan, Barath ICSI Panel
Sriram RajamaniRajamani, Sriram Microsoft Research Committee Member in Programme Committee within the PEPM-track
Zvonimir RakamaricRakamaric, Zvonimir University of UtahUnited States Committee Member in Program Committee within the POPL Research Papers-track
Tahina RamananandroRamananandro, Tahina Microsoft Research, n.n.United States A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Steven RamsayRamsay, Steven University of BristolUnited Kingdom Higher-Order Constrained Horn Clauses for Verification Higher-Order Constrained Horn Clauses for Verification
Norman RamseyRamsey, Norman Committee Member in Programme Committee within the PEPM-track Committee Member in Program Committee within the PPS-track
Robert RandRand, Robert University of PennsylvaniaUnited States Phantom Types for Quantum Programs
Francesco RanzatoRanzato, Francesco University of PadovaItaly Session Chair of Security (part of VMCAI) On Constructivity of Galois Connections
Dan RasinRasin, Dan Technion – Israel Institute of Technology Generating Tests by Example
Aseem RastogiRastogi, Aseem Microsoft ResearchIndia A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations Recalling a Witness: Foundations and Applications of Monotonic State Recalling a Witness: Foundations and Applications of Monotonic State Committee Member in Program Committee within the POPL Research Papers-track
Kristian RealeReale, Kristian A REST-based Development Framework for ASP: Tools and Application
Jakob RehofRehof, Jakob Technical University Dortmund Towards Language-independent Code Synthesis (Poster/Demo Talk)
Giselle ReisReis, Giselle Carnegie Mellon University Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
John RennerRenner, John UCSD Constant-time WebAssembly
Thomas RepsReps, Thomas University of Wisconsin - Madison and GrammaTech, Inc.United States Non-Linear Reasoning For Invariant Synthesis Non-Linear Reasoning For Invariant Synthesis Introduction to Algebraic Program analysis. Committee Member in Programme Committee within the PEPM-track
Tamara RezkRezk, Tamara InriaFrance Committee Member in Program Committee within the PriSC-track Organizer in Organizing Committee within the PriSC-track
Rodrigo Geraldo RibeiroRibeiro, Rodrigo Geraldo UFOP Inference of Static Semantics for Incomplete C Programs Inference of Static Semantics for Incomplete C Programs
Francesco RiccaRicca, Francesco A REST-based Development Framework for ASP: Tools and Application
François-René RideauRideau, François-René Climbing Up the Semantic Tower — at Runtime
James RielyRiely, James DePaul University Session Chair of Verifying Protocols and Systems (part of VMCAI) On abstraction and compositionality for weak-memory linearisability Transactions in Relaxed Memory Architectures
Noam RinetzkyRinetzky, Noam Tel Aviv UniversityIsrael Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts Committee Member in Program Committee within the VMCAI-track
Talia RingerRinger, Talia University of WashingtonUnited States Adapting Proof Automation to Adapt Proofs Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Nick RiouxRioux, Nick Northeastern University, USAUnited States Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible
Christine RizkallahRizkallah, Christine University of Pennsylvania, USAUnited States Total Haskell is Reasonable Coq
Jared RoeschRoesch, Jared University of Washington, USAUnited States Extensible Semantics for Fluidics
Adam RogalewiczRogalewicz, Adam Brno University of Technology From Shapes to Amortized Complexity
Sergei RomanenkoRomanenko, Sergei Keldysh Institute of Applied Mathematics of Russian Academy of SciencesRussia Committee Member in Programme Committee within the PEPM-track
Tiark RompfRompf, Tiark Purdue UniversityUnited States Collapsing Towers of Interpreters Collapsing Towers of Interpreters Committee Member in Steering Committee within the PEPM-track Committee Member in Programme Committee within the PEPM-track
Nima RoohiRoohi, Nima University of Pennsylvania Revisiting MITL to Fix Decision Procedures
Gregory RosenblattRosenblatt, Gregory n.n., n.n.Canada One Weird Trick: Relational Interpreters for Program Synthesis.
Damien RouhlingRouhling, Damien University of Côte d'Azur, France A Formal Proof in Coq of a Control Function for the Inverted Pendulum
Arjen RouvoetRouvoet, Arjen Delft University of Technology Intrinsically-Typed Definitional Interpreters Intrinsically-Typed Definitional Interpreters for Imperative Languages
Daniel RoyRoy, Daniel Auxiliary variables in Probabilistic Programs
Grigore RoşuRoşu, Grigore University of Illinois at Urbana-ChampaignUnited States Committee Member in Program Committee within the POPL Research Papers-track
Sasha RubinRubin, Sasha University of Naples Federico II Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction
Philipp RuemmerRuemmer, Philipp Uppsala UniversitySweden String Constraints with Concatenation and Transducers Solved Efficiently String Constraints with Concatenation and Transducers Solved Efficiently Committee Member in Program Committee within the VMCAI-track
Brian RuttenbergRuttenberg, Brian Charles River Analytics Committee Member in Program Committee within the PPS-track
Andrey RybalchenkoRybalchenko, Andrey Microsoft ResearchUnited Kingdom Very Large Scale Network Verification Committee Member in Program Committee within the POPL Research Papers-track
Didier RémyRémy, Didier Inria A Principled approach to Ornamentation in ML A Principled approach to Ornamentation in ML
S Amr SabrySabry, Amr Indiana UniversityEgypt Committee Member in Program Committee within the POPL Research Papers-track
P. SadayappanSadayappan, P. Ohio State UniversityUnited States Analytical Modeling of Cache Behavior for Affine Programs
Mooly SagivSagiv, Mooly Tel Aviv University Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts Reducing Liveness to Safety in First-Order Logic Reducing Liveness to Safety in First-Order Logic
Konstantinos (Kostis) SagonasSagonas, Konstantinos (Kostis) Effective Stateless Model Checking for C/C++ Concurrency Effective Stateless Model Checking for C/C++ Concurrency Committee Member in Steering Committee within the PEPM-track
Mouhammad SakrSakr, Mouhammad Saarland University Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity
Roopsha SamantaSamanta, Roopsha Purdue University Committee Member in Selection Committee within the POPL Student Research Competition-track Committee Member in Program Committee within the VMCAI-track
Alex Sanchez-SternSanchez-Stern, Alex University of California, San DiegoUnited States Student Volunteer Co-Captain in Organizing Committee for POPL 2018 Student Volunteer Captain in Organizers within the POPL Student Volunteers-track
Dave SandsSands, Dave Chalmers University of Technology Committee Member in Program Committee within the POPL Research Papers-track
Davide SangiorgiSangiorgi, Davide University of Bologna Committee Member in Program Committee within the POPL Research Papers-track
José Fragoso SantosSantos, José Fragoso Imperial College London JaVerT: JavaScript Verification using Separation Logic JaVerT: JavaScript Verification Toolchain
Susmit SarkarSarkar, Susmit University of St. Andrews Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8 Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8
Isao SasanoSasano, Isao Shibaura Institute of TechnologyJapan An Approach to Generating Text-Based IDEs with Syntax Completion (Poster/Demo Talk)
Yuki SatakeSatake, Yuki University of Tsukuba Propositional Dynamic Logic for Higher-Order Functional Programs Relatively Complete Refinement Type System for Verification of Higher-Order Non-Deterministic Programs
Annabel SatinSatin, Annabel P.C.K. Conference Manager in Organizing Committee for POPL 2018
Tetsuya SatoSato, Tetsuya University at Buffalo, SUNY, USAUnited States Reasoning about Divergences via Span-liftings
Rif A. SaurousSaurous, Rif A. Google Session Chair of SESSION IV (4 talks) (part of PPS) Deep Probabilistic Programming: TensorFlow Distributions and Edward TensorFlow Distributions
Gabriel SchererScherer, Gabriel Northeastern University, USAUnited States Correctness of Speculative Optimizations with Dynamic Deoptimization
Sven ScheweSchewe, Sven University of Liverpool Learning to Complement Büchi Automata
Tanja SchindlerSchindler, Tanja University of Freiburg Selfless Interpolation for Infinite-State Model Checking
Alan SchmittSchmitt, Alan Inria HOpi in Coq
Ulrik Pagh SchultzSchultz, Ulrik Pagh University of Southern Denmark Committee Member in Steering Committee within the PEPM-track
Steven SchäferSchäfer, Steven Binder Aware Recursion over Well-Scoped de Bruijn Syntax
Ryan ScottScott, Ryan Indiana UniversityUnited States Refinement Reflection: Complete Verification with SMT Refinement Reflection: Complete Verification with SMT
Taro SekiyamaSekiyama, Taro IBM Research, JapanJapan Towards Proof Synthesis by Neural Machine Translation Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Daniel SelsamSelsam, Daniel Stanford UniversityUnited States Formal Methods For Probabilistic Programming
Ilya SergeySergey, Ilya University College LondonUnited Kingdom Session Chair of Semantics and Synthesis (part of CoqPL) Mechanising Blockchain Consensus Programming and Proving with Distributed Protocols Programming and Proving with Distributed Protocols Programme Co-Chair in Organizing Committee within the CoqPL-track Programme Co-Chair in Program Committee within the CoqPL-track
Peter SestoftSestoft, Peter IT University of Copenhagen Rewriting High-Level Spreadsheet Structures into Higher-Order Functional Programs Committee Member in Programme Committee within the PEPM-track
Peter SewellSewell, Peter University of Cambridge Simplifying ARM Concurrency: Multicopy-Atomic Axiomatic and Operational Models for ARMv8 Simplifying ARM Concurrency: Multicopy-atomic Axiomatic and Operational Models for ARMv8 Committee Member in Program Committee within the POPL Research Papers-track
Anees ShaikhShaikh, Anees Google Common Models for Network Configuration and Behavioral Validation
Amir ShaikhhaShaikhha, Amir EPFL Unifying Analytic and Statically-Typed Quasiquotes Unifying Analytic and Statically-Typed Quasiquotes
Chung-chieh ShanShan, Chung-chieh Indiana University, USA More support for symbolic disintegration Equational reasoning for probabilistic programming.
Natarajan ShankarShankar, Natarajan SRI International, USA Session Chair of Verifying Programs and Systems (part of CPP ) Proofs in Conflict-Driven Theory Combination
Zhong ShaoShao, Zhong Yale University Session Chair of Verification I (part of POPL Research Papers) Session Chair of Trusted Verification Frameworks and Systems (part of CPP ) Committee Member in Program Committee within the POPL Research Papers-track
Marc ShapiroShapiro, Marc LIP6 Co-Design and Verification of an Available File System
Ekansh SharmaSharma, Ekansh Auxiliary variables in Probabilistic Programs
Rahul SharmaSharma, Rahul Microsoft ResearchIndia On Automatically Proving the Correctness of math.h Implementations Committee Member in Program Committee within the VMCAI-track
Dennis ShashaShasha, Dennis New York University Go with the Flow: Compositional Abstractions for Concurrent Data Structures
Benjamin ShermanSherman, Benjamin Massachusetts Institute of Technology, USAUnited States Constructive probabilistic semantics with non-spatial locales
Sharon ShohamShoham, Sharon Tel Aviv universityIsrael Safety Verification of Stateful Networks Abstraction-Based Interaction Model for Synthesis Reducing Liveness to Safety in First-Order Logic Reducing Liveness to Safety in First-Order Logic
Wolfram ShulteShulte, Wolfram Facebook Committee Member in Programme Committee within the PEPM-track
Xujie SiSi, Xujie University of Pennsylvania Maximum Satisfiability in Program Analysis: Applications and Techniques
Filip SieczkowskiSieczkowski, Filip University of WrocławPoland Handle with Care: Relational Interpretation of Algebraic Effects and Handlers Handle with Care: Relational Interpretation of Algebraic Effects and Handlers
Jeremy G. SiekSiek, Jeremy G. Indiana University, USAUnited States Back to the Future with Denotational Semantics Gradually Typed Symbolic Expressions
Alexandra SilvaSilva, Alexandra University College LondonUnited Kingdom Probabilistic Program Equivalence for NetKAT Committee Member in Organizers within the PLMW-track
Axel SimonSimon, Axel Google Modular Analysis of Executables using On-Demand Heyting Completion
Gagandeep SinghSingh, Gagandeep United States A Practical Construction for Decomposing Numerical Abstract Domains A Practical Construction for Decomposing Numerical Abstract Domains
Rishabh SinghSingh, Rishabh Microsoft ResearchUnited States WebRelate: Integrating Web Data with Spreadsheets using Examples WebRelate: Integrating Web Data with Spreadsheets using Examples Program Synthesis using Abstraction Refinement
Rohit SinghSingh, Rohit CSAIL, MITUnited States Website Chair in Organizing Committee for POPL 2018
Satnam SinghSingh, Satnam X, the moonshot factoryUnited States SIGPLAN Awards
Nishant SinhaSinha, Nishant IBM Research Data-centric Dynamic Partial Order Reduction
Moritz SinnSinn, Moritz St. Polten University of Applied Sciences From Shapes to Amortized Complexity
Rob SisonSison, Rob Data61, CSIRO and UNSWAustralia Per-Thread Compositional Compilation for Confidentiality-Preserving Concurrent Programs
Lau SkorstengaardSkorstengaard, Lau Enforcing Well-bracketed Control Flow and Stack Encapsulation using Linear Capabilities
Yannis SmaragdakisSmaragdakis, Yannis University of Athens Committee Member in Program Committee within the POPL Research Papers-track
Jonathan SmithSmith, Jonathan DARPAUnited States Store, Translate and Forward: From Model to Metal in 25 Years Panel
Gert SmolkaSmolka, Gert Saarland University Large Model Constructions for Second-Order ZF in Dependent Type Theory Committee Member in Program Committee within the CPP -track
Steffen SmolkaSmolka, Steffen Cornell University Probabilistic Program Equivalence for NetKAT
Ana SokolovaSokolova, Ana University of Salzburg Committee Member in Program Committee within the VMCAI-track
Armando Solar-LezamaSolar-Lezama, Armando MIT CSAILUnited States How to Become a Researcher Committee Member in Speakers within the PLMW-track
Tran Cao SonSon, Tran Cao Automatic Web Services Composition for Phylotastic
Harald SondergaardSondergaard, Harald Committee Member in Programme Committee within the PEPM-track
Matthieu SozeauSozeau, Matthieu InriaFrance Session with the Coq Development Team Typed Template Coq Equations: From Clauses to Splittings to Functions (Poster/Demo Talk)
Antal Spector-ZabuskySpector-Zabusky, Antal Total Haskell is Reasonable Coq
Bas SpittersSpitters, Bas Committee Member in Program Committee within the CPP -track
Arnaud SpiwackSpiwack, Arnaud Tweag I/OFrance Linear Haskell: practical linearity in a higher-order polymorphic language Linear Haskell: practical linearity in a higher-order polymorphic language
Vivek SrikumarSrikumar, Vivek University of Utah SweetPea: A Language for Designing Experiments
Mark StaplesStaples, Mark CSIRO, Australia Towards Verifying Ethereum Smart Contract Bytecode in Isabelle/HOL
Ian StarkStark, Ian The University of EdinburghUnited Kingdom Triangulating Context Lemmas
Kathrin StarkStark, Kathrin Saarland University, Germany Binder Aware Recursion over Well-Scoped de Bruijn Syntax
Sam StatonStaton, Sam University of Oxford The semantic structure of quasi-Borel spaces: algebra, logic, and recursion Denotational validation of higher-order Bayesian inference
Deian StefanStefan, Deian University of California, San Diego Constant-time WebAssembly
Leo StefanescoStefanesco, Leo ENS Lyon A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST
Gordon StewartStewart, Gordon Ohio University Snaarkl: Somewhat Practical, Pretty Much Declarative Verifiable Computing in Haskell
Ilina StoilkovskaStoilkovska, Ilina Vienna University of Technology Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction
Jan StolarekStolarek, Jan University of Edinburgh, UKPoland Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Marco StronatiStronati, Marco Formally Secure Compilation of Unsafe Low-Level Components Robust Hyperproperty Preservation for Secure Compilation
Pierre-Yves StrubStrub, Pierre-Yves Ecole PolytechniqueFrance Proving Expected Sensitivity of Probabilistic Programs Proving expected sensitivity of probabilistic programs Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Committee Member in Program Committee within the CPP -track
Sandro StuckiStucki, Sandro EPFLSwitzerland Simplicitly: Foundations and Applications of Implicit Function Types Simplicitly: Foundations and Applications of Implicit Function Types
Nataliia StulovaStulova, Nataliia IMDEA Software Institute and T.U. of Madrid (UPM)Spain Exploiting Term Hiding to Reduce Run-time Checking Overhead
Aaron StumpStump, Aaron University of Iowa, USA Generic Derivation of Induction for Impredicative Encodings in Cedille
Zhendong SuSu, Zhendong University of California, DavisUnited States Committee Member in Program Committee within the POPL Research Papers-track
Martin SudaSuda, Martin TU Wien, Vienna, Austria Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Kohei SuenagaSuenaga, Kohei Graduate School of Informatics, Kyoto UniversityJapan Session Chair of Session 2-2 (part of PEPM) Towards Proof Synthesis by Neural Machine Translation A Guess-and-Assume Approach to Loop Fusion for Program Verification Committee Member in Programme Committee within the PEPM-track
Charles SuttonSutton, Charles University of EdinburghUnited Kingdom SlicStan: Improving Probabilistic Programming using Information Flow Analysis
Nikhil SwamySwamy, Nikhil Microsoft ResearchUnited States A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations Recalling a Witness: Foundations and Applications of Monotonic State Recalling a Witness: Foundations and Applications of Monotonic State Committee Member in Program Committee within the PriSC-track
David SwaseySwasey, David MPI-SWSGermany Robust Hyperproperty Preservation for Secure Compilation
T Quang-Trung TaTa, Quang-Trung National University of Singapore Automated Lemma Synthesis in Symbolic-Heap Separation Logic Automated Lemma Synthesis in Symbolic-Heap Separation Logic
Nicolas TabareauTabareau, Nicolas Inria, France Typed Template Coq Foundations of Dependent Interoperability
Éric TanterTanter, Éric University of ChileChile Foundations of Dependent Interoperability Gradual Program Verification Committee Member in Program Committee within the POPL Research Papers-track
Paul TarauTarau, Paul University of North TexasUnited States On k-colored Lambda Terms and their Skeletons
Enrico TassiTassi, Enrico INRIA Elpi: an extension language for Coq
Christine TassonTasson, Christine University Paris Diderot Stable, measurable functions and probabilistic programs Measurable cones and stable, measurable functions
Zachary TatlockTatlock, Zachary University of Washington, SeattleUnited States Session Chair of Language Design (part of POPL Research Papers) Session Chair of Strings (part of POPL Research Papers) Panel II: Life in Grad School (and Beyond) Œuf: Minimizing the Coq Extraction TCB Programming and Proving with Distributed Protocols Programming and Proving with Distributed Protocols Committee Member in Panelists within the PLMW-track Committee Member in Program Committee within the POPL Research Papers-track
Finn TeegenTeegen, Finn University of Kiel, GermanyGermany Probabilistic Functional Logic Programming
Tachio TerauchiTerauchi, Tachio Waseda University Session Chair of Program Analysis I (part of POPL Research Papers) Session Chair of Types and Analysis (part of VMCAI) Relatively Complete Refinement Type System for Verification of Higher-Order Non-Deterministic Programs Committee Member in Program Committee within the VMCAI-track Committee Member in Program Committee within the POPL Research Papers-track
Peter ThiemannThiemann, Peter University of Freiburg, Germany Committee Member in Steering Committee for POPL 2018 Committee Member in Selection Committee within the POPL Workshops-track
René ThiemannThiemann, René University of Innsbruck Session Chair of Proof Methods and Libraries (part of CPP ) Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
Laurent ThéryThéry, Laurent INRIAFrance Committee Member in Program Committee within the CPP -track
Amin TimanyTimany, Amin imec-Distrinet KU-LeuvenBelgium A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST
Laura TitoloTitolo, Laura National Institute of Aerospace, USAItaly An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs
Sam Tobin-HochstadtTobin-Hochstadt, Sam Indiana UniversityUnited States Soft Contract Verification for Higher-order Stateful Programs Soft Contract Verification for Higher-order Stateful Programs
Andrew TolmachTolmach, Andrew Portland State University Formally Secure Compilation of Unsafe Low-Level Components Intrinsically-Typed Definitional Interpreters Intrinsically-Typed Definitional Interpreters for Imperative Languages
Anish TondwalkarTondwalkar, Anish UCSD Refinement Reflection: Complete Verification with SMT Refinement Reflection: Complete Verification with SMT
Jordan TorfTorf, Jordan UIC P5: Planner-less Proofs of Probabilistic Parameterized Protocols
Emina TorlakTorlak, Emina University of WashingtonUnited States A Framework for Computer-Aided Design of Educational Domain Models Refinement Types for Ruby Symbolic Types for Lenient Symbolic Execution Symbolic Types for Lenient Symbolic Execution
Matías ToroToro, Matías University of Chile Type-Driven Gradual Security with References
Jared TramontanoTramontano, Jared Massachusetts Institute of Technology Constructive probabilistic semantics with non-spatial locales
Dustin TranTran, Dustin Deep Probabilistic Programming: TensorFlow Distributions and Edward TensorFlow Distributions
Jean-Baptiste TristanTristan, Jean-Baptiste Oracle LabsUnited States Committee Member in Program Committee within the PPS-track
Andrea TurriniTurrini, Andrea State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences Learning to Complement Büchi Automata
U Chihiro UeharaUehara, Chihiro Ochanomizu University Selective CPS Transformation for Shift and Reset
Hiroshi UnnoUnno, Hiroshi University of Tsukuba Relatively Complete Refinement Type System for Verification of Higher-Order Non-Deterministic Programs
Josef UrbanUrban, Josef Czech Technical University in PragueCzechia Committee Member in Program Committee within the CPP -track
V Viktor VafeiadisVafeiadis, Viktor MPI-SWS, GermanyGreece Effective Stateless Model Checking for C/C++ Concurrency Effective Stateless Model Checking for C/C++ Concurrency Committee Member in Organizers within the PLMW-track Committee Member in Program Committee within the POPL Research Papers-track Committee Member in Program Committee within the CPP -track
Kapil VaidyaVaidya, Kapil IIT Bombay Data-centric Dynamic Partial Order Reduction
L. Thomas van Binsbergenvan Binsbergen, L. Thomas Royal Holloway University of LondonNetherlands Checking Cryptographic API Usage with Composable Annotations (Short Paper)
Jan-Willem van de Meentvan de Meent, Jan-Willem Northeastern UniversityUnited States Committee Member in Program Committee within the PPS-track
Guy Van den BroeckVan den Broeck, Guy University of California, Los Angeles Probabilistic Program Inference With Abstractions
Niels van der Weidevan der Weide, Niels Radboud University Nijmegen, Netherlands Finite Sets in Homotopy Type Theory
David Van HornVan Horn, David University of Maryland Soft Contract Verification for Higher-order Stateful Programs Soft Contract Verification for Higher-order Stateful Programs
Peter Van RoyVan Roy, Peter Université catholique de LouvainBelgium Towards A Systems Approach To Distributed Programming
Thomas Van StrydonckVan Strydonck, Thomas KULeuven Linear capabilities for modular fully-abstract compilation of verified code
Andrea VandinVandin, Andrea DTU, DenmarkDenmark Committee Member in Artifact Evaluation Committee within the POPL Artifact Evaluation-track
Dimitrios VardoulakisVardoulakis, Dimitrios Google On quantifying the degree of unsoundness of static analyses
George VargheseVarghese, George UCLA A Vision for Network Design Automation
Srinivas VasudevanVasudevan, Srinivas Google TensorFlow Distributions
Niki VazouVazou, Niki University of Maryland Liquid Haskell: Refinement Types for Haskell Refinement Types for Ruby Refinement Reflection: Complete Verification with SMT Refinement Reflection: Complete Verification with SMT Committee Member in Speakers within the PLMW-track
Martin VechevVechev, Martin ETH Zürich Automatic Verification of RMA Programs via Abstraction Extrapolation A Practical Construction for Decomposing Numerical Abstract Domains A Practical Construction for Decomposing Numerical Abstract Domains Committee Member in Programme Committee within the PEPM-track
Pierfrancesco VeltriVeltri, Pierfrancesco A REST-based Development Framework for ASP: Tools and Application
Abhinav VermaVerma, Abhinav Program Synthesis with Neural Oracles
Andrea VezzosiVezzosi, Andrea Chalmers University of Technology Decidability of Conversion for Type Theory in Type Theory Decidability of Conversion for Type Theory in Type Theory
Pierre VialVial, Pierre Polyadic Approximations, Fibrations and Intersection Types
Marcos VieraViera, Marcos University of the Republic, Uruguay Committee Member in Programme Committee within the PEPM-track
Eelco VisserVisser, Eelco Delft University of TechnologyNetherlands Intrinsically-Typed Definitional Interpreters Intrinsically-Typed Definitional Interpreters for Imperative Languages
Mahesh ViswanathanViswanathan, Mahesh University of Illinois at Urbana-Champaign Revisiting MITL to Fix Decision Procedures
Jan VitekVitek, Jan Northeastern UniversityUnited States Committee Member in Steering Committee for POPL 2018 Correctness of Speculative Optimizations with Dynamic Deoptimization
Antoine VoizardVoizard, Antoine University of Pennsylvannia Locally Nameless at Scale Unifying Analytic and Statically-Typed Quasiquotes Unifying Analytic and Statically-Typed Quasiquotes
Tomáš VojnarVojnar, Tomáš Brno University of Technology From Shapes to Amortized Complexity String Constraints with Concatenation and Transducers Solved Efficiently String Constraints with Concatenation and Transducers Solved Efficiently
Tamara von Glehnvon Glehn, Tamara University of Cambridge Partially Static Data as Free Extension of Algebras (Short Paper)
Matthijs VákárVákár, Matthijs University of Oxford Game Semantics for Probabilistic Programs The semantic structure of quasi-Borel spaces: algebra, logic, and recursion Denotational validation of higher-order Bayesian inference
W Philip WadlerWadler, Philip University of Edinburgh, UKUnited Kingdom Refinement Reflection: Complete Verification with SMT Refinement Reflection: Complete Verification with SMT Committee Member in Program Committee within the POPL Research Papers-track
Thomas WahlWahl, Thomas Northeastern University Committee Member in Program Committee within the VMCAI-track
David WalkerWalker, David Princeton UniversityUnited States Industrial Relations Chair in Organizing Committee for POPL 2018 Committee Member in Steering Committee for POPL 2018 Panel I: Technical Trends in Programming Languages Research Panel Synthesizing Bijective Lenses Synthesizing Bijective Lenses Committee Member in Panelists within the PLMW-track Committee Member in Program Committee within the POPL Research Papers-track
Eric WalkingshawWalkingshaw, Eric Oregon State UniversityUnited States Migrating Gradual Types Migrating Gradual Types
Mitchell WandWand, Mitchell Northeastern University, USA Contextual Equivalence for a Probabilistic Language with Continuous Random Variables and Recursion
Xinyu WangWang, Xinyu UT AustinChina Program Synthesis using Abstraction Refinement
Yanjun WangWang, Yanjun A Decidable Logic for Tree Data-Structures with Measurements
Yuepeng WangWang, Yuepeng University of Texas at Austin Verifying Equivalence of Database-Driven Applications
Takahisa WatanabeWatanabe, Takahisa University of Tsukuba, Japan Program Generation for ML Modules (Short Paper)
Conrad WattWatt, Conrad University of Cambridge, UK Mechanising and Verifying the WebAssembly Specification
Stephanie WeirichWeirich, Stephanie University of Pennsylvania, USAUnited States Locally Nameless at Scale Total Haskell is Reasonable Coq POPL 2019 Preview Committee Member in Program Committee within the POPL Research Papers-track Committee Member in Program Committee within the CPP -track
Edwin WestbrookWestbrook, Edwin Galois, Inc. Mechanizing the Construction and Rewriting of Proper Functions in Coq
Leo WhiteWhite, Leo Jane Street Modular Macros (Poster/Demo Talk)
Josef WidderWidder, Josef TU WienAustria Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction
Paweł WieczorekWieczorek, Paweł University of WrocławPoland A Coq Formalization of Normalization by Evaluation for Martin-Löf Type Theory
Thomas WiesWies, Thomas New York University Go with the Flow: Compositional Abstractions for Concurrent Data Structures Committee Member in Program Committee within the VMCAI-track
James R. WilcoxWilcox, James R. University of WashingtonUnited States Œuf: Minimizing the Coq Extraction TCB Programming and Proving with Distributed Protocols Programming and Proving with Distributed Protocols
Thomas WilliamsWilliams, Thomas Inria A Principled approach to Ornamentation in ML A Principled approach to Ornamentation in ML
Max WillseyWillsey, Max University of WashingtonUnited States Extensible Semantics for Fluidics
Thomas WoodWood, Thomas Imperial College LondonUnited Kingdom JaVerT: JavaScript Verification using Separation Logic JaVerT: JavaScript Verification Toolchain
Zhilin WuWu, Zhilin State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences What's Decidable About String Constraints with ReplaceAll Function?
X Haochen XieXie, Haochen Nagoya UniversityJapan Formal Models Underlying Blockchain Technology
Rachel XuXu, Rachel Comparison among three program verification techniques in Dependent Haskell, Liquid Haskell and F*
Y Eran YahavYahav, Eran TechnionIsrael Generating Tests by Example
Jeremy YallopYallop, Jeremy University of Cambridge, UK Partially Static Data as Free Extension of Algebras (Short Paper) Modular Macros (Poster/Demo Talk) Committee Member in Steering Committee within the PEPM-track
Akihisa YamadaYamada, Akihisa Efficient Certification of Complexity Proofs: Formalizing the Perron–Frobenius Theorem (Invited Talk Paper)
Hongseok YangYang, Hongseok University of Oxford The semantic structure of quasi-Borel spaces: algebra, logic, and recursion Denotational validation of higher-order Bayesian inference
Jean YangYang, Jean Carnegie Mellon University Artefact Evaluation Co-Chair in Organizing Committee for POPL 2018 Publicity Chair in Organizing Committee for POPL 2018 Session Chair of Dynamic Languages (part of POPL Research Papers) Artifact Evaluation Co-Chair in Artifact Evaluation Committee within the POPL Artifact Evaluation-track Committee Member in Program Committee within the POPL Research Papers-track
Jianhua YaoYao, Jianhua Stevens Institute of Technology Dataflow Metaprogramming (Poster/Demo Talk)
Nathaniel YazdaniYazdani, Nathaniel University of Washington, SeattleUnited States Adapting Proof Automation to Adapt Proofs
Ming-Ho YeeYee, Ming-Ho Northeastern University, USAUnited States Correctness of Speculative Optimizations with Dynamic Deoptimization
Mingsheng YingYing, Mingsheng University of Technology Sydney Algorithmic Analysis of Termination Problems for Quantum Programs
Brent YorgeyYorgey, Brent Hendrix CollegeUnited States Explaining Type Errors
Nobuko YoshidaYoshida, Nobuko Imperial College London Committee Member in Programme Committee within the PEPM-track
Z Jakub ZalewskiZalewski, Jakub University of EdinburghUnited Kingdom Student Volunteer Co-Captain in Organizing Committee for POPL 2018 Student Volunteer Captain in Organizers within the POPL Student Volunteers-track
Santiago Zanella-BéguelinZanella-Béguelin, Santiago Microsoft Research, n.n. A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations
Jessica ZangariZangari, Jessica Optimizing Answer Set Computation via Heuristic-Based Decomposition
Carlo ZanioloZaniolo, Carlo INVITED TALK: Declarative Algorithms on Big Data: a Logic-Based Solution
Steve ZdancewicZdancewic, Steve University of PennsylvaniaUnited States Session Chair of PL Metatheory (part of CoqPL) Phantom Types for Quantum Programs Synthesizing Bijective Lenses Synthesizing Bijective Lenses Committee Member in Organizers within the PLMW-track
Charles ZhangZhang, Charles Committee Member in Program Committee within the VMCAI-track
Danfeng ZhangZhang, Danfeng Pennsylvania State UniversityUnited States Committee Member in Program Committee within the POPL Research Papers-track
Lijun ZhangZhang, Lijun Institute of Software, Chinese Academy of Sciences Learning to Complement Büchi Automata
Xin ZhangZhang, Xin Massachusetts Institute of Technology, USAUnited States Maximum Satisfiability in Program Analysis: Applications and Techniques
Xinyue ZhangZhang, Xinyue Bryn Mawr College, USAUnited States Comparison among three program verification techniques in Dependent Haskell, Liquid Haskell and F*
Beta ZilianiZiliani, Beta FAMAF, UNC and CONICETArgentina A “destruct” Tactic for Mtac2 Committee Member in Program Committee within the CoqPL-track
Yoni ZoharZohar, Yoni Tel Aviv University Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts Online Detection of Effectively Callback Free Objects with Applications to Smart Contracts
Lenore ZuckZuck, Lenore Session Chair of Invited Talk by Kenneth L. McMillan (part of VMCAI) P5: Planner-less Proofs of Probabilistic Parameterized Protocols
Florian ZulegerZuleger, Florian TU Vienna Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction From Shapes to Amortized Complexity Monadic refinements for relational cost analysis
Ç Ezgi ÇiçekÇiçek, Ezgi MPI-SWS, Germany Committee Member in Programme Committee within the PEPM-track
Ö Joakim ÖhmanÖhman, Joakim IMDEA Software Institute Decidability of Conversion for Type Theory in Type Theory Decidability of Conversion for Type Theory in Type Theory
Ś Adam ŚcibiorŚcibior, Adam University of Cambridge and MPI Tuebingen The semantic structure of quasi-Borel spaces: algebra, logic, and recursion Denotational validation of higher-order Bayesian inference

POPL 2018 Contributors

Results (699)

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposia