Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sun 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Sun 17 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
07:00 - 08:00 | |||
07:00 60mSocial Event | POPL Card Game POPL Meetups | ||
15:30 - 16:00 | |||
15:30 30mSocial Event | Sunday Breakfast Tables Workshops and Co-located Events | ||
16:00 - 17:00 | Invited TalkCPP at CPP Chair(s): Cătălin Hriţcu MPI-SP Streamed session: https://youtu.be/PAxUO84tUE8 | ||
16:00 60mTalk | Invited Talk: Teaching Algorithms and Data Structures with a Proof Assistant CPP Tobias Nipkow Technische Universität München Media Attached File Attached | ||
16:00 - 16:50 | |||
16:00 - 17:30 | Secure compilers & cryptographyPriSC at PriSC Chair(s): Fraser Brown Stanford University, USA, Aastha Mehta MPI-SWS, Germany and University of British Columbia, Canada | ||
16:00 18mTalk | High-level high-speed high-assurance crypto PriSC Jonathan Cogan Stanford, Fraser Brown Stanford University, USA, Alex Ozdemir Stanford, Riad S. Wahby Stanford University, USA Media Attached | ||
16:18 18mTalk | Cross-Architecture Testing for Compiler-Introduced Security Bugs PriSC Media Attached File Attached | ||
16:36 18mTalk | High-Assurance Cryptography in the Spectre Era PriSC Gilles Barthe MPI-SP, Germany / IMDEA Software Institute, Spain, Sunjay Cauligi University of California at San Diego, USA, Benjamin Gregoire INRIA, Adrien Koutsos INRIA Paris, Kevin Liao Max Planck Institute for Security and Privacy, Tiago Oliveira University of Porto (FCUP) and INESC TEC, Swarn Priya Purdue University, Tamara Rezk Inria, France, Peter Schwabe Max Planck Institute for Security and Privacy Media Attached | ||
16:54 18mTalk | Compilation as Multi-Language Semantics PriSC William J. Bowman University of British Columbia Pre-print Media Attached | ||
17:12 18mTalk | Viaduct: An Optimizing, Extensible Compiler for Secure Distributed Programs PriSC Coşku Acay Cornell University, Rolph Recto , Joshua Gancher Cornell University, Andrew Myers Cornell University, Elaine Shi Cornell University Media Attached | ||
16:00 - 17:00 | |||
16:00 60mKeynote | Model Checking Hyperproperties VMCAI Media Attached | ||
16:50 - 17:30 | |||
16:50 13mTalk | Binary Tree Hamiltonian Monte Carlo LAFI Carol Mak University of Oxford, Fabian Zaiser University of Oxford, C.-H. Luke Ong University of Oxford File Attached | ||
17:03 13mTalk | An algebraic theory of conditioning LAFI File Attached | ||
17:16 13mTalk | The Selection Monad and Decision-Making Languages LAFI File Attached | ||
17:00 - 17:30 | Proof TacticsCPP at CPP Chair(s): Jesper Cockx TU Delft Streamed session: https://youtu.be/PAxUO84tUE8?t=3781 | ||
17:00 15mTalk | A Novice-Friendly Induction Tactic for Lean CPP Jannis Limperg Vrije Universiteit Amsterdam Pre-print Media Attached | ||
17:15 15mTalk | Lassie: HOL4 Tactics by Example CPP Heiko Becker MPI-SWS, Nathaniel Bos McGill University, Ivan Gavran MPI-SWS, Eva Darulova MPI-SWS, Rupak Majumdar MPI-SWS Pre-print Media Attached File Attached | ||
17:00 - 17:30 | |||
17:00 15mTalk | Compositional Model Checking for Multi-Properties VMCAI Ohad Goudsmid Department of Computer Science, The Technion, Orna Grumberg Technion – Israel Institute of Technology, Sarai Sheinvald Department of Software Engineering, ORT Braude College of Engineering Media Attached | ||
17:15 15mTalk | Decomposing Data Structure Commutativity Proofs with mn-Differencing VMCAI Media Attached | ||
17:30 - 18:00 | |||
17:30 30mBreak | Sunday Coffee Break Workshops and Co-located Events | ||
18:00 - 18:45 | Logic, Set Theory, and Category TheoryCPP at CPP Chair(s): Yannick Forster Saarland University Streamed session: https://youtu.be/U_ZT9hfDAUQ | ||
18:00 15mTalk | An Anti-Locally-Nameless Approach to Formalizing Quantifiers CPP Olivier Laurent CNRS & ENS Lyon Pre-print Media Attached | ||
18:15 15mTalk | The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq CPP Pre-print Media Attached | ||
18:30 15mTalk | Formalizing Category Theory in Agda CPP Pre-print Media Attached | ||
18:00 - 19:00 | |||
18:00 60mKeynote | Frontiers in Secure Compilation – an Industrial Perspective (invited talk) PriSC Hugo Vincent Arm Research | ||
18:00 - 19:30 | |||
18:00 90mPoster | SRC Poster Session Student Research Competition | ||
18:00 - 18:30 | Infinite-State Systems and CompilationVMCAI at VMCAI Chair(s): Orna Grumberg Technion – Israel Institute of Technology | ||
18:00 15mTalk | Proving the existence of fair paths in infinite state systems VMCAI Enrico Magnago Fondazione Bruno Kessler, Alberto Griggio Fondazione Bruno Kessler, Alessandro Cimatti Fondazione Bruno Kessler Media Attached | ||
18:15 15mTalk | A Self-Certifying Compilation Framework for WebAssembly VMCAI Media Attached | ||
18:45 - 19:30 | Formalized MathematicsCPP at CPP Chair(s): Amin Timany Aarhus University Streamed session: https://youtu.be/U_ZT9hfDAUQ?t=2768 | ||
18:45 15mTalk | Formalizing the Ring of Witt VectorsDistinguished Paper Award CPP Pre-print Media Attached | ||
19:00 15mTalk | Formal Verification of Semi-algebraic Sets and Real Analytic Functions CPP J Tanner Slagel NASA Langley Research Center, Lauren White Kansas State University, Aaron Dutle NASA Langley Research Center Pre-print Media Attached | ||
19:15 15mTalk | On the Formalisation of Kolmogorov Complexity CPP Pre-print Media Attached | ||
19:30 - 20:00 | |||
19:30 30mSocial Event | Sunday Hallway Time Workshops and Co-located Events | ||
21:00 - 21:30 | |||
21:00 15mTalk | A Categorical Approach to Secure Compilation (and others things) (short talk) PriSC Stelios Tsampas , Andreas Nuyts KU Leuven, Belgium, Dominique Devriese Vrije Universiteit Brussel, Frank Piessens KU Leuven | ||
21:15 15mTalk | Contract-aware Secure Compilation (short talk) PriSC Pre-print | ||
Mon 18 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Mon 18 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
04:30 - 05:30 | |||
04:30 60mSocial Event | Panel Discussion 1: Choosing Research Topics POPL Meetups Chung-Kil Hur Seoul National University, South Korea, Christine Rizkallah The University of Melbourne, Hongseok Yang KAIST, Ilya Sergey Yale-NUS College and National University of Singapore, James Noble Victoria University of Wellington | ||
07:00 - 08:00 | |||
07:00 60mBreak | Monday Coffee Break 1 POPL Meetups | ||
10:00 - 11:00 | Session 1PEPM at PEPM Chair(s): Torben Mogensen DIKU, University of Copenhagen Live stream: https://www.youtube.com/watch?v=fvWxWyV05v4 | ||
10:00 30mShort-paper | A Functional Abstraction of Typed Trails PEPM Kenichi Asai Ochanomizu University, Youyou Cong Tokyo Institute of Technology, Chiaki Ishio Ochanomizu University Media Attached File Attached | ||
10:30 30mResearch paper | A Text-based Syntax Completion Method Using LR Parsing PEPM Media Attached | ||
11:30 - 12:30 | Session 2PEPM at PEPM Chair(s): Youyou Cong Tokyo Institute of Technology Live stream: https://www.youtube.com/watch?v=tuxm51MLkHM | ||
11:30 30mResearch paper | Coq to C Translation with Partial Evaluation PEPM Akira Tanaka National Institute of Advanced Industrial Science and Technology (AIST) Media Attached | ||
12:00 30mResearch paper | Counterexample Generation for Program Verification based on Ownership Refinement TypesBest Paper Award PEPM Hideto Ueno The Univeristy of Tokyo, John Toman Certora, inc., Naoki Kobayashi University of Tokyo, Japan, Takeshi Tsukada Chiba University, Japan Media Attached | ||
13:30 - 14:30 | Session 3PEPM at PEPM Chair(s): Robert Atkey University of Strathclyde Live stream: https://www.youtube.com/watch?v=G5vngBBn398 | ||
13:30 30mShort-paper | Control Flow Obfuscation for Featherweight Java using Continuation Passing PEPM Kenny Zhuo Ming Lu ISTD, Singapore University of Technology and Design Media Attached File Attached | ||
14:00 30mResearch paper | Efficient Fair Conjunction for Structurally-Recursive Relations PEPM Petr Lozov Sain Petersburg State University, SPbGU, Dmitri Boulytchev Saint Petersburg State University / JetBrains Research Media Attached File Attached | ||
14:30 - 15:30 | |||
14:30 60mKeynote | Semantics-based Synthesis in miniKanren PADL William E. Byrd University of Alabama at Birmingham, USA | ||
14:30 - 15:15 | |||
14:30 45mTalk | Think Abstractly, Work Concretely PLMW Ichiro Hasuo National Institute of Informatics, Japan Media Attached | ||
15:00 - 16:00 | Keynote 1PEPM at PEPM Chair(s): Sam Lindley Heriot-Watt University, UK / The University of Edinburgh, UK Live stream: https://www.youtube.com/watch?v=kaJOj_LErQo The PEPM 2021 Best Paper Award will be announced at the beginning of this session immediately before this keynote. | ||
15:00 60mKeynote | Program Manipulation of C Code: From Partial Evaluation to Semantic Patches for the Linux Kernel PEPM Julia Lawall Inria File Attached | ||
15:30 - 16:00 | |||
15:30 30mSocial Event | Topic Oriented Discussions Workshops and Co-located Events | ||
16:00 - 17:00 | Invited TalkCPP at CPP Chair(s): Andrei Popescu University of Sheffield Streamed session: https://youtu.be/poHYVOMQuro?t=144 | ||
16:00 60mTalk | Invited Talk: Underpinning the foundations: Sail-based semantics, testing, and reasoning, for production and CHERI-enabled architectures CPP Peter Sewell University of Cambridge Media Attached | ||
16:00 - 17:30 | Applications of Declarative LanguagesPADL at PADL Chair(s): Ekaterina Komendantskaya Heriot-Watt University, UK | ||
16:00 30mResearch paper | A Logic Programming Approach to Regression Based Repair of Incorrect Initial Belief States PADL Fabio Tardivo New Mexico State University, Loc Pham New Mexico State University, Tran Cao Son New Mexico State University, Enrico Pontelli New Mexico State University | ||
16:30 30mResearch paper | Data validation meets Answer Set Programming PADL Mario Alviano University of Calabria, Carmine Dodaro Department of Mathematics and Computer Science, University of Calabria, Arnel Zamayla University of Calabria, Italy | ||
17:00 30mResearch paper | Lightweight Declarative Server-Side Web Programming PADL Michael Hanus Kiel University | ||
16:00 - 17:30 | |||
16:00 45mTalk | Numbers, Logic, and Decidability Results for Cyber-Physical Systems PLMW Rupak Majumdar MPI-SWS | ||
16:45 45mTalk | The Lean Researcher PLMW Alastair F. Donaldson Imperial College London and Google | ||
16:00 - 17:30 | |||
16:00 90mTutorial | [T1] The Current State of Automatic Differentiation TutorialFest Barak A. Pearlmutter Maynooth University | ||
16:00 - 17:30 | |||
16:00 90mTutorial | [T2] Liquid Haskell: Refinement Type Checker for Haskell TutorialFest | ||
16:00 - 17:30 | |||
16:00 90mTutorial | [T3] Dynamic Data-Race Prediction : Fundamentals, Theory and Practice TutorialFest Pre-print Media Attached File Attached | ||
16:00 - 17:00 | |||
16:00 60mKeynote | Algebra-based Synthesis of Loops and their Invariants VMCAI I: Laura Kovacs Vienna University of Technology (TU Wien), Andreas Humenberger Vienna University of Technology Media Attached | ||
17:00 - 17:30 | Program LogicsCPP at CPP Chair(s): William Mansky University of Illinois at Chicago Streamed session: https://youtu.be/poHYVOMQuro?t=3869 | ||
17:00 15mTalk | Contextual Refinement of the Michael-Scott Queue (Proof Pearl) CPP Pre-print Media Attached | ||
17:15 15mTalk | Reasoning About Monotonicity in Separation Logic CPP Pre-print Media Attached | ||
17:00 - 17:30 | |||
17:00 15mTalk | Runtime Abstract Interpretation for Numerical Accuracy and Robustness VMCAI Franck Védrine CEA LIST, Maxime Jacquemin CEA LIST, France, Nikolai Kosmatov Thales Research and Technology, Julien Signoles CEA LIST Media Attached | ||
17:15 15mTalk | Twinning automata and regular expressions for string static analysis VMCAI Luca Negrini Ca’ Foscari University of Venice, Julia S.r.l., Vincenzo Arceri Ca’ Foscari University of Venice, Pietro Ferrara Università Ca' Foscari, Venezia, Italy, Agostino Cortesi Università Ca' Foscari Venezia Media Attached | ||
17:30 - 18:00 | |||
17:30 30mBreak | Monday Coffee Break 2 Workshops and Co-located Events | ||
18:00 - 18:45 | |||
18:00 15mTalk | A Coq Formalization of Data Provenance CPP Véronique Benzaken Université Paris Saclay, Sarah Cohen-Boulakia LRI, Université de Paris Sud, CNRS (UMR8623) - Université Paris Saclay, Evelyne Contejean CNRS, Chantal Keller LRI, Univ. Paris-Sud, Rébecca Zucchini LRI, Université de Paris Sud, CNRS (UMR8623) - Université Paris Saclay Pre-print Media Attached | ||
18:15 15mTalk | Developing and certifying Datalog optimizations in Coq/MathComp CPP Pre-print Media Attached | ||
18:30 15mTalk | Machine-Checked Semantic Session TypingDistinguished Paper Award CPP Jonas Kastberg Hinrichsen IT University of Copenhagen, Daniël Louwrink University of Amsterdam, Robbert Krebbers Radboud University Nijmegen, Jesper Bengtson IT University of Copenhagen Pre-print Media Attached | ||
18:00 - 19:30 | |||
18:00 30mResearch paper | A Family of Unification-oblivious Program Transformations and Their Applications PADL Paul Tarau University of North Texas | ||
18:30 30mResearch paper | On Adding Pattern Matching to Haskell-based Deeply Embedded Domain Specific Languages PADL David Young University of Kansas, USA, Mark Grebe University of Central Missouri, USA, Andy Gill University of Kansas, USA | ||
18:00 - 19:30 | |||
18:00 45mTalk | Reasoning About Programs in Higher-Order Concurrent Separation Logic PLMW Amin Timany Aarhus University | ||
18:45 45mTalk | εσόμεθα πολλώ κάρρονες – making your way in a changing world PLMW Sophia Drossopoulou Imperial College London | ||
18:00 - 19:30 | |||
18:00 90mTutorial | [T5] An Invitation to the Intersection of Quantum Computing and Programming Languages TutorialFest Xiaodi Wu University of Maryland, USA Pre-print | ||
18:00 - 19:30 | |||
18:00 90mTutorial | [T4] Iris – A Modular Foundation for Higher-Order Concurrent Separation Logic TutorialFest Tej Chajed Massachusetts Institute of Technology, USA, Ralf Jung MPI-SWS, Joseph Tassarotti Boston College Link to publication | ||
18:00 - 18:30 | |||
18:00 15mTalk | Unbounded Procedure Summaries from Bounded Environments VMCAI Lauren Pick Princeton University, Grigory Fedyukovich Florida State University, Aarti Gupta Princeton University Media Attached | ||
18:15 15mTalk | Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking VMCAI Hongce Zhang Princeton University, Aarti Gupta Princeton University, Sharad Malik Princeton University Media Attached | ||
18:30 - 19:15 | |||
18:30 15mTalk | Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible VMCAI Marius Kamp Friedrich-Alexander University Erlangen-Nürnberg, Michael Philippsen Friedrich-Alexander University Erlangen-Nürnberg (FAU) Media Attached | ||
18:45 15mTalk | Automated Repair of Heap-Manipulating Programs using Deductive Synthesis VMCAI Thanh-Toan Nguyen National University of Singapore, Quang-Trung Ta National University of Singapore, Ilya Sergey Yale-NUS College and National University of Singapore, Wei-Ngan Chin National University of Singapore Media Attached | ||
19:00 15mTalk | GPURepair: Automated Repair of GPU Kernels VMCAI Media Attached | ||
18:45 - 19:30 | Security, Blockchains, and Smart ContractsCPP at CPP Chair(s): Andreas Lochbihler Digital Asset Streamed session: https://youtu.be/Qak5mK92etU?t=2832 | ||
18:45 15mTalk | Extracting Smart Contracts Tested and Verified in Coq CPP Danil Annenkov Concordium Blockchain Research Center, Aarhus University, Mikkel Milo Concordium Blockchain Research Center, Aarhus University, Jakob Botsch Nielsen Concordium Blockchain Research Center, Aarhus University, Bas Spitters Concordium Blockchain Research Center, Aarhus University Pre-print Media Attached File Attached | ||
19:00 15mTalk | Formal Verification of Authenticated, Append-Only Skip Lists in Agda CPP Victor Cacciari Miraldo DFINITY Foundation, Harold Carr Oracle Labs, USA, Mark Moir Oracle Labs, New Zealand, Lisandra Silva University of Minho, Guy L. Steele Jr. Oracle Labs Pre-print Media Attached | ||
19:15 15mTalk | Towards formally verified compilation of tag-based policy enforcement CPP CHR Chhak Portland State University, Andrew Tolmach Portland State University, Sean Anderson Portland State University Pre-print Media Attached | ||
19:30 - 20:00 | |||
19:30 30mSocial Event | Monday Shuffle-Space Time Workshops and Co-located Events | ||
20:00 - 21:00 | |||
20:00 60mSocial Event | POPL Card Game Workshops and Co-located Events | ||
20:00 - 21:00 | Lightning TalksCPP / CPP Lightning Talks at CPP Chair(s): Natarajan Shankar SRI International, USA Streamed sessions: https://youtu.be/sFMJBTtbjTc | ||
20:00 5mTalk | Certified Semantics for miniKanren CPP Lightning Talks Dmitry Rozplokhas Saint Petersburg State University and JetBrains Research, Andrey Vyatkin Saint Petersburg State University, Petr Lozov Sain Petersburg State University, SPbGU, Dmitri Boulytchev Saint Petersburg State University / JetBrains Research Media Attached | ||
20:05 5mTalk | Cameleer: a Deductive Verification Tool for OCaml CPP Lightning Talks Mário Pereira NOVA LINCS & Nova School of Sciences and Tecnhology, Antonio Ravara Department of Informatics, Faculty of Sciences and Technology, NOVA University of Lisbon and NOVA LINCS | ||
20:10 5mTalk | Gradualizing the Calculus of Inductive Constructions CPP Lightning Talks Meven Lennon-Bertrand Inria – LS2N, Université de Nantes, Kenji Maillard Inria Nantes & University of Chile, Nicolas Tabareau Inria, Éric Tanter University of Chile Pre-print | ||
20:15 5mTalk | Formally Verified Decentralized Exchange with Mi-Cho-Coq CPP Lightning Talks Arvid Jakobsson Nomadic Labs, Colin González Université de Paris, Irif -- Nomadic Labs, Bruno Bernardo Nomadic Labs, Raphaël Cauderlier Nomadic Labs | ||
20:20 5mTalk | A semantic domain for privacy-aware smart contracts and interoperable sharded ledgers CPP Lightning Talks Sören Bleikertz Digital Asset, Andreas Lochbihler Digital Asset, Ognjen Marić Digital Asset, Simon Meier Digital Asset, Phoebe Nichols Digital Asset, Matthias Schmalz Digital Asset, Ratko G. Veprek Digital Asset File Attached | ||
20:25 5mTalk | Specification and model checking of Tendermint consensus in TLA+ CPP Lightning Talks | ||
20:30 5mTalk | Formalization of Combinatorics on Words in Isabelle/HOL CPP Lightning Talks Štěpán Holub Charles University, Štěpán Starosta Faculty of Information Technology, Czech Technical University in Prague Link to publication Media Attached File Attached | ||
20:35 5mTalk | Formalising MPC-in-the-head-based zero-knowledge CPP Lightning Talks Nikolaj Sidorenco Aarhus University, Sabine Oechsner Aarhus University, Bas Spitters Concordium Blockchain Research Center, Aarhus University File Attached | ||
20:40 5mTalk | Mechanically-checked soundness of type-based null safety CPP Lightning Talks Alexander Kogtenkov Schaffhausen Institute of Technology, Switzerland Media Attached File Attached | ||
20:45 5mTalk | Formalising MiniSail in Isabelle CPP Lightning Talks Mark Wassell University of Cambridge | ||
20:50 5mTalk | How to verify an ASN.1 Protocol C-language Stack in Coq? CPP Lightning Talks File Attached | ||
20:55 5mTalk | Monadic Second-Order Logic and Pomset Languages CPP Lightning Talks Tobias Kappé Cornell University | ||
20:00 - 21:00 | |||
20:00 60mLive Q&A | Panel: Doing Research in PL PLMW Greg Morrisett Cornell Tech, Susan Eisenbach Imperial College London, Sam Lindley Heriot-Watt University, UK / The University of Edinburgh, UK, Jeehoon Kang KAIST, Delphine Demange Univ Rennes, Inria, CNRS, IRISA, Kuen-Bang Hou (Favonia) University of Minnesota, Twin Cities | ||
Tue 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Tue 19 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
04:30 - 05:30 | |||
04:30 60mSocial Event | Panel Discussion 2: Improving Peer Review POPL Meetups Hongseok Yang KAIST, Ilya Sergey Yale-NUS College and National University of Singapore, James Noble Victoria University of Wellington, Soham Chakraborty IIT Delhi, Youyou Cong Tokyo Institute of Technology | ||
07:00 - 08:00 | |||
07:00 60mBreak | Tuesday Coffee Break 1 POPL Meetups | ||
14:30 - 15:30 | |||
14:30 60mKeynote | Verifying a compiler through equational means CoqPL Yannick Zakowski Inria | ||
14:30 - 15:30 | |||
14:30 60mKeynote | SMT-based Constraint Answer Set Solver EZSMT PADL Yuliya Lierler University of Nebraska | ||
14:30 - 15:30 | |||
14:30 60mLive Q&A | Panel: Navigating PhD studies PLMW Hila Peleg University of California at San Diego, Nick Giannarakis University of Wisconsin-Madison, Anne-Kathrin Schmuck MPI-SWS, Sacha-Élie Ayoun Imperial College London, Farzaneh Derakhshan Carnegie Mellon University, Soham Chakraborty IIT Delhi | ||
15:00 - 16:00 | Keynote 2PEPM at PEPM Chair(s): Torben Mogensen DIKU, University of Copenhagen Live stream: https://www.youtube.com/watch?v=Ps_rUSG1yg0 | ||
15:00 60mKeynote | Erasure In Dependently Typed Programming PEPM Matúš Tejiščák Chordify | ||
15:30 - 16:00 | |||
15:30 30mSocial Event | Tuesday Shuffle-Space Time Workshops and Co-located Events | ||
16:00 - 16:45 | Compilers and InterpretersCPP at CPP Chair(s): Freek Wiedijk Radboud University Nijmegen Streamed session: https://youtu.be/TVqCuMMTuos | ||
16:00 15mTalk | A Minimalistic Verified Bootstrapped Compiler (Proof Pearl)Distinguished Paper Award CPP Magnus O. Myreen Chalmers University of Technology Pre-print Media Attached | ||
16:15 15mTalk | Lutsig: A Verified Verilog Compiler for Verified Circuit Development CPP Andreas Lööw Chalmers University of Technology Pre-print Media Attached | ||
16:30 15mTalk | Towards Efficient and Verified Virtual Machines for Dynamic Languages CPP Martin Desharnais Universität der Bundeswehr München, Stefan Brunthaler Universität der Bundeswehr München Pre-print Media Attached | ||
16:00 - 17:30 | |||
16:00 15mTalk | A Limited Case for Reification by Type Inference CoqPL Jason Gross MIT CSAIL Media Attached File Attached | ||
16:15 15mTalk | Towards a Coq Specification for Generalized Algebraic Datatypes in OCaml CoqPL File Attached | ||
16:30 15mTalk | Record Updates in Coq CoqPL Tej Chajed Massachusetts Institute of Technology, USA Media Attached File Attached | ||
16:45 15mBreak | Break CoqPL | ||
17:00 15mTalk | The B+-tree Index as a Verified Software Unit CoqPL Anastasiya Kravchuk-Kirilyuk Harvard University, Andrew Appel Princeton, Lennart Beringer Princeton University File Attached | ||
17:15 15mTalk | Automated Synthesis of Verified Firewalls CoqPL Shardul Chiplunkar Massachusetts Institute of Technology, Clément Pit-Claudel Massachusetts Institute of Technology, USA, Adam Chlipala Massachusetts Institute of Technology File Attached | ||
16:00 - 17:30 | Declarative Approaches to Testing and DebuggingPADL at PADL Chair(s): Paul Tarau University of North Texas | ||
16:00 30mResearch paper | ConFuzz: Coverage-guided Property Fuzzing for Event-driven Programs PADL Link to publication | ||
16:30 30mResearch paper | Causal-Consistent Reversible Debugging: Improving CauDEr PADL Juan José González-Abril MiST, VRAIN, Universitat Politecnica de Valencia, German Vidal Universitat Politecnica de Valencia | ||
17:00 30mResearch paper | Declarative Debugging of XML Queries PADL | ||
16:00 - 17:30 | |||
16:00 45mTalk | Connecting Information Flow Types to Runtime Monitors via Gradual Typing PLMW Limin Jia Carnegie Mellon University | ||
16:45 45mTalk | Emotional Machines PLMW Aaron Turon Fastly | ||
16:00 - 17:00 | |||
16:00 60mKeynote | Generative Program Analysis and Beyond: The Power of Domain-Specific Languages VMCAI Media Attached | ||
16:30 - 17:30 | Session 4PEPM at PEPM Chair(s): Jeremy Yallop University of Cambridge Live stream: https://www.youtube.com/watch?v=BmBSJFkfL2M | ||
16:30 30mShort-paper | Staged Effects and Handlers for Modular Languages with Abstraction PEPM Casper Bach Poulsen Delft University of Technology, Cas van der Rest Delft University of Technology, Tom Schrijvers KU Leuven Media Attached File Attached | ||
17:00 30mShort-paper | Automatic Differentiation via Effects and Handlers: An Implementation in Frank PEPM Jesse Sigal University of Edinburgh Media Attached File Attached | ||
16:45 - 17:30 | Rewriting and Automated ReasoningCPP at CPP Chair(s): Cyril Cohen Université Côte d’Azur, Inria, France Streamed session: https://youtu.be/TVqCuMMTuos?t=2806 | ||
16:45 15mTalk | A Modular Isabelle Framework for Verifying Saturation Provers CPP Pre-print Media Attached | ||
17:00 15mTalk | An Isabelle/HOL Formalization of AProVE's Termination Method for LLVM IR CPP Pre-print Media Attached | ||
17:15 15mTalk | A Verified Decision Procedure for the First-Order Theory of Rewriting for Linear Variable-Separated Rewrite Systems CPP Alexander Lochmann University of Innsbruck, Aart Middeldorp University of Innsbruck, Fabian Mitterwallner University of Innsbruck, Bertram Felgenhauer Pre-print Media Attached | ||
17:00 - 17:30 | ApplicationsVMCAI at VMCAI Chair(s): Rayna Dimitrova CISPA Helmholtz Center for Information Security | ||
17:00 15mTalk | A Synchronous Effects Logic for Temporal Verification of Pure Esterel VMCAI Media Attached | ||
17:15 15mTalk | A Design of GPU-Based Quantitative Model Checking VMCAI Media Attached | ||
17:30 - 18:00 | |||
17:30 30mBreak | Tuesday Coffee Break 2 Workshops and Co-located Events | ||
18:00 - 18:30 | AI and Machine LearningCPP at CPP Chair(s): Ekaterina Komendantskaya Heriot-Watt University, UK Streamed session: https://youtu.be/6NJdWdiZEiA | ||
18:00 15mTalk | A Formal Proof of PAC Learnability for Decision Stumps CPP Joseph Tassarotti Boston College, Koundinya Vajjha University of Pittsburgh, Anindya Banerjee IMDEA Software Institute, Jean-Baptiste Tristan Boston College Pre-print Media Attached | ||
18:15 15mTalk | CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq CPP Koundinya Vajjha University of Pittsburgh, Avraham Shinnar IBM Research, Barry Trager IBM Research, Vasily Pestun IBM Research; IHES, Nathan Fulton IBM Research Pre-print Media Attached | ||
18:00 - 18:45 | |||
18:00 15mTalk | Verification of Algorithm and Code Generation for Signal Transforms CoqPL File Attached | ||
18:15 15mTalk | An experience report on writing usable DSLs in Coq CoqPL File Attached | ||
18:30 15mBreak | Break CoqPL | ||
18:00 - 19:30 | Foundations and Programming Concepts at WorkPADL at PADL Chair(s): Mario Alviano University of Calabria | ||
18:00 30mResearch paper | Synchronous Message-Passing with Priority PADL Cheng-En Chuang University at Buffalo, Grant Iraci University at Buffalo, Lukasz Ziarek SUNY Buffalo, USA | ||
18:30 30mResearch paper | Putting gradual types to work PADL Bhargav Shivkumar State University of New York - University at Buffalo, Enrique Naudon Bloomberg, Lukasz Ziarek SUNY Buffalo, USA | ||
19:00 30mShort-paper | Psamathe: A DSL with Flows for Safe Blockchain Assets (extended abstract) PADL Reed Oei University of Illinois at Urbana-Champaign, Michael Coblenz University of Maryland at College Park, Jonathan Aldrich Carnegie Mellon University File Attached | ||
18:00 - 19:00 | Session 5PEPM at PEPM Chair(s): Torben Mogensen DIKU, University of Copenhagen Live stream: https://www.youtube.com/watch?v=VJZcAtvGOyE | ||
18:00 30mResearch paper | A Type-Safe Structure Editor Calculus PEPM Christian Godiksen Department of Computer Science, Aalborg University, Thomas Herrmann Department of Computer Science, Aalborg University, Hans Hüttel Department of Computer Science, Aalborg University, Mikkel Korup Lauridsen Department of Computer Science, Aalborg University, Iman Owliaie Department of Computer Science, Aalborg University Media Attached | ||
18:30 30mResearch paper | Strictly Capturing Non-Strict Closures PEPM Zachary Sullivan University of Oregon, Paul Downen University of Oregon, USA, Zena M. Ariola University of Oregon, USA Media Attached | ||
18:00 - 19:30 | |||
18:00 90mTalk | SRC Finalists Presentations Student Research Competition | ||
18:00 - 18:30 | Case StudiesVMCAI at VMCAI Chair(s): Roderick Bloem Institute of Software Technology, Graz University of Technology | ||
18:00 15mTalk | Formal Semantics and Verification of Network Based Biocomputation Circuits VMCAI Michelle Aluf-Medina Bar Ilan University, Till Korten TU Dresden, Avraham Raviv Bar Ilan University, Dan Nicolau Jr. Molecular Sense, Hillel Kugler Bar Ilan University Media Attached | ||
18:15 15mTalk | Netter: Probabilistic, Stateful Network Models VMCAI Han Zhang Carnegie Mellon University, Chi Zhang CMU, Arthur Azevedo de Amorim Carnegie Mellon University, USA, Yuvraj Agarwal Carnegie Mellon University, Matt Fredrikson Carnegie Mellon University, Limin Jia Carnegie Mellon University Media Attached | ||
18:30 - 19:30 | |||
18:30 60mTalk | Chairs' report and community meeting CPP Cătălin Hriţcu MPI-SP, Andrei Popescu University of Sheffield, Lennart Beringer Princeton University Media Attached File Attached | ||
18:30 - 19:30 | |||
18:30 15mTalk | Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories VMCAI Martin Bromberger MPI-INF, Alberto Fiori Max Planck Institute for Informatics, Christoph Weidenbach MPI-INF Media Attached | ||
18:45 15mTalk | Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching VMCAI Media Attached | ||
19:00 15mTalk | On Pre- and Inprocessing for Weighted MaxSAT VMCAI Tobias Paxian University of Freiburg, Pascal Raiola University of Freiburg, Bernd Becker Albert-Ludwigs-University Freiburg Media Attached | ||
19:15 15mTalk | Compositional Satisfiability Solving in Separation Logic VMCAI Quang Loc Le University College London, UK Media Attached | ||
18:45 - 19:30 | |||
18:45 45mDemonstration | Session with the Coq Development Team CoqPL | ||
19:30 - 20:00 | |||
19:30 30mBreak | Welcome to Copenhagen! Workshops and Co-located Events | ||
19:30 - 20:30 | Keynote 3PEPM at PEPM Chair(s): Sam Lindley Heriot-Watt University, UK / The University of Edinburgh, UK Live stream: https://www.youtube.com/watch?v=MMq4J8eti1g | ||
19:30 60mKeynote | Hardware DSLs PEPM Pat Hanrahan Stanford University, USA | ||
Wed 20 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Wed 20 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
04:30 - 05:30 | |||
04:30 60mSocial Event | Panel Discussion 3: Work/Life Balance POPL Meetups Andreea Costea School of Computing, National University Of Singapore, Atsushi Igarashi Kyoto University, Japan, KC Sivaramakrishnan IIT Madras, Soham Chakraborty IIT Delhi | ||
07:00 - 08:00 | |||
07:00 60mBreak | Wednesday Coffee Break POPL Meetups | ||
15:15 - 15:45 | |||
15:15 30mSocial Event | Wednesday Breakfast Tables POPL | ||
16:00 - 17:00 | |||
16:00 10mTalk | A Computational Interpretation of Compact Closed Categories: Reversible Programming with Negative and Fractional Types POPL Link to publication DOI | ||
16:10 10mTalk | Internalizing Representation Independence with Univalence POPL Carlo Angiuli Carnegie Mellon University, Evan Cavallo Carnegie Mellon University, Anders Mörtberg Department of Mathematics, Stockholm University, Max Zeuner Stockholm University Link to publication DOI | ||
16:20 10mTalk | Petr4: Formal Foundations for P4 Data Planes POPL Ryan Doenges Cornell University, Mina Tahmasbi Arashloo Cornell University, Santiago Bautista Univ Rennes, ENS Rennes, Inria, IRISA, Alexander Chang Cornell University, Newton Ni Cornell University, Samwise Parkinson Cornell University, Rudy Peterson Cornell University, Alaia Solko-Breslin Cornell University, Amanda Xu Cornell University, Nate Foster Cornell University Link to publication DOI Pre-print | ||
16:30 10mTalk | The (In)Efficiency of Interaction POPL Beniamino Accattoli Inria & Ecole Polytechnique, Ugo Dal Lago University of Bologna, Italy / Inria, France, Gabriele Vanoni University of Bologna & INRIA Sophia Antipolis Link to publication DOI | ||
16:40 10mTalk | Functorial Semantics for Partial Theories POPL Chad Nester Tallinn University of Technology, Ivan Di Liberti Czech Academy of Sciences, Fosco Loregian Tallinn University of Technology, Pawel Sobocinski Tallinn University of Technology Link to publication DOI | ||
16:50 10mBreak | Break POPL | ||
17:00 - 18:00 | |||
17:00 60mKeynote | The road to a Universal Internet Machine (Demystifying Blockchain Protocols)Invited Talk POPL Rachid Guerraoui EPFL Media Attached | ||
19:30 - 20:00 | |||
19:30 30mSocial Event | Happy Hour POPL | ||
19:30 - 20:00 | |||
19:30 30mIndustry talk | Sponsor Reception POPL Media Attached | ||
20:00 - 21:00 | |||
20:00 60mSocial Event | Trivia Night POPL | ||
20:00 - 20:30 | |||
20:00 30mMeeting | SIGPLAN CARES POPL P: Stephanie Weirich University of Pennsylvania, P: Alexandra Silva University College London, P: Shriram Krishnamurthi Brown University, United States, P: David Walker Princeton University, USA | ||
Thu 21 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Thu 21 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
02:00 - 03:00 | |||
02:00 60mSocial Event | POPL Cocktail Hour POPL | ||
04:00 - 04:30 | |||
04:00 30mMeeting | SIGPLAN CARES POPL P: Stephanie Weirich University of Pennsylvania, P: Hongseok Yang KAIST, P: Shriram Krishnamurthi Brown University, United States, P: David Walker Princeton University, USA | ||
04:30 - 05:30 | |||
04:30 60mSocial Event | Panel Discussion 4: Finding Friends and Collaborators in Academia POPL Meetups Aseem Rastogi Microsoft Research, Atsushi Igarashi Kyoto University, Japan, Christine Rizkallah The University of Melbourne, Jeehoon Kang KAIST, Youyou Cong Tokyo Institute of Technology | ||
07:00 - 08:00 | |||
07:00 60mBreak | Thursday Coffee Break POPL Meetups | ||
15:15 - 15:45 | |||
15:15 30mSocial Event | Topic Oriented Discussions POPL | ||
15:45 - 15:55 | |||
15:45 10mAwards | Most Influential POPL Paper POPL Media Attached | ||
15:55 - 16:00 | |||
15:55 5mAwards | Student Research Competition Results Student Research Competition | ||
16:00 - 17:00 | |||
16:00 10mTalk | Efficient and Provable Local Capability Revocation using Uninitialized Capabilities POPL Aina Linn Georges Aarhus University, Armaël Guéneau Aarhus University, Thomas Van Strydonck KULeuven, Amin Timany Aarhus University, Alix Trieu Aarhus University, Sander Huyghebaert Vrije Universiteit Brussel, Dominique Devriese Vrije Universiteit Brussel, Lars Birkedal Aarhus University Link to publication DOI Pre-print | ||
16:10 10mTalk | Mechanized Logical Relations for Termination-Insensitive Noninterference POPL Simon Oddershede Gregersen Aarhus University, Johan Bay Aarhus University, Amin Timany Aarhus University, Lars Birkedal Aarhus University Link to publication DOI Pre-print | ||
16:20 10mTalk | Giving Semantics to Program-Counter Labels via Secure Effects POPL Link to publication DOI | ||
16:30 10mTalk | Automata and Fixpoints for Asynchronous Hyperproperties POPL Jens Oliver Gutsfeld Westfälische Wilhelm-Universität Münster (WWU), Germany, Markus Müller-Olm University of Münster, Christoph Ohrem Westfälische Wilhelms-Universität Münster (WWU), Germany Link to publication DOI | ||
16:40 10mTalk | Automatically Eliminating Speculative Leaks from Cryptographic Code with BladeDistinguished Paper POPL Marco Vassena CISPA Helmholtz Center for Information Security, Craig Disselkoen University of California at San Diego, USA, Klaus v. Gleissenthall Vrije Universiteit Amsterdam, Netherlands, Sunjay Cauligi University of California at San Diego, USA, Rami Gökhan Kıcı University of California at San Diego, USA, Ranjit Jhala University of California at San Diego, Dean Tullsen University of California at San Diego, USA, Deian Stefan University of California at San Diego, USA Link to publication DOI Pre-print | ||
16:50 10mBreak | Break POPL | ||
16:00 - 17:00 | |||
16:00 10mTalk | Verifying Observational Robustness Against a C11-style Memory Model POPL Link to publication DOI | ||
16:10 10mTalk | Provably Space Efficient Parallel Functional ProgrammingDistinguished Paper POPL Link to publication DOI | ||
16:20 10mTalk | Modeling and Analyzing Evaluation Cost of CUDA Kernels POPL Link to publication DOI | ||
16:30 10mTalk | Optimal Prediction of Synchronization-Preserving Races POPL Umang Mathur University of Illinois at Urbana-Champaign, Andreas Pavlogiannis Aarhus University, Mahesh Viswanathan University of Illinois at Urbana-Champaign Link to publication DOI Pre-print | ||
16:40 10mTalk | Taming x86-TSO Persistency POPL Link to publication DOI Pre-print | ||
16:50 10mBreak | Break POPL | ||
17:00 - 18:00 | |||
17:00 60mKeynote | Dynamical Systems and Program AnalysisInvited Talk POPL James Worrell University of Oxford File Attached | ||
19:30 - 20:30 | |||
19:30 60mMeeting | Business Meeting & Townhall POPL | ||
20:30 - 21:30 | |||
20:30 60mMeeting | Iris meetup POPL Meetups | ||
21:00 - 22:00 | |||
21:00 60mSocial Event | Games Programming Languages BoF Session POPL Meetups | ||
Fri 22 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Fri 22 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
07:00 - 08:00 | |||
07:00 60mBreak | Friday Coffee Break POPL Meetups | ||
15:15 - 15:45 | |||
15:15 30mSocial Event | Friday Breakfast Tables POPL | ||
17:00 - 18:00 | |||
17:00 60mKeynote | Toward a Programmable Cloud: CALM Foundations and Open ChallengesInvited Talk POPL Media Attached File Attached | ||
18:30 - 19:00 | |||
18:30 10mTalk | Generating Collection Transformations from Proofs POPL Link to publication DOI | ||
18:40 10mTalk | Semantics-Guided Synthesis POPL Jinwoo Kim University of Wisconsin-Madison, Qinheping Hu University of Wisconsin-Madison, USA, Loris D'Antoni University of Wisconsin-Madison, USA, Thomas Reps University of Wisconsin--Madison Link to publication DOI | ||
18:50 10mTalk | Combining the Top-down Propagation and Bottom-up Enumeration for Inductive Program Synthesis POPL Woosuk Lee Hanyang University, South Korea Link to publication DOI | ||
18:30 - 19:00 | |||
18:30 10mTalk | Cyclic Proofs, System T, and the Power of Contraction POPL Link to publication DOI | ||
18:40 10mTalk | egg: Fast and Extensible Equality SaturationDistinguished Paper POPL Max Willsey University of Washington, USA, Chandrakana Nandi University of Washington, USA, Yisu Remy Wang University of Washington, Oliver Flatt University of Utah, Zachary Tatlock University of Washington, Seattle, Pavel Panchekha University of Utah Link to publication DOI Pre-print | ||
18:50 10mTalk | Debugging Large-Scale Datalog: A Scalable Provenance Evaluation StrategyTOPLAS POPL David Zhao The University of Sydney, Pavle Subotic Microsoft and Mathematical Institute, Serbian Academy of Sciences and Arts (SASA), Bernhard Scholz University of Sydney, Australia Link to publication DOI | ||
19:00 - 20:00 | |||
19:00 60mAwards | Robin Milner Award Talk: "Structural Language Models of Code" POPL Media Attached | ||
20:00 - 20:30 | |||
20:00 30mSocial Event | Farewell Reception POPL | ||
21:00 - 22:00 | |||
21:00 60mMeeting | Iris meetup #2 POPL Meetups | ||