Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sun 16 JanDisplayed time zone: Eastern Time (US & Canada) change
Sun 16 Jan
Displayed time zone: Eastern Time (US & Canada) change
09:00 - 10:00 | KeynoteLAFI at LAFI Chair(s): Cameron Freer Massachusetts Institute of Technology, Ohad Kammar University of Edinburgh | ||
09:00 60mKeynote | Abstract types in probabilistic programmingRemote LAFI Sam Staton University of Oxford File Attached | ||
09:00 - 10:00 | |||
09:00 60mKeynote | Sequential Information FlowRemote VMCAI Thomas A. Henzinger IST Austria, Austria | ||
09:00 - 09:45 | |||
09:00 45mKeynote | Research keynote -- Programming Languages and Law: A Research Agenda for a New FieldRemote ProLaLa James Grimmelmann Cornell University File Attached | ||
09:45 - 10:05 | |||
09:45 20mTalk | Legal CalculiInPerson ProLaLa Shrutarshi Basu Harvard University, Anshuman Mohan Cornell University, James Grimmelmann Cornell University, Nate Foster Cornell University File Attached | ||
10:20 - 12:00 | |||
10:20 33mTalk | Probabilistic and Differentiable Programming in Scientific SimulatorsRemote LAFI Atılım Güneş Baydin Department of Engineering Science, University of Oxford File Attached | ||
10:53 33mTalk | Stateful processes in probabilistic programming Remote LAFI Hugo Paquet University of Cambridge File Attached | ||
11:26 33mTalk | Programming Languages for Automatic Differentiation: What Now?Remote LAFI Damiano Mazza CNRS File Attached | ||
10:20 - 11:50 | Static Analysis and Abstract InterpretationVMCAI at Salon I Chair(s): Thomas Wies New York University | ||
10:20 30mPaper | Relational String Abstract DomainsRemote VMCAI Vincenzo Arceri University of Parma - Department of Mathematical, Physical, and Computer Sciences, Martina Olliaro Ca' Foscari University of Venice - Department of Environmental Sciences, Informatics and Statistics, Agostino Cortesi Università Ca' Foscari Venezia, Pietro Ferrara Università Ca' Foscari, Venezia, Italy | ||
10:50 30mPaper | Lightweight Shape Analysis based on Physical TypesInPerson VMCAI Olivier Nicole CEA LIST, France, Matthieu Lemerre CEA LIST, France, Xavier Rival INRIA/CNRS/ENS Paris | ||
11:20 30mPaper | A Flow-Insensitive-Complete Program RepresentationRemote VMCAI | ||
13:30 - 14:45 | |||
13:30 37mTalk | JAX: accelerating ML research with composable function transformationsRemote LAFI Roy Frostig Google Research | ||
14:07 37mTalk | Scalable structure learning and inference for domain-specific probabilistic programsRemote LAFI Feras Saad Massachusetts Institute of Technology | ||
13:30 - 14:30 | Privacy and SecurityVMCAI at Salon I Chair(s): Vincenzo Arceri University of Parma - Department of Mathematical, Physical, and Computer Sciences | ||
13:30 30mPaper | Verifying Pufferfish Privacy in Hidden Markov ModelsRemote VMCAI Depeng Liu Institute of Software, Chinese Academy of Sciences, Bow-Yaw Wang Academia Sinica, Lijun Zhang Institute of Software, Chinese Academy of Sciences | ||
14:00 30mPaper | Verifying Solidity Smart Contracts Via Communication Abstraction in SmartACERemote VMCAI Scott Wesley University of Waterloo, Canada, Maria Christakis MPI-SWS, Jorge A. Navas Certora, inc., Richard Trefler University of Waterloo, Canada, Valentin Wüstholz ConsenSys, Arie Gurfinkel University of Waterloo | ||
13:30 - 14:10 | |||
13:30 10mTalk | Littleton: An Educational Environment for Property LawRemote ProLaLa Shrutarshi Basu Harvard University, Anshuman Mohan Cornell University, James Grimmelmann Cornell University, Nate Foster Cornell University File Attached | ||
13:40 10mTalk | Modeling Administrative Discretion Using Goal-Directed Answer Set ProgrammingRemote ProLaLa Joaquín Arias Universidad Rey Juan Carlos, Mar Moreno-Rebato Universidad Rey Juan Carlos, José Antonio Rodríguez-García Universidad Rey Juan Carlos, Sascha Ossowski Universidad Rey Juan Carlos Pre-print Media Attached File Attached | ||
13:50 10mTalk | Probabilistic programming for Employment Tribunal remediesRemote ProLaLa James Cheney University of Edinburgh; Alan Turing Institute | ||
14:00 10mTalk | Prevalence of Expression Types in Legislative TextRemote ProLaLa Jason Morris Service Canada, Lexpedite Legal Technology | ||
14:10 - 14:50 | |||
14:10 20mTalk | Law Smells: Defining and Detecting Problematic Patterns in Legal DraftingRemote ProLaLa Corinna Coupette Max Planck Institute for Informatics, Saarbrücken, Germany, Dirk Hartung Center for Legal Technology and Data Science, Bucerius Law School, Hamburg, Germany, Janis Beckedorf Ruprecht-Karls-Universität Heidelberg, Heidelberg, Germany, Maximilian Böther Hasso Plattner Institute, University of Potsdam, Potsdam, Germany, Daniel Martin Katz Illinois Tech – Chicago Kent College of Law, Chicago, IL, USA Pre-print File Attached | ||
14:30 20mTalk | Cod(e)ifying The LawInPerson ProLaLa Nel Escher University of Michigan, Jeffrey Bilik University of Michigan, Alexander Miller University of Michigan, Jennifer Jiyoung Huseby University of Michigan, Divya Ramesh University of Michigan, Alice Liu University of Michigan, Sam Mikell University of Michigan, Nina Cahill University of Michigan, Ben Green University of Michigan, Nikola Banovic University of Michigan File Attached | ||
15:05 - 16:20 | |||
15:05 18mTalk | Towards Denotational Semantics of AD for Higher-Order, Recursive, Probabilistic LanguagesRemote LAFI Alexander K. Lew Massachusetts Institute of Technology, USA, Mathieu Huot Oxford University, Vikash K. Mansinghka MIT File Attached | ||
15:23 18mTalk | A Language and Smoothed Semantics for Convergent Stochastic Gradient DescentRemote LAFI File Attached | ||
15:42 18mTalk | Nonparametric Involutive Markov Chain Monte CarloRemote LAFI Carol Mak University of Oxford, Fabian Zaiser University of Oxford, C.-H. Luke Ong University of Oxford File Attached | ||
16:01 18mTalk | Rigorous Approximation of Posterior Inference for Probabilistic ProgramsRemote LAFI Fabian Zaiser University of Oxford, Raven Beutner CISPA Helmholtz Center for Information Security, Germany, C.-H. Luke Ong University of Oxford File Attached | ||
15:05 - 16:35 | |||
15:05 - 16:35 | |||
15:05 30mPaper | Generalized Arrays for Stainless FramesRemote VMCAI | ||
15:35 30mPaper | NP Satisfiability for Arrays as PowersInPerson VMCAI | ||
16:05 30mPaper | Bit-Precise Reasoning via Int-BlastingRemote VMCAI Yoni Zohar Bar Ilan University, Ahmed Irfan Stanford University, Makai Mann Stanford University, Aina Niemetz Stanford University, Andres Nötzli Stanford University, USA, Mathias Preiner Stanford University, Andrew Reynolds University of Iowa, Clark Barrett Stanford University, Cesare Tinelli University of Iowa | ||
15:05 - 15:25 | |||
15:05 20mTalk | Stipula: a domain specific language for legal contractsRemote ProLaLa Silvia Crafa University of Padova, Cosimo Laneve University of Bologna, Giovanni Sartor University of Bologna Pre-print File Attached | ||
15:25 - 16:10 | |||
15:25 45mIndustry talk | Industry keynote -- What does a toolchain for legislation eventually become?Remote ProLaLa Link to publication | ||
16:10 - 16:30 | |||
16:10 20mTalk | Ergo - a programming language for Smart Legal ContractsRemote ProLaLa Niall Roche Mishcon de Reya,University College London,Accord Project, Jerome Simeon Clause, Walter Hernandez Mishcon de Reya,Accord Project, Eason Chen Accord Project, Dan Selman Docusign,Accord Project Pre-print File Attached | ||
16:40 - 17:30 | KeynoteLAFI at LAFI Chair(s): Ohad Kammar University of Edinburgh, Christine Tasson Sorbonne Université — LIP6 | ||
16:40 50mKeynote | Program Analysis of Probabilistic ProgramsRemote LAFI Maria I. Gorinova The University of Edinburgh File Attached | ||
16:40 - 17:40 | |||
16:40 20mTalk | A General Library of Legal ComponentsRemote ProLaLa Chris Bailey University of Illinois College of Law Link to publication | ||
17:00 20mTalk | Overview of the CCLAW L4 projectRemote ProLaLa Avishkar Mahajan Singapore Management University, Martin Strecker Singapore Management University, Meng Weng Wong Singapore Management University | ||
17:20 20mTalk | Turning Catala into a Proof Platform for the LawRemote ProLaLa Pre-print | ||
Mon 17 JanDisplayed time zone: Eastern Time (US & Canada) change
Mon 17 Jan
Displayed time zone: Eastern Time (US & Canada) change
08:50 - 09:00 | Welcome from the chairsCPP at Salon III Chair(s): Lennart Beringer Princeton University, Robbert Krebbers Radboud University Nijmegen, Andrei Popescu University of Sheffield, Steve Zdancewic University of Pennsylvania | ||
08:50 10mTalk | Chairs' report CPP File Attached | ||
09:00 - 10:00 | Invited talkPADL at Directors Chair(s): James Cheney University of Edinburgh; Alan Turing Institute Remote session chair | ||
09:00 60mKeynote | People, Ideas, and the Path AheadIn-Person PADL Marcello Balduccini Saint Joseph's University, USA | ||
09:00 - 10:00 | |||
09:00 60mTutorial | Program Analysis via Graph Reachability: Past, Present, and Future [Part A]Remote TutorialFest Thomas Reps University of Wisconsin--Madison | ||
09:00 - 10:00 | Invited TalkVMCAI at Salon I Chair(s): Bernd Finkbeiner CISPA Helmholtz Center for Information Security | ||
09:00 60mKeynote | Back to the Future: A Fresh Look at Linear Temporal LogicRemote VMCAI | ||
09:00 - 10:00 | |||
09:00 60mTalk | Coq’s vibrant ecosystem for verification engineeringInPerson CPP Link to publication | ||
10:00 - 10:15 | |||
10:00 15mDay opening | Welcome & AnnouncementRemote PEPM Zena M. Ariola University of Oregon, Youyou Cong Tokyo Institute of Technology, Fritz Henglein Department of Computer Science, University of Copenhagen (DIKU) and Deon Digital | ||
10:15 - 11:15 | |||
10:15 60mKeynote | Why are partial evaluation and supercompilation still not widely used in practice? Reflections in light of Russian work on metacomputation.Remote PEPM Andrei Klimov Keldysh Institute of Applied Mathematics of Russian Academy of Sciences File Attached | ||
10:20 - 12:00 | Languages, Methods and ToolsPADL at Directors Chair(s): Esra Erdem Sabanci University, Turkey Remote session chair | ||
10:20 25mTalk | Smart Devices and Large Scale Reasoning via ASP: Tools and ApplicationsRemote PADL Kristian Reale Department of Mathematics and Computer Science University of Calabria - DLVSystem S.r.l., Francesco Calimeri University of Calabria, Nicola Leone University of Calabria, Italy, Francesco Ricca University of Calabria, Italy | ||
10:45 25mTalk | Timed Concurrent Language for Argumentation: an Interleaving ApproachRemote PADL Stefano Bistarelli University of Perugia, Maria Chiara Meo University “G. d’Annunzio” of Chieti-Pescara, Carlo Taticchi University of Perugia | ||
11:10 25mTalk | Towards Dynamic Consistency Checking in Goal-directed Predicate Answer Set ProgrammingRemote PADL Joaquín Arias Universidad Rey Juan Carlos, Manuel Carro IMDEA Software Institute and T.U. of Madrid (UPM), Gopal Gupta The University of Texas at Dallas DOI Pre-print File Attached | ||
11:35 25mTalk | Implementing Stable-Unstable Semantics with ASPTOOLS and ClingoRemote PADL Tomi Janhunen Tampere University | ||
10:20 - 11:50 | |||
10:20 90mTutorial | Program Analysis via Graph Reachability: Past, Present, and Future [Part B]InPerson TutorialFest Qirun Zhang Georgia Institute of Technology | ||
10:20 - 11:50 | |||
10:20 30mPaper | Automata-Driven Partial Order Reduction and Guided Search for LTL Model CheckingRemote VMCAI Peter Gjøl Jensen Aalborg University, Denmark, Jiri Srba Aalborg University, Nikolaj Jensen Ulrik Aalborg University, Simon Mejlby Virenfeldt Aalborg University | ||
10:50 30mPaper | Stateful Dynamic Partial Order Reduction for Model Checking Event-Driven Applications that Do Not TerminateRemote VMCAI Rahmadi Trimananda University of California at Irvine, USA, Weiyu Luo University of California, Irvine, Brian Demsky University of California at Irvine, Harry Xu University of California, Los Angeles (UCLA) Link to publication DOI Pre-print Media Attached File Attached | ||
11:20 30mPaper | Scaling Up Livelock Verification for Network-on-Chip Routing AlgorithmsInPerson VMCAI | ||
10:20 - 12:00 | |||
10:20 25mTalk | Specification and Verification of a Transient StackDistinguished Paper AwardRemote CPP DOI Pre-print Media Attached File Attached | ||
10:45 25mTalk | Mechanized Verification of a Fine-Grained Concurrent Queue from Meta’s Folly LibraryRemote CPP Simon Friis Vindum Aarhus University, Lars Birkedal Aarhus University, Daniel Frumin University of Groningen Pre-print Media Attached | ||
11:10 25mTalk | Applying Formal Verification to Microkernel IPC at MetaInPerson CPP Quentin Carbonneaux Meta, Noam Zilberstein Cornell University, Christoph Klee Facebook, Peter W. O'Hearn Meta; University College London, Francesco Zappa Nardelli Meta Pre-print | ||
11:35 25mTalk | Certified Abstract Machines for Skeletal SemanticsRemote CPP Pre-print Media Attached | ||
11:35 - 12:35 | Contributed Talks 1PEPM at PEPM Chair(s): Antonina Nepeivoda Program Systems Institute of RAS, Russia | ||
11:35 30mTalk | Partially Evaluating Symbolic Interpreters for AllRemote PEPM File Attached | ||
12:05 30mTalk | Parallel Algebraic Effect HandlersRemote PEPM Ningning Xie University of Toronto, Daniel D. Johnson Google Research, Dougal Maclaurin Google Research, Adam Paszke Google Research File Attached | ||
12:55 - 13:55 | |||
12:55 60mKeynote | From meta frameworks and transformations to distributed computing and moreRemote PEPM Y. Annie Liu Stony Brook University | ||
13:30 - 14:45 | Answer Set ProgrammingPADL at Directors Chair(s): Martin Gebser University of Klagenfurt, Austria Remote session chair | ||
13:30 25mTalk | Modelling the Outlier Detection Problem in QASPRemote PADL Pierpaolo Bellusci University of Calabria, Giuseppe Mazzotta University of Calabria, Fracesco Ricca University of Calabria | ||
13:55 25mTalk | Multi-Agent Pick and Delivery with Capacities: Action Planning vs Path FindingRemote PADL Nima Tajelipirbazari TED University, Çağrı Uluç Yıldırımoğlu Sabanci University, Orkunt Sabuncu TED University, Ali Can Arıcı Ekol Logistics, İdil Helin Özen Ekol Logistics, Volkan Patoğlu Sabanci University, Esra Erdem Sabanci University, Turkey | ||
14:20 25mTalk | Determining Action Reversibility in STRIPS Using Answer Set Programming with QuantifiersRemote PADL Wolfgang Faber University of Klagenfurt, Michael Morak University of Klagenfurt, Lukas Chrpa Czech Technical University in Prague | ||
13:30 - 14:30 | |||
13:30 60mTutorial | Formal Methods and Deep Learning [Part A]Remote TutorialFest Matthew Mirman ETH Zurich | ||
13:30 - 14:30 | |||
13:30 30mPaper | Fanoos: Multi-Resolution, Multi-Strength, Interactive Explanations for Learned SystemsRemote VMCAI David Bayani Carnegie Mellon University's School of Computer Science, Stefan Mitsch Carnegie Mellon University, USA | ||
14:00 30mPaper | Bisimulations for Neural Network ReductionInPerson VMCAI Pavithra Prabhakar Kansas State University | ||
14:15 - 15:15 | |||
14:15 60mKeynote | Modal Logics and Types: Looking Back and Looking ForwardRemote PEPM Frank Pfenning Carnegie Mellon University, USA | ||
15:00 - 16:30 | |||
15:00 90mTutorial | Formal Methods and Deep Learning [Part B]InPerson TutorialFest Gagandeep Singh University of Illinois at Urbana-Champaign; VMware | ||
15:05 - 16:35 | |||
15:05 30mPaper | High Assurance Software for Financial Regulation and Business PlatformsRemote VMCAI Stephen Goldbaum Morgan Stanley, Attila Mihaly Morgan Stanley, Tosha Ellison Fintech Open Source Foundation, Earl Barr UCL, Mark Marron Microsoft Research | ||
15:35 30mPaper | Loop Verification with Invariants and ContractsRemote VMCAI Gidon Ernst Ludwig Maximilian University of Munich Pre-print | ||
16:05 30mPaper | Making PROGRESS in Property Directed ReachabilityRemote VMCAI Tobias Seufert University of Freiburg, Christoph Scholl University of Freiburg, Arun Chandrasekharan OneSpin Solutions, Munich, Sven Reimer OneSpin Solutions, Munich, Tobias Welp OneSpin Solutions, Munich | ||
15:30 - 17:10 | Security and Distributed SystemsCPP at Salon III Chair(s): Alwyn Goodloe NASA Langley Research Center | ||
15:30 25mTalk | Reflection, Rewinding, and Coin-Toss in EasyCryptRemote CPP Pre-print Media Attached | ||
15:55 25mTalk | A verified algebraic representation of Cairo program executionRemote CPP Jeremy Avigad Carnegie Mellon University, USA, Lior Goldberg Starkware Industries Ltd., David Levit Starkware Industries Ltd., Yoav Seginer cdl-lang.org, Netherlands, Alon Titelman Starkware Industries Ltd. Pre-print | ||
16:20 25mTalk | Formal Verification of a Distributed Dynamic Reconfiguration ProtocolInPerson CPP William Schultz Northeastern University, Ian Dardik Northeastern University, Stavros Tripakis Northeastern University Pre-print | ||
16:45 25mTalk | Forward build systems, formallyInPerson CPP Link to publication | ||
17:30 - 18:30 | |||
17:30 60mTalk | The seL4 verification: the art and craft of proof and the reality of commercial supportRemote CPP Media Attached | ||
Tue 18 JanDisplayed time zone: Eastern Time (US & Canada) change
Tue 18 Jan
Displayed time zone: Eastern Time (US & Canada) change
04:00 - 05:00 | |||
04:00 60mKeynote | On Type-Based Techniques for Program ManipulationRemote PEPM Naoki Kobayashi University of Tokyo, Japan | ||
05:20 - 06:35 | |||
05:20 45mTalk | Two-level Just-in-Time Compilation with One Interpreter and One EngineRemote PEPM Yusuke Izawa Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology, CF Bolz-Tereick Heinrich-Heine-Universität Düsseldorf Pre-print Media Attached File Attached | ||
06:05 30mTalk | let (rec) insertion without Effects, Lights or MagicRemote PEPM Pre-print | ||
06:55 - 07:55 | |||
06:55 60mKeynote | A partial history of partial evaluationRemote PEPM Peter Sestoft IT University of Copenhagen | ||
08:15 - 09:15 | |||
08:15 30mTalk | Semi-Automatic Ladderisation: Improving Code Security through Rewriting and Dependent TypesRemote PEPM Christopher Brown University of St. Andrews, UK, Adam D. Barwell Imperial College London, UK, Yoann Marquer INRIA, Rennes, France, Olivier Zendra INRIA, Rennes, France, Tania Richmond INRIA, Rennes, France then DGA - Maîtrise de l’Information, Chen Gu Hefei University of Technology, China Link to publication | ||
08:45 30mTalk | Dependent tagless finalRemote PEPM Nicolas Biri Luxembourg Institute of Science and Technology Link to publication | ||
09:00 - 10:00 | Invited talkPADL at Directors Chair(s): Antonio Brogi Università di Pisa, Simona Perri University of Calabria, Italy Remote session chair | ||
09:00 60mKeynote | Declarative Programming and EducationRemote PADL Shriram Krishnamurthi Brown University, United States | ||
09:00 - 10:00 | |||
09:00 20mDay opening | Welcome by POPL 2022 Program ChairRemote PLMW Hongseok Yang KAIST | ||
09:25 35mTalk | Automatically Synthesising Programs that We Can TrustRemote PLMW Ilya Sergey National University of Singapore | ||
09:00 - 10:00 | |||
09:00 30mPaper | Gradient-Descent for Randomized Controllers under Partial ObservabilityInPerson VMCAI Jip Spel RWTH Aachen University, Linus Heck RWTH Aachen University, Sebastian Junges University of California, Berkeley, Joshua Moerman Open University of the Netherlands, Joost-Pieter Katoen RWTH Aachen University | ||
09:30 30mPaper | Satisfiability and Synthesis Modulo OraclesRemote VMCAI Elizabeth Polgreen University of Edinburgh, Andrew Reynolds University of Iowa, Sanjit Seshia UC Berkeley | ||
09:00 - 10:00 | |||
09:00 60mTalk | Structural Embeddings RevisitedRemote CPP | ||
10:20 - 12:00 | Declarative SolutionsPADL at Directors Chair(s): Francesco Calimeri University of Calabria Remote session chair | ||
10:20 25mTalk | Green Application Placement in the Cloud-IoT ContinuumRemote PADL | ||
10:45 25mTalk | Decomposition-based job-shop scheduling with constrained clusteringRemote PADL Mohammed M. S. El-Kholany University of Klagenfurt, Martin Gebser University of Klagenfurt, Austria, Konstantin Schekotihin Alpen-Adria Universit�t Klagenfurt | ||
11:10 25mTalk | Modeling and Verification of Real-Time Systems with the Event Calculus and s(CASP)Remote PADL Sarat Chandra Varanasi The University of Texas at Dallas, Joaquín Arias Universidad Rey Juan Carlos, Elmer Salazar The University of Texas at Dallas, Fang Li The University of Texas at Dallas, Kinjal Basu The University of Texas at Dallas, Gopal Gupta The University of Texas at Dallas | ||
11:35 25mTalk | Parallel Declarative Solutions of Sequencing Problems using Multi-valued Decision Diagrams and GPUsRemote PADL | ||
10:20 - 11:10 | |||
10:20 50mTalk | You and Your EnvironmentIn-person PLMW Talia Ringer University of Illinois at Urbana-Champaign | ||
10:20 - 11:50 | |||
10:20 30mPaper | Out of Control: Reducing Probabilistic Models by Control-State EliminationInPerson VMCAI Tobias Winkler RWTH Aachen University, Johannes Lehmann RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University | ||
10:50 30mPaper | STAMINA 2.0: Improving Scalability of Infinite-StateStochastic Model CheckingRemote VMCAI Riley Roberts Utah State University, Thakur Neupane The MathWorks, Inc., Lukas Buecherl University of Colorado, Boulder, Chris Myers University of Colorado, Boulder, Zhen Zhang Utah State University | ||
11:20 30mPaper | EPMC Gets Knowledge in Multi-Agent SystemsRemote VMCAI Chen Fu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Ernst Moritz Hahn University of Twente, Yong Li Institute of Software, Chinese Academy of Sciences, Sven Schewe University of Liverpool, Meng Sun Peking University, Andrea Turrini State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun Zhang Institute of Software, Chinese Academy of Sciences | ||
10:20 - 12:00 | Proof Infrastructure, Rewriting and Automated ReasoningCPP at Salon III Chair(s): Steve Zdancewic University of Pennsylvania | ||
10:20 25mTalk | CertiStr: A Certified String SolverDistinguished Paper AwardRemote CPP Shuanglong Kan TU Kaiserslautern, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Philipp Ruemmer Uppsala University, Micha Schrader Technische Universität Kaiserslautern DOI Pre-print Media Attached | ||
10:45 25mTalk | Safe, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo RewritingRemote CPP Michael Färber Universität Innsbruck, Austria DOI Pre-print Media Attached File Attached | ||
11:10 25mTalk | An Extension of the Framework Types-To-Sets for Isabelle/HOLRemote CPP Pre-print Media Attached | ||
11:35 25mTalk | A Drag-and-Drop Proof TacticRemote CPP Benjamin Werner Ecole polytechnique, Pablo Donato Ecole polytechnique, Pierre-Yves Strub Ecole Polytechnique DOI Pre-print Media Attached | ||
11:10 - 12:00 | Morning 3 (live only, no recording)PLMW at Independence Chair(s): Stephanie Balzer Carnegie Mellon University | ||
11:10 50mPanel | Panel (live only, no recording)Hybrid PLMW François Pottier Inria, Azadeh Farzan University of Toronto, Henry DeYoung CMU, Wen Kokke University of Edinburgh, Stephanie Weirich University of Pennsylvania, Ralf Jung MPI-SWS | ||
13:30 - 14:45 | |||
13:30 25mTalk | Graph-based Interpretation of Normal Logic ProgramsRemote PADL Fang Li The University of Texas at Dallas, Elmer Salazar The University of Texas at Dallas, Gopal Gupta The University of Texas at Dallas | ||
13:55 25mTalk | Functional Programming on Top of SQL EnginesRemote PADL Tobias Burghardt University of Tübingen, Denis Hirn University of Tübingen, Torsten Grust University of Tübingen | ||
14:20 25mTalk | CircuitFlow: : A Domain Specific Language for Dataflow ProgrammingIn-Person PADL Riley Evans University of Bristol, Samantha Frohlich University of Bristol, Meng Wang University of Bristol | ||
13:30 - 14:45 | |||
13:30 35mTalk | Implementing Languages for Fun and ProfitRemote PLMW | ||
14:10 35mTalk | Writing Valuable PapersRemote PLMW Liam O'Connor University of Edinburgh | ||
13:30 - 14:30 | Invited TalkVMCAI at Salon I Chair(s): Bernd Finkbeiner CISPA Helmholtz Center for Information Security | ||
13:30 60mKeynote | Simplifying Concurrent Programming via Synchronization SynthesisRemote VMCAI Işıl Dillig University of Texas at Austin | ||
13:30 - 15:10 | Formalization of Logic, Algebra and GeometryCPP at Salon III Chair(s): Andrei Popescu University of Sheffield | ||
13:30 25mTalk | Semantic cut elimination for the logic of bunched implications, formalized in CoqDistinguished Paper AwardRemote CPP Daniel Frumin University of Groningen Pre-print Media Attached | ||
13:55 25mTalk | Undecidability, Incompleteness, and Completeness of Second-Order Logic in CoqRemote CPP Pre-print | ||
14:20 25mTalk | Formalising Lie algebrasRemote CPP Oliver Nash Imperial College, London Pre-print Media Attached | ||
14:45 25mTalk | A Machine-Checked Direct Proof of the Steiner-Lehmus TheoremInPerson CPP Ariel E. Kellison Cornell University Pre-print | ||
15:05 - 16:20 | |||
15:05 35mTalk | Proving and ProgrammingRemote PLMW Zena M. Ariola University of Oregon | ||
15:45 35mTalk | Finding a research topic (or being found by a research topic?)Remote PLMW Alexandra Silva Cornell University | ||
15:05 - 16:35 | |||
15:05 15mTalk | Towards a Syntactic Model of Sized Dependent Types Student Research Competition Jonathan Chan University of British Columbia (UBC) Media Attached | ||
15:20 15mTalk | Dependent-Type-Preserving Memory Allocation Student Research Competition Paulette Koronkevich University of British Columbia | ||
15:35 15mTalk | Linearity, Uniqueness, Ownership: An Entente Cordiale Student Research Competition Danielle Marshall University of Kent, UK Media Attached | ||
15:50 15mTalk | CapableWasm: Bringing Better Interop Down to WebAssembly Student Research Competition | ||
16:05 15mTalk | Filling a Niche: Using Spare Bits to Optimize Data Representations Student Research Competition | ||
16:20 15mTalk | A Realizability Model for Interoperability Between Languages with Garbage-Collected and Manually Managed Memory Student Research Competition Noble Mushtak Northeastern University | ||
15:05 - 16:05 | |||
15:05 30mPaper | Fast Three-Valued Abstract Bit-Vector ArithmeticInPerson VMCAI | ||
15:35 30mPaper | Mixed Semantics Guided Layered Bounded Reachability Analysis of Compositional Linear Hybrid AutomataRemote VMCAI Yuming Wu Nanjing University, Lei Bu Nanjing University, Jiawan Wang Nanjing University, Xinyue Ren Nanjing University, Wen Xiong Nanjing University, Xuandong Li Nanjing University | ||
15:30 - 16:10 | Chairs' Report and Business MeetingCPP at Salon III Chair(s): Lennart Beringer Princeton University, Robbert Krebbers Radboud University Nijmegen, Andrei Popescu University of Sheffield, Steve Zdancewic University of Pennsylvania | ||
15:30 40mTalk | Chairs' Report CPP File Attached | ||
16:30 - 18:10 | Category Theory, HoTT, Number TheoryCPP at Salon III Chair(s): Kuen-Bang Hou (Favonia) University of Minnesota | ||
16:30 25mTalk | Implementing a category-theoretic framework for typed abstract syntaxRemote CPP Benedikt Ahrens TU Delft, The Netherlands, Ralph Matthes IRIT, Université de Toulouse, CNRS, Toulouse INP, UT3, Toulouse, Anders Mörtberg Department of Mathematics, Stockholm University DOI Pre-print Media Attached | ||
16:55 25mTalk | (Deep) Induction Rules for GADTsRemote CPP Pre-print Media Attached | ||
17:20 25mTalk | On homotopy of walks and spherical maps in homotopy type theoryRemote CPP Jonathan Prieto-Cubides University of Bergen Pre-print Media Attached | ||
17:45 25mTalk | Windmills of the minds: an algorithm for Fermat's Two Squares TheoremRemote CPP Hing Lun Chan Australian National University DOI Pre-print Media Attached File Attached | ||
Wed 19 JanDisplayed time zone: Eastern Time (US & Canada) change
Wed 19 Jan
Displayed time zone: Eastern Time (US & Canada) change
08:50 - 09:00 | |||
09:00 - 10:00 | |||
09:00 60mKeynote | Principles of Programming Language TranslatorsRemoteInvited Talk POPL Alfred V. Aho Columbia University | ||
10:00 - 10:20 | SIGPLAN CARESDiversity, Equity and Inclusion at Salon II Chair(s): Stephanie Weirich University of Pennsylvania Only in person | ||
10:20 - 12:00 | |||
10:20 25mResearch paper | Software Model-Checking as Cyclic-Proof SearchRemote POPL DOI Media Attached | ||
10:45 25mResearch paper | Induction Duality: Primal-Dual Search for InvariantsRemote POPL Oded Padon VMware Research; Stanford University, James R. Wilcox Certora, Jason R. Koenig Stanford University, Kenneth L. McMillan University of Texas at Austin, Alex Aiken Stanford University DOI Media Attached | ||
11:10 25mResearch paper | Solving Constrained Horn Clauses Modulo Algebraic Data Types and Recursive FunctionsRemote POPL Hari Govind V K University of Waterloo, Sharon Shoham Tel Aviv University, Arie Gurfinkel University of Waterloo DOI Media Attached | ||
11:35 25mResearch paper | Solving String Constraints with Regex-Dependent Functions through Transducers with Priorities and VariablesRemote POPL Taolue Chen Birkbeck University of London, Alejandro Flores Lamas Royal Holloway University of London, Matthew Hague Royal Holloway University of London, Zhilei Han Tsinghua University, Denghang Hu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Shuanglong Kan TU Kaiserslautern, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS, Philipp Ruemmer Uppsala University, Zhilin Wu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences DOI Media Attached | ||
10:20 - 12:00 | |||
10:20 25mTalk | A Separation Logic for Heap Space under Garbage CollectionRemote POPL DOI Media Attached | ||
10:45 25mResearch paper | Simuliris: A Separation Logic Framework for Verifying Concurrent Program OptimizationsDistinguished PaperRemote POPL Lennard Gäher MPI-SWS, Michael Sammler MPI-SWS, Simon Spies MPI-SWS, Ralf Jung MPI-SWS, Hoang-Hai Dang MPI-SWS, Robbert Krebbers Radboud University Nijmegen, Jeehoon Kang KAIST, Derek Dreyer MPI-SWS DOI Media Attached | ||
11:10 25mResearch paper | Concurrent Incorrectness Separation LogicRemote POPL Azalea Raad Imperial College London, Josh Berdine Meta, Derek Dreyer MPI-SWS, Peter W. O'Hearn Meta; University College London DOI Media Attached | ||
11:35 25mResearch paper | On Incorrectness Logic and Kleene Algebra with Top and TestsInPerson POPL Cheng Zhang Boston University, Arthur Azevedo de Amorim Boston University, Marco Gaboardi Boston University DOI Media Attached | ||
12:00 - 13:30 | |||
13:30 - 14:45 | Program AnalysisPOPL at Salon I Chair(s): Gagandeep Singh University of Illinois at Urbana-Champaign; VMware | ||
13:30 25mResearch paper | Property-Directed Reachability as Abstract Interpretation in the Monotone TheoryRemote POPL Yotam M. Y. Feldman Tel Aviv University, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv University, James R. Wilcox Certora DOI Media Attached | ||
13:55 25mResearch paper | Partial (In)Completeness in Abstract Interpretation: Limiting the Imprecision in Program AnalysisInPerson POPL Marco Campion University of Verona, Mila Dalla Preda University of Verona, Roberto Giacobazzi University of Verona DOI Media Attached | ||
14:20 25mResearch paper | Return of CFA: Call-Site Sensitivity Can Be Superior to Object Sensitivity Even for Object-Oriented ProgramsInPerson POPL DOI Media Attached | ||
13:30 - 14:45 | |||
13:30 25mResearch paper | The Leaky Semicolon: Compositional Semantic Dependencies for Relaxed-Memory ConcurrencyInPerson POPL Alan Jeffrey Roblox, James Riely DePaul University, Mark Batty University of Kent, Simon Cooksey University of Kent, Ilya Kaysin JetBrains Research; University of Cambridge, Anton Podkopaev HSE University DOI Media Attached | ||
13:55 25mResearch paper | Extending Intel-x86 Consistency and Persistency: Formalising the Semantics of Intel-x86 Memory Types and Non-temporal StoresRemote POPL DOI Media Attached | ||
14:20 25mResearch paper | Truly Stateless, Optimal Dynamic Partial Order ReductionRemote POPL Michalis Kokologiannakis MPI-SWS, Iason Marmanis MPI-SWS, Vladimir Gladstein MPI-SWS; St. Petersburg University; JetBrains Research, Viktor Vafeiadis MPI-SWS DOI Media Attached | ||
15:05 - 16:20 | |||
15:05 25mResearch paper | Efficient Algorithms for Dynamic Bidirected Dyck-ReachabilityRemote POPL Yuanbo Li Georgia Institute of Technology, Kris Satya Georgia Institute of Technology, Qirun Zhang Georgia Institute of Technology DOI Media Attached | ||
15:30 25mResearch paper | The Decidability and Complexity of Interleaved Bidirected Dyck ReachabilityRemote POPL DOI Media Attached | ||
15:55 25mResearch paper | Subcubic Certificates for CFL ReachabilityRemote POPL DOI Media Attached | ||
15:05 - 16:20 | |||
15:05 25mResearch paper | Visibility Reasoning for Concurrent Snapshot AlgorithmsRemote POPL Joakim Öhman IMDEA Software Institute; Universidad Politécnica de Madrid, Aleksandar Nanevski IMDEA Software Institute DOI Media Attached | ||
15:30 25mResearch paper | Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation LogicRemote POPL Jules Jacobs Radboud University Nijmegen, Stephanie Balzer Carnegie Mellon University, Robbert Krebbers Radboud University Nijmegen DOI Media Attached | ||
15:55 25mResearch paper | Static Prediction of Parallel Computation GraphsInPerson POPL Stefan K. Muller Illinois Institute of Technology DOI Media Attached | ||
16:40 - 17:30 | |||
16:40 25mResearch paper | Context-Bounded Verification of Thread PoolsRemote POPL Pascal Baumann MPI-SWS, Rupak Majumdar MPI-SWS, Ramanathan S. Thinniyam MPI-SWS, Georg Zetzsche MPI-SWS DOI Media Attached | ||
17:05 25mResearch paper | What’s Decidable about Linear Loops?InPerson POPL Toghrul Karimov MPI-SWS, Engel Lefaucheux MPI-SWS, Joël Ouaknine MPI-SWS, David Purser MPI-SWS, Anton Varonka MPI-SWS, Markus A. Whiteland MPI-SWS, James Worrell University of Oxford DOI Pre-print Media Attached | ||
16:40 - 17:30 | Reasoning about Probabilistic Programs and AlgorithmsPOPL at Salon III Chair(s): Armando Solar-Lezama Massachusetts Institute of Technology | ||
16:40 25mResearch paper | A Separation Logic for Negative DependenceRemote POPL Jialu Bao Cornell University, Marco Gaboardi Boston University, Justin Hsu Cornell University, Joseph Tassarotti Boston College DOI Media Attached | ||
17:05 25mResearch paper | Reasoning about “Reasoning about Reasoning”: Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and RecursionRemote POPL DOI Media Attached | ||
Thu 20 JanDisplayed time zone: Eastern Time (US & Canada) change
Thu 20 Jan
Displayed time zone: Eastern Time (US & Canada) change
08:00 - 09:00 | Junior Faculty Mentoring BreakfastDiversity, Equity and Inclusion at Independence Chair(s): Michael Hicks University of Maryland at College Park Only in person | ||
09:00 - 10:00 | |||
09:00 60mKeynote | Better Learning through Programming LanguagesInvited TalkInPerson POPL Armando Solar-Lezama Massachusetts Institute of Technology | ||
10:20 - 12:00 | Foundation and Verification of Machine-Learning SystemsPOPL at Salon I Chair(s): Gilbert Bernstein University of California at Berkeley | ||
10:20 25mResearch paper | A Dual Number Abstraction for Static Analysis of Clarke JacobiansInPerson POPL Jacob Laurel University of Illinois at Urbana-Champaign, Rem Yang University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware, Sasa Misailovic University of Illinois at Urbana-Champaign DOI Media Attached | ||
10:45 25mResearch paper | Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic DifferentiationRemote POPL Faustyna Krawiec University of Cambridge, Simon Peyton Jones Microsoft Research, Neel Krishnaswami University of Cambridge, Tom Ellis Microsoft Research, Richard A. Eisenberg Tweag, Andrew Fitzgibbon Graphcore DOI Media Attached | ||
11:10 25mResearch paper | Interval Universal Approximation for Neural NetworksInPerson POPL Zi Wang University of Wisconsin-Madison, Aws Albarghouthi University of Wisconsin-Madison, Gautam Prakriya Chinese University of Hong Kong, Somesh Jha University of Wisconsin DOI Media Attached | ||
11:35 25mResearch paper | PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull ApproximationsInPerson POPL Mark Niklas Müller ETH Zurich, Gleb Makarchuk ETH Zurich, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware, Markus Püschel ETH Zurich, Martin Vechev ETH Zurich DOI Media Attached | ||
10:20 - 12:00 | |||
10:20 25mResearch paper | Quantum Information EffectsRemote POPL DOI Media Attached | ||
10:45 25mResearch paper | Twist: Sound Reasoning for Purity and Entanglement in Quantum ProgramsInPerson POPL Charles Yuan Massachusetts Institute of Technology, Christopher McNally Massachusetts Institute of Technology, Michael Carbin Massachusetts Institute of Technology DOI Media Attached | ||
11:10 25mResearch paper | A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation LogicRemote POPL Xuan-Bach Le Nanyang Technological University, Shang-Wei Lin Nanyang Technological University, Jun Sun Singapore Management University, David Sanan Nanyang Technological University DOI Media Attached | ||
11:35 25mResearch paper | Semantics for Variational Quantum ProgrammingRemote POPL Xiaodong Jia Hunan University, Andre Kornell Tulane University, Bert Lindenhovius JKU Linz, Michael Mislove Tulane University, Vladimir Zamdzhiev Inria DOI Media Attached | ||
12:00 - 13:30 | |||
13:30 - 14:45 | |||
13:30 25mResearch paper | On Type-Cases, Union Elimination, and Occurrence TypingInPerson POPL Giuseppe Castagna CNRS; Université de Paris, Mickaël Laurent Université de Paris, Kim Nguyễn Université Paris-Saclay, Matthew Lutze Université de Paris DOI Media Attached | ||
13:55 25mResearch paper | Oblivious Algebraic Data TypesInPerson POPL DOI Media Attached | ||
14:20 25mResearch paper | SolType: Refinement Types for Arithmetic Overflow in SolidityRemote POPL Bryan Tan University of California at Santa Barbara, Benjamin Mariano University of Texas at Austin, Shuvendu K. Lahiri Microsoft Research, Işıl Dillig University of Texas at Austin, Yu Feng University of California at Santa Barbara DOI Media Attached | ||
13:30 - 14:45 | Dynamic AnalysisPOPL at Salon III Chair(s): Armando Solar-Lezama Massachusetts Institute of Technology | ||
13:30 25mResearch paper | A Formal Foundation for Symbolic Evaluation with MergingRemote POPL Sorawee Porncharoenwase University of Washington, Luke Nelson University of Washington, Xi Wang University of Washington, Emina Torlak University of Washington DOI Media Attached | ||
13:55 25mResearch paper | Logarithm and Program TestingInPerson POPL DOI Media Attached | ||
14:20 25mResearch paper | Profile Inference RevisitedRemote POPL Wenlei He Facebook, Julián Mestre Facebook; University of Sydney, Sergey Pupyrev , Lei Wang Facebook, Hongtao Yu Facebook DOI Media Attached | ||
15:05 - 16:20 | |||
15:05 25mResearch paper | Isolation without Taxation: Near-Zero-Cost Transitions for WebAssembly and SFIInPerson POPL Matthew Kolosick University of California at San Diego, Shravan Ravi Narayan University of California at San Diego, Evan Johnson University of California at San Diego, Conrad Watt University of Cambridge, Michael LeMay Intel Labs, Deepak Garg MPI-SWS, Ranjit Jhala University of California at San Diego, Deian Stefan University of California at San Diego DOI Media Attached | ||
15:30 25mResearch paper | Relational E-matchingRemote POPL Yihong Zhang University of Washington, Yisu Remy Wang University of Washington, Max Willsey University of Washington, Zachary Tatlock University of Washington DOI Media Attached | ||
15:55 25mResearch paper | Linked Visualisations via Galois DependenciesRemote POPL Roly Perera Alan Turing Institute, Minh Nguyen University of Bristol, Tomas Petricek University of Kent, Meng Wang University of Bristol DOI Media Attached | ||
15:05 - 16:20 | |||
15:05 25mResearch paper | Staging with Class: A Specification for Typed Template HaskellInPerson POPL Ningning Xie University of Toronto, Matthew Pickering Well-Typed LLP, Andres Löh Well-Typed LLP, Nicolas Wu Imperial College London, Jeremy Yallop University of Cambridge, Meng Wang University of Bristol DOI Media Attached | ||
15:30 25mResearch paper | Mœbius: Metaprogramming using Contextual Types: The Stage Where System F Can Pattern Match on ItselfRemote POPL Junyoung Jang McGill University, Samuel Gélineau SimSpace, Stefan Monnier Université de Montréal, Brigitte Pientka McGill University DOI Media Attached | ||
15:55 25mResearch paper | Type-Level Programming with Match TypesRemote POPL Olivier Blanvillain EPFL, Jonathan Immanuel Brachthäuser University of Tübingen, Maxime Kjaer EPFL, Martin Odersky EPFL DOI Media Attached | ||
Fri 21 JanDisplayed time zone: Eastern Time (US & Canada) change
Fri 21 Jan
Displayed time zone: Eastern Time (US & Canada) change
08:00 - 09:00 | Graduating PhDs / Postdocs Mentoring BreakfastDiversity, Equity and Inclusion at Independence Chair(s): Andrew Myers Cornell University Only in person | ||
09:00 - 10:00 | |||
09:00 60mKeynote | Coalgebra for the working programming languages researcherRemoteInvited Talk POPL Alexandra Silva Cornell University | ||
10:20 - 12:00 | |||
10:20 25mResearch paper | Pirouette: Higher-Order Typed Functional ChoreographiesDistinguished PaperInPerson POPL DOI Media Attached | ||
10:45 25mResearch paper | Fair Termination of Binary SessionsRemote POPL DOI Media Attached | ||
11:10 25mResearch paper | Safe, Modular Packet Pipeline ProgrammingRemote POPL DOI Media Attached | ||
11:35 25mResearch paper | Dependently-Typed Data Plane ProgrammingRemote POPL Matthias Eichholz TU Darmstadt, Eric Campbell Cornell University, Matthias Krebs TU Darmstadt, Nate Foster Cornell University, Mira Mezini TU Darmstadt DOI Media Attached | ||
10:20 - 12:00 | |||
10:20 25mResearch paper | From Enhanced Coinduction towards Enhanced InductionRemote POPL Davide Sangiorgi University of Bologna; Inria DOI Media Attached | ||
10:45 25mResearch paper | A Fine-Grained Computational Interpretation of Girard’s Intuitionistic Proof-NetsInPerson POPL Delia Kesner Université de Paris; CNRS; IRIF; Institut Universitaire de France DOI Media Attached | ||
11:10 25mResearch paper | Fully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logical RelationsRemote POPL Ohad Kammar University of Edinburgh, Shin-ya Katsumata National Institute of Informatics, Philip Saville University of Oxford DOI Media Attached | ||
11:35 25mResearch paper | Layered and Object-Based Game SemanticsInPerson POPL Arthur Oliveira Vale Yale University, Paul-André Melliès CNRS; Université de Paris, Zhong Shao Yale University, Jérémie Koenig Yale University, Leo Stefanesco IRIF, University Paris Diderot & CNRS DOI Media Attached | ||
12:30 - 13:30 | |||
12:30 60mTalk | Designing and Developing for the Black ExperienceRemote Diversity, Equity and Inclusion Brittany Johnson George Mason University | ||
13:30 - 14:45 | |||
13:30 25mTalk | Armed cats: formal concurrency modelling at ArmRemote POPL Jade Alglave University College London, Will Deacon ARM Ltd., Richard Grisenthwaite , Antoine Hacquard EPITA, LRDE, Luc Maranget Inria | ||
13:55 25mTalk | TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs Remote POPL Emanuele D’Osualdo MPI-SWS, Julian Sutherland Imperial College London, Azadeh Farzan University of Toronto, Philippa Gardner Imperial College London DOI | ||
14:20 25mTalk | Gradualizing the Calculus of Inductive ConstructionsRemote POPL Meven Lennon-Bertrand Inria – LS2N, Université de Nantes, Kenji Maillard Inria Nantes & University of Chile, Nicolas Tabareau Inria, Éric Tanter University of Chile | ||
13:30 - 14:45 | |||
13:30 25mResearch paper | Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming LanguagesInPerson POPL Vikraman Choudhury Indiana University; University of Cambridge, Jacek Karwowski University of Warsaw, Amr Sabry Indiana University Link to publication DOI Media Attached | ||
13:55 25mResearch paper | A Relational Theory of Effects and CoeffectsRemote POPL DOI Media Attached | ||
14:20 25mResearch paper | Effectful Program DistancingRemote POPL DOI Media Attached | ||
14:45 - 15:05 | SIGPLAN CARESDiversity, Equity and Inclusion at Salon II Chair(s): Stephanie Weirich University of Pennsylvania Only in person | ||
15:05 - 16:20 | |||
15:05 25mResearch paper | Certifying Derivation of State Machines from CoroutinesInPerson POPL Mirai Ikebuchi National Institute of Informatics, Andres Erbsen Massachusetts Institute of Technology, Adam Chlipala Massachusetts Institute of Technology DOI Media Attached | ||
15:30 25mResearch paper | VIP: Verifying Real-World C Idioms with Integer-Pointer CastsRemote POPL Rodolphe Lepigre MPI-SWS, Michael Sammler MPI-SWS, Kayvan Memarian University of Cambridge, Robbert Krebbers Radboud University Nijmegen, Derek Dreyer MPI-SWS, Peter Sewell University of Cambridge DOI Media Attached | ||
15:55 25mResearch paper | Verified Compilation of C Programs with a Nominal Memory ModelRemote POPL Yuting Wang Shanghai Jiao Tong University, Ling Zhang Shanghai Jiao Tong University, Zhong Shao Yale University, Jérémie Koenig Yale University DOI Media Attached | ||
15:05 - 16:20 | |||
15:05 25mResearch paper | A Cost-Aware Logical FrameworkInPerson POPL Yue Niu Carnegie Mellon University, Jonathan Sterling Aarhus University, Harrison Grodin Carnegie Mellon University, Robert Harper Carnegie Mellon University DOI Media Attached | ||
15:30 25mResearch paper | Formal Metatheory of Second-Order Abstract SyntaxDistinguished PaperRemote POPL DOI Media Attached | ||
15:55 25mResearch paper | Observational Equality: Now for GoodDistinguished PaperRemote POPL DOI Media Attached | ||
16:40 - 17:30 | |||
16:40 25mResearch paper | Verified Tensor-Program Optimization Via High-Level Scheduling RewritesRemote POPL Amanda Liu Massachusetts Institute of Technology, Gilbert Bernstein University of California at Berkeley, Adam Chlipala Massachusetts Institute of Technology, Jonathan Ragan-Kelley Massachusetts Institute of Technology DOI Media Attached | ||
17:05 25mResearch paper | One Polynomial Approximation to Produce Correctly Rounded Results of an Elementary Function for Multiple Representations and Rounding ModesDistinguished PaperRemote POPL DOI Media Attached | ||
16:40 - 17:30 | |||
16:40 25mResearch paper | Learning Formulas in Finite Variable LogicsDistinguished PaperInPerson POPL Paul Krogmeier University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign DOI Media Attached | ||
17:05 25mResearch paper | Bottom-Up Synthesis of Recursive Functional Programs using Angelic ExecutionDistinguished PaperRemote POPL Anders Miltner University of Texas at Austin, Adrian Trejo Nuñez University of Texas at Austin, Ana Brendel University of Texas at Austin, Swarat Chaudhuri University of Texas at Austin, Işıl Dillig University of Texas at Austin DOI Media Attached | ||
Sat 22 JanDisplayed time zone: Eastern Time (US & Canada) change
Sat 22 Jan
Displayed time zone: Eastern Time (US & Canada) change
09:00 - 10:00 | |||
09:00 60mKeynote | BPF and Spectre: Mitigating transient execution attacksRemote PriSC Piotr Krysiuk Symantec, Threat Hunter Team, Benedict Schlüter Ruhr University Bochum, Daniel Borkmann Isovalent File Attached | ||
09:00 - 10:00 | |||
09:00 60mKeynote | Coq meets literate programming: tools for documenting, preserving, and sharing mechanized proofsRemote CoqPL | ||
09:00 - 10:00 | |||
09:00 15mTalk | CN: A Refinement Type System for CRemote WITS Christopher Pulte University of Cambridge, UK, Dhruv Makwana University of Cambridge, Kayvan Memarian University of Cambridge, Jean Pichon-Pharabod Aarhus University, Peter Sewell University of Cambridge, Neel Krishnaswami University of Cambridge | ||
09:15 45mOther | Type-aware equational rewriting (discussion)In-Person WITS Richard A. Eisenberg Tweag | ||
09:15 45mOther | Multi case trees: confluence and coverage (discussion)In-Person WITS Tesla Zhang The Pennsylvania State University | ||
09:15 45mOther | Intrinsically-Typed Interpreters for Effectful and Coeffectful Languages (discussion)Remote WITS Syouki Tsuyama Tokyo Institute of Technology, Youyou Cong Tokyo Institute of Technology, Hidehiko Masuhara Tokyo Institute of Technology File Attached | ||
09:15 45mOther | The Expression Problem and Theorem Proving (discussion)Remote WITS Yao Li University of Pennsylvania, Nick Rioux University of Pennsylvania, Stephanie Weirich University of Pennsylvania | ||
10:20 - 11:35 | |||
10:20 25mTalk | Type-directed Program Transformation for Constant-Time EnforcementRemote PriSC File Attached | ||
10:45 25mTalk | Towards Understanding Spectre-PHT in Memory-Safe LanguagesRemote PriSC Zirui Neil Zhao University of Illinois at Urbana-Champaign, Fangfei Liu Intel Corporation, Scott Constable Intel Corporation, Carlos Rozas Intel Corporation | ||
11:10 25mTalk | Synthesizing Evidence of Emergent ComputationRemote PriSC Media Attached File Attached | ||
10:20 - 12:00 | |||
10:20 20mTalk | A Visual Ltac Debugger in CoqIDERemote CoqPL File Attached | ||
10:40 20mTalk | Scrap your boilerplate definitions in 10 lines of Ltac!InPerson CoqPL File Attached | ||
11:00 20mTalk | Tealeaves: Categorical structures for syntaxInPerson CoqPL S: Lawrence Dunn University of Pennsylvania, Steve Zdancewic University of Pennsylvania, Val Tannen University of Pennsylvania, USA File Attached | ||
11:20 20mTalk | Towards a Formalization of Nominal Sets in CoqRemote CoqPL File Attached | ||
11:40 20mTalk | A Case for Lightweight Interfaces in CoqInPerson CoqPL David Swasey BedRock Systems, Paolo G. Giarrusso BedRock Systems, S: Gregory Malecha BedRock Systems File Attached | ||
10:20 - 12:00 | |||
10:20 45mKeynote | Make Three To Throw Away: Frontiers in Homotopical Proof AssistantsRemote WITS Jonathan Sterling Aarhus University | ||
11:05 15mTalk | The curious case of case: correct & efficient representation of case analysis in Coq and MetaCoqRemote WITS Matthieu Sozeau Inria, Meven Lennon-Bertrand Inria – LS2N, Université de Nantes, Yannick Forster Inria | ||
11:20 40mOther | Elaborator reflection APIs (discussion)Remote WITS Jesper Cockx TU Delft | ||
11:20 40mOther | Invisible arguments: language design (discussion)In-Person WITS Richard A. Eisenberg Tweag | ||
11:35 - 12:00 | |||
13:30 - 14:30 | |||
13:30 60mKeynote | Providing evidence for the security properties of hardware/software codesignsRemote PriSC Frank Piessens KU Leuven File Attached | ||
13:30 - 14:30 | |||
13:30 60mKeynote | Verifying Concurrent, Crash-Safe Systems with PerennialRemote CoqPL | ||
13:30 - 14:45 | |||
13:30 15mTalk | Tries that matchRemote WITS Sebastian Graf Karlsruhe Institute of Technology | ||
13:45 15mTalk | Gotta prove fast: building an ecosystem for effortless native compilation of tacticsRemote WITS Sebastian Ullrich Karlsruhe Institute of Technology | ||
14:00 45mOther | Benchmarking Binding (discussion)In-Person WITS Stephanie Weirich University of Pennsylvania | ||
14:00 45mOther | Fancy module systems (discussion)Remote WITS Jesper Cockx TU Delft | ||
14:30 - 14:50 | |||
14:30 20mTalk | A Verified Pipeline from a Specification Language to Optimized, Safe RustRemote CoqPL S: Rasmus Holdsbjerg-Larsen Aarhus University, Bas Spitters Aarhus University, Mikkel Milo Concordium Blockchain Research Center, Aarhus University Pre-print File Attached | ||
15:05 - 16:20 | |||
15:05 25mTalk | Composing Secure CompilersRemote PriSC Matthis Kruse CISPA Helmholtz Center for Information Security, Marco Patrignani CISPA Helmholtz Center for Information Security / Stanford University File Attached | ||
15:30 25mTalk | SecurePtrs: Proving Secure Compilation with Data-Flow Back-Translation and Turn-Taking SimulationRemote PriSC Akram El-Korashy Max Planck Institute for Software Systems (MPI-SWS), Roberto Blanco Max Planck Institute for Security and Privacy (MPI-SP), Jérémy Thibault MPI-SP, Adrien Durier Max Planck Institute for Security and Privacy (MPI-SP), Cătălin Hriţcu MPI-SP, Deepak Garg MPI-SWS Pre-print Media Attached File Attached | ||
15:55 25mTalk | The Fox and the Hound (Episode 2): Fully Abstract, Robust Compilation and How to Reconcile the Two, AbstractlyRemote PriSC Carmine Abate Max Planck Institute for Security and Privacy, Bochum, Germany, Matteo Busi Università di Pisa - Dipartimento di Informatica, Stelios Tsampas FAU Erlangen-Nuremberg, INF 8 DOI Pre-print File Attached | ||
15:05 - 15:50 | |||
15:05 45mPanel | Session with the Coq Development TeamRemote CoqPL S: Matthieu Sozeau Inria, S: Yves Bertot INRIA, S: Hugo Herbelin , S: Emilio Jesús Gallego Arias INRIA, S: Jason Gross MIT CSAIL | ||
15:05 - 16:20 | |||
15:05 15mTalk | mitten: A Flexible Multimodal Proof AssistantRemote WITS Philipp Stassen Aarhus University, Daniel Gratzer Aarhus University, Lars Birkedal Aarhus University | ||
15:20 15mTalk | Understandable and Useful Error Messages for Liquid TypesRemote WITS Alcides Fonseca LASIGE, Faculdade de Ciências da Universidade de Lisboa, Catarina Gamboa LASIGE, Faculdade de Ciências da Universidade de Lisboa, João David LASIGE, Faculdade de Ciências da Universidade de Lisboa, Guilherme Espada LASIGE, Faculdade de Ciências da Universidade de Lisboa, Paulo Canelas LASIGE, Faculdade de Ciências da Universidade de Lisboa | ||
15:35 15mTalk | Deciding type equivalence with simple grammarsIn-Person WITS Bernardo Almeida LASIGE, Faculty of Sciences, University of Lisbon, Andreia Mordido Lasige / Faculty of Sciences, Universidade de Lisboa, Vasco T. Vasconcelos LASIGE, Faculty of Sciences, University of Lisbon | ||
15:50 15mTalk | Typechecking up to CongruenceIn-Person WITS Jad Elkhaleq Ghalayini University of Cambridge | ||
16:05 15mTalk | À bas l’η — Coq’s troublesome η-conversionRemote WITS Meven Lennon-Bertrand Inria – LS2N, Université de Nantes | ||
16:40 - 17:55 | |||
16:40 25mTalk | A CompCert backend with symbolic encryptionRemote PriSC File Attached | ||
17:05 25mTalk | Effect-Oblivious EquivalenceRemote PriSC Pre-print File Attached | ||
17:30 25mTalk | The Supervisionary proof-checking kernel, or: a work-in-progress toward proof-generating codeRemote PriSC File Attached | ||
16:40 - 17:30 | |||
16:40 15mTalk | Using Dependent Types at Scale: Maintaining the Agda Standard LibraryIn-Person WITS | ||
16:55 15mTalk | Setting the Record Straight with SingletonsRemote WITS Reed Mullanix University of Minnesota | ||
17:10 15mTalk | First-class pattern synonymsIn-Person WITS Tesla Zhang The Pennsylvania State University | ||
Thu 27 JanDisplayed time zone: Eastern Time (US & Canada) change
Thu 27 Jan
Displayed time zone: Eastern Time (US & Canada) change
12:00 - 13:00 | |||
12:00 60mBreak | Break at the Airmeet tables ("Lounge") Virtual Workshop | ||
13:00 - 14:00 | |||
13:00 60mSocial Event | Networking: careers at sponsor companies Virtual Workshop | ||
14:00 - 15:00 | |||
14:00 60mSocial Event | Networking: academic job searches and PhD applications Virtual Workshop | ||
15:00 - 16:00 | |||
15:00 60mPanel | Panel 1: proof assistants for PL and math Virtual Workshop Kevin Buzzard Imperial College London, Kuen-Bang Hou (Favonia) University of Minnesota, Zhong Shao Yale University, Nicolas Tabareau Inria | ||
16:00 - 18:00 | |||
16:00 2hBreak | Unstructured time Virtual Workshop | ||
18:00 - 19:00 | |||
18:00 60mKeynote | Keynote 1: OpenAI Codex presentation & demo Virtual Workshop Łukasz Kaiser OpenAI | ||
19:00 - 20:00 | |||
19:00 60mBreak | Unstructured time Virtual Workshop | ||
20:00 - 21:00 | |||
20:00 60mSocial Event | Mentoring for graduating PhDs and postdocs Virtual Workshop | ||
21:00 - 03:00 | |||
21:00 6hBreak | Unstructured time Virtual Workshop | ||
Fri 28 JanDisplayed time zone: Eastern Time (US & Canada) change
Fri 28 Jan
Displayed time zone: Eastern Time (US & Canada) change
03:00 - 04:00 | |||
03:00 60mPanel | PLMW Panel (on Zoom) Virtual Workshop Youyou Cong Tokyo Institute of Technology, Andreea Costea School of Computing, National University Of Singapore, Cristina Cifuentes Oracle Labs, Sukyoung Ryu KAIST | ||
04:00 - 05:00 | |||
04:00 60mSocial Event | Networking: careers at sponsor companies Virtual Workshop | ||
05:00 - 06:00 | |||
05:00 60mSocial Event | Networking: academic job searches and PhD applications Virtual Workshop | ||
06:00 - 07:00 | |||
06:00 60mTutorial | Tutorial 1: Data-driven program analysis: combining machine learning and program analysis Virtual Workshop Hakjoo Oh Korea University | ||
07:00 - 09:00 | |||
07:00 2hBreak | Unstructured time Virtual Workshop | ||
07:00 2hBreak | Unstructured time Virtual Workshop | ||
09:00 - 10:00 | |||
09:00 60mKeynote | Keynote 2: on WebAssembly Virtual Workshop Andreas Rossberg Dfinity Stiftung | ||
10:00 - 11:00 | |||
10:00 60mBreak | Unstructured time Virtual Workshop | ||
11:00 - 14:00 | |||
11:00 3hBreak | Unstructured time Virtual Workshop | ||
14:00 - 18:00 | |||
14:00 4hBreak | Unstructured time Virtual Workshop | ||
18:00 - 19:00 | |||
18:00 60mSocial Event | Mentoring for junior faculty Virtual Workshop | ||
19:00 - 20:00 | |||
19:00 60mPanel | Panel 2: the future of concurrency and parallelism Virtual Workshop Stephanie Balzer Carnegie Mellon University, Jeehoon Kang KAIST, Keshav Pingali The University of Texas at Austin, Ilya Sergey National University of Singapore | ||
20:00 - 21:00 | |||
20:00 60mSocial Event | Mentoring for junior faculty Virtual Workshop | ||
21:00 - 22:00 | |||
21:00 60mSocial Event | Mentoring for graduating PhDs and postdocs Virtual Workshop | ||
22:00 - 22:59 | |||
22:00 59mTutorial | Tutorial 2: some advanced features of the Dafny verification tool Virtual Workshop K. Rustan M. Leino Amazon | ||