Filter Program
Dates
Rooms
Tracks
Badges
Your Program
Sun 19 JanDisplayed time zone: Saskatchewan, Central America change
Sun 19 Jan
Displayed time zone: Saskatchewan, Central America change
09:00 - 10:00 | |||
09:00 30mTalk | Invited Talk: Quantum Computing for Programming Languages Researchers PLanQC Media Attached File Attached | ||
09:30 30mTalk | Invited Talk: Dependently Typed Quantum Programming in Proto-Quipper PLanQC Media Attached | ||
09:00 - 10:00 | |||
09:00 60mTalk | The Siren Song of Temporal Synthesis VMCAI Moshe Vardi Rice University | ||
10:30 - 12:30 | |||
10:30 30mTalk | Invited Talk: Q# - Going Beyond Quantum Circuits PLanQC Media Attached | ||
11:00 30mTalk | Invited Talk: Resource-Efficient Quantum Computing by Breaking Abstractions PLanQC Media Attached File Attached | ||
11:30 20mTalk | Tuning up entanglement through the cloud using Qiskit-OpenPulse PLanQC Thomas Alexander IBM T.J. Watson Research Center, New York, USA, Naoki Kanazawa IBM Research, Tokyo, Japan, Daniel Egger IBM Research, Zurich, Switzerland, Ali Javadi-Abhari IBM T.J. Watson Research Center, New York, USA, David C. McKay IBM T.J. Watson Research Center, New York, USA | ||
11:50 20mTalk | Tracking Errors through Types in Quantum Programs PLanQC Kesha Hietala University of Maryland, Robert Rand University of Maryland, Michael Hicks University of Maryland Pre-print Media Attached File Attached | ||
12:10 20mTalk | Quantum CPOs PLanQC | ||
10:30 - 12:30 | |||
10:30 30mTalk | Witnessing Secure Compilation VMCAI | ||
11:00 30mTalk | BackFlow: Backward Context-sensitive Flow Reconstruction of Taint Analysis Results VMCAI Pietro Ferrara Università Ca' Foscari, Venezia, Italy, Luca Olivieri JuliaSoft SRL, Fausto Spoto U. Verona | ||
11:30 30mCoffee break | Mini Break VMCAI | ||
12:00 30mTalk | Fixing Code That Explodes Under Symbolic Evaluation VMCAI Sorawee Porncharoenwase University of Washington, James Bornholt University of Texas at Austin, Emina Torlak University of Washington | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:05 | |||
14:00 20mTalk | Runtime Analysis of Quantum Programs: A Formal Approach PLanQC Pre-print File Attached | ||
14:20 20mTalk | Qbricks: formal verification in quantum computing PLanQC Christopĥe Chareton CEA, LIST, France, Sébastien Bardin CEA LIST, François Bobot CEA, Valentin Perrelle CEA, LIST, France, Benoit Valiron LRI, CentraleSupelec, Univ. Paris Saclay File Attached | ||
14:40 25mTalk | Merged Talk: A Verified Optimizer for Quantum Circuits & Verified Translation Between Low-Level Quantum Languages PLanQC Kesha Hietala University of Maryland, Kartik Singhal University of Chicago, Robert Rand University of Maryland, Shih-Han Hung University of Maryland, Xiaodi Wu University of Maryland, College Park, Michael Hicks University of Maryland Media Attached | ||
14:00 - 15:05 | |||
14:00 65mTalk | Safety and Robustness for Deep Learning with Provable Guarantees VMCAI Marta Kwiatkowska University of Oxford | ||
15:35 - 16:35 | |||
15:35 20mTalk | Optimal Two-Qubit Circuits for Universal Fault-Tolerant Quantum Computation PLanQC Andrew N. Glaudell University of Maryland, Neil Julien Ross Dalhousie University, Jacob M. Taylor University of Maryland Pre-print Media Attached File Attached | ||
15:55 20mTalk | Context-Sensitive and Duration-Aware Qubit Mapping for Various NISQ Devices PLanQC Yu Zhang University of Science and Technology of China, Haowei Deng University of Science and Technology of China, Quanxi Li University of Science and Technology of China Pre-print Media Attached | ||
16:15 20mTalk | Quingo: A Domain Specific Language for Quantum Computing with NISQ Features PLanQC Xiang Fu Institute for Quantum Information & State Key Laboratory of High Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Jintao Yu State Key Laboratory of Mathematical Engineering and Advanced Computing, Zhengzhou, China, Xing Su College of Meteorology and Oceanography, National University of Defense Technology, Changsha, China, Hanru Jiang Center for Quantum Computing, Peng Cheng Laboratory, Shenzhen, China, Hua Wu Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China, Dong Chen Department of Computing Science, College of Computer, National University of Defense Technology, Changsha, China, Fucheng Cheng Center for Quantum Computing, Peng Cheng Laboratory, Shenzhen, China, Xi Deng Center for Quantum Computing, Peng Cheng Laboratory, Shenzhen, China, Jinrong Zhang Center for Quantum Computing, Peng Cheng Laboratory, Shenzhen, China, Lei Jin School of Information Engineering, Zhengzhou University, Zhengzhou, China, Yihang Yang School of Information Engineering, Zhengzhou University, Zhengzhou, China, Le Xu School of Information Engineering, Zhengzhou University, Zhengzhou, China, Chunchao Hu School of Information Engineering, Zhengzhou University, Zhengzhou, China, Anqi Huang Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Guangyao Huang Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Xiaogang Qiang Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Mingtang Deng Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Ping Xu Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Wanwei Liu National University of Defense Technology, Yuxin Deng East China Normal University, Junjie Wu Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Yuan Feng Centre for Quantum Software and Information, University of Technology Sydney, Australia File Attached | ||
15:35 - 17:45 | |||
15:35 32mTalk | The Correctness of a Code Generator for a Functional Language VMCAI | ||
16:07 32mTalk | Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification VMCAI Jack Garzella University of Utah, Marek S. Baranowski University of Utah, Shaobo He University of Utah, Zvonimir Rakamaric University of Utah | ||
16:40 32mCoffee break | Mini Break VMCAI | ||
17:12 32mTalk | Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction VMCAI Oren Ish-Shalom Tel Aviv University, Israel, Shachar Itzhaky Technion, Israel, Noam Rinetzky Tel Aviv University, Sharon Shoham Tel Aviv university | ||
16:50 - 17:50 | |||
16:50 20mTalk | Extending Modern C++ for Heterogeneous Quantum-Classical Computing PLanQC Alexander McCaskey Oak Ridge National Laboratory, Tiffany Mintz Oak Ridge National Laboratory, Eugene Dumitrescu Oak Ridge National Laboratory, Sarah Powers Oak Ridge National Laboratory, Shirley Moore Oak Ridge National Laboratory, Pavel Lougovski Oak Ridge National Laboratory | ||
17:10 20mTalk | Formalization of a Programming Language for Quantum Circuits with Measurement and Classical Control PLanQC Dongho LEE LRI / CEA LIST, Univ Paris Saclay, Sébastien Bardin CEA LIST, Valentin Perrelle CEA, LIST, France, Benoit Valiron LRI, CentraleSupelec, Univ. Paris Saclay File Attached | ||
17:30 20mTalk | Automated distribution of quantum circuits via hypergraph partitioning PLanQC Link to publication DOI Pre-print Media Attached File Attached | ||
Mon 20 JanDisplayed time zone: Saskatchewan, Central America change
Mon 20 Jan
Displayed time zone: Saskatchewan, Central America change
08:30 - 10:00 | Logical Engines and ApplicationsPADL at Bacchus Chair(s): Ekaterina Komendantskaya Heriot-Watt University, UK | ||
08:30 15mDay opening | Opening PADL | ||
08:45 50mTalk | Invited Talk: Logical Engines for Cloud Configurations PADL | ||
09:35 25mTalk | Interactive Text Graph Mining with a Prolog-based Dialog Engine PADL | ||
09:00 - 10:00 | |||
09:00 60mTutorial | [T6] Verifying Probabilistic Properties with Couplings TutorialFest Justin Hsu University of Wisconsin-Madison, USA File Attached | ||
09:00 - 10:00 | |||
09:00 60mTalk | Relational reasoning using concurrent separation logic ADSL Media Attached File Attached | ||
09:00 - 10:00 | |||
09:00 60mTutorial | [T2] Verified Quantum Computing TutorialFest Robert Rand University of Maryland Pre-print | ||
09:00 - 10:00 | Opening & Keynote Talk 1PEPM at Frontenac Chair(s): Casper Bach Poulsen Delft University of Technology, Zhenjiang Hu Peking University | ||
09:00 5mDay opening | Opening PEPM | ||
09:05 55mTalk | Network Verification: Past, Present, and Future PEPM Nate Foster Cornell University | ||
09:00 - 10:00 | |||
09:00 60mTalk | Invited talk: Matching Logic: The Foundation of the K Framework CPP Grigore Roşu University of Illinois at Urbana-Champaign, Xiaohong Chen University of Illinois at Urbana-Champaign DOI Media Attached | ||
09:00 - 10:00 | |||
09:00 60mTutorial | [T1] Building Program Reasoning Tools using LLVM and Z3 TutorialFest Elizabeth Dinella University of Pennsylvania, Pardis Pashakhanloo University of Pennsylvania, Anthony Canino , Mayur Naik University of Pennsylvania Pre-print | ||
09:00 - 10:00 | |||
09:00 60mTutorial | [T3] Synthesizing Programs from Types TutorialFest Nadia Polikarpova University of California, San Diego Link to publication File Attached | ||
09:00 - 10:00 | |||
09:00 60mTalk | Model Checking for Safe Autonomy VMCAI Rajeev Alur University of Pennsylvania | ||
10:30 - 12:30 | |||
10:30 2hTutorial | [T6] Verifying Probabilistic Properties with Couplings TutorialFest Justin Hsu University of Wisconsin-Madison, USA File Attached | ||
10:30 - 12:00 | Answer Set Programming SystemsPADL at Bacchus Chair(s): Neng-Fa Zhou CUNY Brooklyn College and Graduate Center | ||
10:30 25mTalk | AQuA: ASP-based Visual Question Answering PADL | ||
10:55 15mShort-paper | Diagnosing Data Pipeline Failures Using Action Languages: A Progress Report PADL | ||
11:10 15mShort-paper | VRASP: A Virtual Reality Environment for Learning Answer Set Programming PADL Vinh The Nguyen Texas Tech University, Yuanlin Zhang , Kwanghee Jung , Wanli Xing , Tommy Dang Texas Tech University | ||
11:25 35mOther | Panel: Programming with logic for the masses PADL Nikolaj Bjørner Microsoft Research, Paul Tarau University of North Texas, Eduardo Blanco , Kinjal Basu , Farhad Shakerin , Gopal Gupta , Alex Brik , Jeffrey Xu UCLA, Vinh The Nguyen Texas Tech University, Yuanlin Zhang , Kwanghee Jung , Wanli Xing , Tommy Dang Texas Tech University | ||
10:30 - 12:30 | |||
10:30 30mResearch paper | Extending the Profile Abstraction for Complete Entailment Checking of Symbolic Heaps of Bounded Treewidth ADSL File Attached | ||
11:00 30mResearch paper | Steel: scaling up memory reasoning for F* ADSL File Attached | ||
11:30 30mResearch paper | Strong-Separation Logic ADSL File Attached | ||
12:00 30mResearch paper | The Lower Bound of Decidable Entailments in Separation Logic with Inductive Definitions ADSL Pre-print File Attached | ||
10:30 - 12:30 | |||
10:30 2hTutorial | [T2] Verified Quantum Computing TutorialFest Robert Rand University of Maryland Pre-print | ||
10:30 - 12:30 | |||
10:30 35mTalk | Dependently-Typed Multi-Stage Programming Revisited (invited talk) PEPM Atsushi Igarashi Kyoto University, Japan | ||
11:05 25mResearch paper | High-Fidelity Metaprogramming with Separator Syntax Trees PEPM DOI | ||
11:30 15mBreak | Mini Break 1 PEPM | ||
11:45 25mResearch paper | Module Generation without Regret PEPM Yuhi Sato University of Tsukuba, Yukiyoshi Kameyama University of Tsukuba, Japan, Takahisa Watanabe University of Tsukuba, Japan DOI | ||
12:10 20mShort-paper | GOOL: A Generic Object-Oriented Language PEPM Jacques Carette McMaster University, Brooks MacLachlan McMaster University, Spencer Smith McMaster University, Computing and Software Department DOI Pre-print File Attached | ||
10:30 - 11:35 | |||
10:30 21mTalk | A Verified Packrat Parser Interpreter for Parsing Expression Grammars CPP DOI Pre-print Media Attached | ||
10:51 22mTalk | Proof Pearl: Braun Trees CPP Tobias Nipkow Technische Universität München, Thomas Sewell Chalmers University of Technology, Sweden DOI Pre-print Media Attached | ||
11:13 22mTalk | FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq CPP DOI Pre-print Media Attached | ||
10:30 - 12:30 | |||
10:30 2hTutorial | [T1] Building Program Reasoning Tools using LLVM and Z3 TutorialFest Elizabeth Dinella University of Pennsylvania, Pardis Pashakhanloo University of Pennsylvania, Anthony Canino , Mayur Naik University of Pennsylvania Pre-print | ||
10:30 - 12:30 | |||
10:30 2hTutorial | [T3] Synthesizing Programs from Types TutorialFest Nadia Polikarpova University of California, San Diego Link to publication File Attached | ||
10:30 - 12:30 | |||
10:30 30mResearch paper | A Systematic Approach to Abstract Interpretation of Program Transformations VMCAI Pre-print | ||
11:00 30mTalk | Sharing Ghost Variables in a Collection of Abstract Domains VMCAI | ||
11:30 30mCoffee break | Mini Break VMCAI | ||
12:00 30mTalk | Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation VMCAI Oren Ish-Shalom Tel Aviv University, Israel, Shachar Itzhaky Technion, Israel, Roman Manevich Mellanox Technologies, Noam Rinetzky Tel Aviv University | ||
11:45 - 12:30 | |||
11:45 22mTalk | Verifying x86 Instruction Implementations CPP Shilpi Goel Centaur Technology, Inc., Anna Slobodova Centaur Technology, Inc., Rob Sumners Centaur Technology, Inc., Sol Swords Centaur Technology, Inc. DOI Pre-print File Attached | ||
12:07 22mTalk | Frying the Egg, Roasting The Chicken: Unit Deletions in DRAT Proofs CPP DOI Pre-print Media Attached | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
13:30 - 15:00 | Memory and Real-Time in Functional ProgrammingPADL at Bacchus Chair(s): John Hughes Chalmers University of Technology, Sweden | ||
13:30 25mTalk | On the Effects of Integrating Region-based Memory Managemen and Generational Garbage Collection in ML PADL | ||
13:55 25mTalk | RTMLton: An SML Runtime for Real-Time Systems PADL | ||
14:20 25mTalk | A Timed IO Monad PADL David Janin Bordeaux INP / CNRS LaBRI / Bordeaux University | ||
14:45 15mOther | Panel: Memory and real-time programming in practice PADL Martin Elsman University of Copenhagen, Denmark, Niels Hallenberg , Bhargav Shivkumar , Jeffrey Murphy , Lukasz Ziarek SUNY Buffalo, USA, David Janin Bordeaux INP / CNRS LaBRI / Bordeaux University | ||
14:00 - 15:05 | |||
14:00 65mTalk | SLEdge: Bounded Model Checking in Separation Logic ADSL File Attached | ||
14:00 - 15:05 | Stateless Model Checking Algorithms and Tools for Strong and Weak Memory Models (I)TutorialFest at Endymion | ||
14:00 65mTutorial | [T5] Stateless Model Checking Algorithms and Tools for Strong and Weak Memory Models TutorialFest Konstantinos (Kostis) Sagonas Uppsala University, Sweden | ||
14:00 - 15:05 | |||
14:00 60mTalk | Reasoning about Progress of Concurrent Objects PEPM Xinyu Feng Nanjing University | ||
14:00 - 15:05 | |||
14:00 21mTalk | An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction CPP Yannick Zakowski University of Pennsylvania, Paul He University of Pennsylvania, Chung-Kil Hur Seoul National University, Steve Zdancewic University of Pennsylvania DOI Pre-print Media Attached File Attached | ||
14:21 21mTalk | Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar CPP Qingxiang Wang University of Innsbruck, Chad Brown Czech Technical University in Prague, Cezary Kaliszyk University of Innsbruck, Josef Urban Czech Technical University in Prague DOI Pre-print | ||
14:43 21mTalk | REPLICA: REPL Instrumentation for Coq Analysis CPP Talia Ringer University of Washington, Alex Sanchez-Stern University of California, San Diego, Dan Grossman University of Washington, Sorin Lerner University of California, San Diego DOI Pre-print Media Attached | ||
14:00 - 15:05 | |||
14:00 65mTutorial | [T4] Proving Semantic Type Soundness in Iris TutorialFest Derek Dreyer MPI-SWS, Robbert Krebbers Delft University of Technology, Amin Timany imec-Distrinet KU-Leuven Link to publication File Attached | ||
14:00 - 15:05 | |||
14:00 65mTutorial | [T7] Programming and Reasoning with Kleene Algebra with Tests TutorialFest Nate Foster Cornell University, Dexter Kozen Cornell University, Alexandra Silva University College London File Attached | ||
14:00 - 15:05 | |||
14:00 32mTalk | Synthesizing Environment Invariants for Modular Hardware Verification VMCAI Hongce Zhang Princeton University, Weikun Yang Princeton University, Grigory Fedyukovich Florida State University, Aarti Gupta Princeton University, Sharad Malik Princeton University | ||
14:32 32mTalk | Systematic Classification of Attackers via Bounded Model Checking VMCAI Eric Rothstein-Morris Singapore University of Technology and Design, Jun Sun Singapore Management University, Singapore, Sudipta Chattopadhyay Singapore University of Technology and Design | ||
15:30 - 17:00 | |||
15:30 25mTalk | Flexible Graph Matching and Graph Edit Distance Using Answer Set Programming PADL | ||
15:55 25mTalk | On Repairing Web Services Workflows PADL | ||
16:20 40mTalk | Competitive Programming with PiCat PADL Neng-Fa Zhou CUNY Brooklyn College and Graduate Center | ||
15:35 - 17:45 | |||
15:35 65mTalk | Programs Synthesis with Separation Logic ADSL Nadia Polikarpova University of California, San Diego | ||
16:40 65mTalk | Local Reasoning for Global Graph Properties ADSL Thomas Wies New York University | ||
15:35 - 17:35 | Stateless Model Checking Algorithms and Tools for Strong and Weak Memory Models (II)TutorialFest at Endymion | ||
15:35 2hTutorial | [T5] Stateless Model Checking Algorithms and Tools for Strong and Weak Memory Models TutorialFest Konstantinos (Kostis) Sagonas Uppsala University, Sweden | ||
15:35 - 17:45 | Sessions 3 & 4PEPM at Frontenac Chair(s): Atsushi Igarashi Kyoto University, Japan, Jeremy Yallop University of Cambridge, UK | ||
15:35 35mTalk | Frex: Free extensions for normalisation by evaluation (invited talk) PEPM Ohad Kammar University of Edinburgh Media Attached | ||
16:10 25mResearch paper | Symbolic Bisimulation for Open and Parameterized System PEPM DOI File Attached | ||
16:35 15mBreak | Mini Break 2 PEPM | ||
16:50 35mTalk | Acumen: A Domain-Specific Language for Cyber-Physical Systems (invited talk) PEPM | ||
17:25 20mShort-paper | An approach to generating text-based IDEs with syntax completion from syntax specification PEPM Isao Sasano Shibaura Institute of Technology DOI | ||
15:35 - 16:40 | |||
15:35 21mTalk | Verified Programming of Turing Machines in Coq CPP Yannick Forster Saarland University, Fabian Kunze Saarland University, Maximilian Wuttke Saarland University DOI Pre-print Media Attached | ||
15:56 21mTalk | A Functional Proof Pearl: Inverting the Ackermann Hierarchy CPP Linh Tran National University of Singapore, Anshuman Mohan National University of Singapore, Aquinas Hobor National University of Singapore DOI Pre-print Media Attached | ||
16:18 21mTalk | Undecidability of Higher-Order Unification Formalised in Coq CPP DOI Pre-print Media Attached | ||
15:35 - 17:35 | |||
15:35 2hTutorial | [T4] Proving Semantic Type Soundness in Iris TutorialFest Derek Dreyer MPI-SWS, Robbert Krebbers Delft University of Technology, Amin Timany imec-Distrinet KU-Leuven Link to publication File Attached | ||
15:35 - 17:35 | |||
15:35 2hTutorial | [T7] Programming and Reasoning with Kleene Algebra with Tests TutorialFest Nate Foster Cornell University, Dexter Kozen Cornell University, Alexandra Silva University College London File Attached | ||
15:35 - 17:45 | |||
15:35 32mTalk | Cheap CTL Compassion in NuSMV VMCAI Daniel Hausmann Friedrich-Alexander-Universität Erlangen-Nürnberg, Tadeusz Litak FAU Erlangen-Nuremberg, INF 8, Christoph Rauch FAU Erlangen-Nürnberg, Lehrstuhl 8, Matthias Zinner FAU Erlangen-Nürnberg | ||
16:07 32mTalk | A Cooperative Parallelization Approach for Property-Directed k-Induction VMCAI Martin Blicha Università della Svizzera italiana, Antti Hyvärinen Università della Svizzera Italiana, Matteo Marescotti Università della Svizzera Italiana, Natasha Sharygina USI Lugano, Switzerland | ||
16:40 32mCoffee break | Mini Break VMCAI | ||
17:12 32mTalk | Generalized Property-Directed Reachability for Hybrid Systems VMCAI Link to publication Pre-print | ||
16:50 - 17:56 | Homotopy Type Theory and PC chairs' reportCPP at Maurepas Chair(s): Floris van Doorn University of Pittsburgh | ||
16:50 22mTalk | Cubical Synthetic Homotopy Theory CPP Anders Mörtberg Department of Mathematics, Stockholm University, Loïc Pujet Gallinette Project-Team, Inria DOI Pre-print Media Attached File Attached | ||
17:12 22mTalk | Three equivalent ordinal notation systems in Cubical Agda CPP Fredrik Nordvall Forsberg University of Strathclyde, Chuangjie Xu Ludwig-Maximilians-Universität München, Neil Ghani University of Strathclyde DOI Pre-print Media Attached File Attached | ||
17:34 22mTalk | PC Chairs' report CPP DOI Media Attached File Attached | ||
Tue 21 JanDisplayed time zone: Saskatchewan, Central America change
Tue 21 Jan
Displayed time zone: Saskatchewan, Central America change
08:30 - 10:00 | |||
08:30 50mTalk | Invited Talk: Symbolic Reasoning About Machine Learning Systems PADL Adnan Darwiche UCLA | ||
09:20 25mTalk | Exploiting Database Systems and Treewidth for Counting PADL | ||
09:45 15mShort-paper | Whitebox Induction of Default Rules Using High-Utility Itemset Mining PADL | ||
09:00 - 10:00 | Morning 1PLMW at Ile de France III (IDF III) Chair(s): Stephanie Balzer Carnegie Mellon University, USA | ||
09:00 10mDay opening | Opening PLMW Brigitte Pientka McGill University | ||
09:10 50mTalk | How to Write Papers So People Can Read ThemMentoring Event PLMW Derek Dreyer MPI-SWS File Attached | ||
09:00 - 10:00 | |||
09:00 60mTalk | Invited talk: Proof Assistants at the Hardware-Software Interface CPP Adam Chlipala Massachusetts Institute of Technology DOI Media Attached | ||
09:00 - 10:00 | |||
09:00 10mDay opening | Opening Plenary HASE | ||
09:10 60mTutorial | Interactive Knowledge Shares HASE Peter O'Hearn Facebook, Philippa Gardner Imperial College London, Muralidaran Vijayaraghavan SiFive, Peter Sewell University of Cambridge | ||
09:00 - 10:00 | |||
09:00 60mTalk | Invited talk: Nonstandard Interpretation in Pyro LAFI Pre-print | ||
09:00 - 10:00 | |||
09:00 30mTalk | How to Win First-Order Safety Games VMCAI Helmut Seidl Technische Universität München, Christian Müller Technical University of Munich, Bernd Finkbeiner Saarland University | ||
09:30 30mTalk | Improving Parity Game Solvers with Justifications VMCAI Ruben Lapauw Katholieke Universiteit Leuven, Maurice Bruynooghe Katholieke Universiteit Leuven, Marc Denecker Katholieke Universiteit Leuven | ||
10:30 - 12:00 | Small Languages and ImplementationPADL at Bacchus Chair(s): James Cheney University of Edinburgh, UK | ||
10:30 25mTalk | Explanations for Dynamic Programming PADL | ||
10:55 25mTalk | A DSL for Integer Range Reasoning: Partition, Interval and Mapping Diagrams PADL | ||
11:20 15mShort-paper | Variability-aware Datalog PADL | ||
11:35 25mOther | Panel: Reasoning for machine learning at large PADL Adnan Darwiche UCLA, Johannes K. Fichte TU Dresden, Markus Hecher , Patrick Thier , Stefan Woltran , Farhad Shakerin , Gopal Gupta , Martin Erwig Oregon State University, Prashant Kumar , Alan Fern , Johannes Eriksson , Masoumeh Parsa , Ramy Shahin , Marsha Chechik University of Toronto | ||
10:30 - 12:30 | |||
10:30 2hOther | Ally Skills SessionMentoring Event Ally Skills Session | ||
10:30 - 12:30 | Morning 2PLMW at Ile de France III (IDF III) Chair(s): Robbert Krebbers Delft University of Technology | ||
10:30 40mTalk | Making Progress Under Uncertainty in SMT Solving, Research, and LifeMentoring Event PLMW Lindsey Kuper University of California, Santa Cruz Media Attached | ||
11:10 40mTalk | Research as a collaborative effortMentoring Event PLMW Marco Gaboardi Boston University Media Attached File Attached | ||
11:50 40mTalk | Theorem provers are a P.L. researcher's best friendMentoring Event PLMW Xavier Leroy Collège de France Media Attached File Attached | ||
10:30 - 11:35 | |||
10:30 21mTalk | Coq à la Carte - A Practical Approach to Modular Syntax with Binders CPP DOI Pre-print Media Attached | ||
10:51 21mTalk | A Mechanized Formalization of GraphQL CPP Tomás Díaz IMFD Chile, Federico Olmedo University of Chile & IMFD Chile, Éric Tanter University of Chile DOI Pre-print Media Attached File Attached | ||
11:13 21mTalk | ConCert: A Smart Contract Certification Framework in Coq CPP Danil Annenkov Concordium Blockchain Research Center, Aarhus University, Jakob Botsch Nielsen Concordium Blockchain Research Center, Aarhus University, Bas Spitters Concordium Blockchain Research Center, Aarhus University DOI Pre-print Media Attached File Attached | ||
10:30 - 12:30 | |||
10:30 2hMeeting | Working Sessions I HASE | ||
10:30 - 12:30 | |||
10:30 30mTalk | A Differential-form Pullback Programming Language for Higher-order Reverse-mode Automatic Differentiation LAFI | ||
11:00 30mTalk | A Monad for Point Processes LAFI File Attached | ||
11:30 30mTalk | Denotational Semantics for Differentiable Programming with Manifolds LAFI Jesse Sigal University of Edinburgh | ||
12:00 30mTalk | Backpropagation in the Simply Typed Lambda-calculus with Linear Negation LAFI | ||
10:30 - 12:30 | |||
10:30 30mTalk | Language Inclusion for Finite Prime Event Structures VMCAI Andreas Fellner AIT - Austrian Institute of Technology, Thorsten Tarrach Austrian Institute of Technology, Georg Weissenbacher Technische Universität Wien | ||
11:00 30mTalk | Promptness and Bounded Fairness in Concurrent and Parameterized Systems VMCAI Swen Jacobs CISPA Helmholtz Center for Information Security, Mouhammad Sakr Saarland University, Martin Zimmermann University of Liverpool | ||
11:30 30mCoffee break | Mini Break VMCAI | ||
12:00 30mTalk | Solving LIA* Using Approximations VMCAI Maxwell Levatich Yale, Nikolaj Bjørner Microsoft Research, Ruzica Piskac Yale University, USA, Sharon Shoham Tel Aviv university | ||
11:45 - 12:30 | |||
11:45 22mTalk | Formalising Oblivious Transfer in the Semi-Honest and Malicious Model in CryptHOL CPP David Butler Alan Turing Institute, David Aspinall University of Edinburgh, Adria Gascon Alan Turing Institute DOI Pre-print Media Attached | ||
12:07 22mTalk | Verified Security of BLT Signature Scheme CPP Denis Firsov Guardtime AS, Ahto Buldas Tallinn University of Technology, Ahto Truu Guardtime AS, Risto Laanoja Guardtime AS DOI Pre-print Media Attached File Attached | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
13:30 - 15:00 | Invited Experience and Direction SessionPADL at Bacchus Chair(s): Konstantinos (Kostis) Sagonas Uppsala University, Sweden, David Warren Stony Brook University | ||
13:30 30mTalk | Invited Talk: Relational Artificial Intelligence PADL Molham Aref Relational.ai | ||
14:00 30mTalk | Invited Talk: Learning Interpretable Rules from Structured Data PADL Mayur Naik University of Pennsylvania | ||
14:30 30mTalk | Invited Talk: An Introduction to the Imandra Automated Reasoning System PADL Grant Passmore Imandra Inc. | ||
14:00 - 15:05 | Afternoon 1PLMW at Ile de France III (IDF III) Chair(s): Justin Hsu University of Wisconsin-Madison, USA | ||
14:00 65mTalk | PanelMentoring Event PLMW William J. Bowman University of British Columbia, Kenny Foner Galois, Andrew K. Hirsch Max Planck Institute for Software Systems, Taro Sekiyama National Institute of Informatics, Juliana Franco Microsoft Research, Cambridge, Hannah Gommerstadt Vassar College Media Attached | ||
14:00 - 15:05 | |||
14:00 21mTalk | Formalizing Determinacy of Concurrent Revisions CPP Roy Overbeek Vrije Universiteit Amsterdam DOI Pre-print Media Attached | ||
14:21 21mTalk | Formalizing π-calculus in Guarded Cubical Agda CPP DOI Pre-print Media Attached File Attached | ||
14:43 21mTalk | Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages CPP Arjen Rouvoet Delft University of Technology, Casper Bach Poulsen Delft University of Technology, Robbert Krebbers Delft University of Technology, Eelco Visser Delft University of Technology DOI Pre-print Media Attached File Attached | ||
14:00 - 15:05 | |||
13:30 45mTutorial | Peer Skillshare HASE Sarah de Haas Google Research | ||
14:00 - 15:05 | |||
14:00 30mTalk | Divide, Conquer, and Combine: a New Inference Strategy for Probabilistic Programs with Stochastic Support LAFI Yuan Zhou University of Oxford, Hongseok Yang KAIST, Yee Whye Teh University of Oxford, Tom Rainforth Department of Statistics, University of Oxford | ||
14:32 15mTalk | MetaPPL: Inference Algorithms as First-Class Generative Models LAFI Alexander K. Lew Massachusetts Institute of Technology, USA, Benjamin Sherman Massachusetts Institute of Technology, USA, Marco Cusumano-Towner MIT-CSAIL, Austin Garrett MIT, Ben Zinberg MIT, Vikash K. Mansinghka MIT, Michael Carbin Massachusetts Institute of Technology File Attached | ||
14:49 16mTalk | Monte Carlo Semantic Differencing of Probabilistic Programs LAFI | ||
14:00 - 15:05 | |||
14:00 32mTalk | Formalizing and Checking Multilevel Consistency VMCAI Ahmed Bouajjani IRIF, Université Paris Diderot, Constantin Enea IRIF, University Paris Diderot & CNRS, Madhavan Mukund Chennai Mathematical Institute, Gautham Shenoy R Chennai Mathematical Institute, S.P. Suresh Chennai Mathematical Institute | ||
14:32 32mTalk | Practical Abstractions for Automated Verification of Shared-Memory Concurrency VMCAI Wytse Oortwijn ETH Zürich, Dilian Gurov KTH Royal Institute of Technology, Marieke Huisman University of Twente | ||
15:30 - 17:00 | Invited Experience and Direction Session (Continued)PADL at Bacchus Chair(s): Y. Annie Liu Stony Brook University, Konstantinos (Kostis) Sagonas Uppsala University, Sweden, David Warren Stony Brook University | ||
15:30 30mTalk | Invited Talk: We Are All Poor Schmucks: On the Value of Gradual Types PADL Philip Wadler University of Edinburgh, UK | ||
16:00 45mOther | Panel: Experience and Direction PADL I: Molham Aref Relational.ai, I: Mayur Naik University of Pennsylvania, I: Grant Passmore Imandra Inc., I: Philip Wadler University of Edinburgh, UK | ||
16:45 15mDay closing | Closing PADL | ||
15:35 - 17:45 | |||
15:35 2hOther | POPLmark 15 Year Retrospective Panel POPLmark 15 Year Retrospective Panel | ||
15:35 - 17:45 | |||
15:40 60mTalk | How Can I Academia When My Brain Can't Even? Mental Health in Grad School and BeyondMentoring Event PLMW Kenny Foner Galois Media Attached | ||
16:40 10mCoffee break | Mini break PLMW | ||
16:50 45mTalk | Automated Program Verification using Abductive ReasoningMentoring Event PLMW Işıl Dillig University of Texas Austin Media Attached | ||
15:35 - 16:40 | |||
15:35 21mTalk | Formalising perfectoid spaces CPP Patrick Massot Université Paris Sud, Kevin Buzzard Imperial College London, Johan Commelin Universität Freiburg DOI Pre-print Media Attached File Attached | ||
15:56 21mTalk | A Constructive Formalization of the Weak Perfect Graph Theorem CPP Abhishek Kr Singh Tata Institute of Fundamental Research Mumbai, Raja Natarajan Tata Institute of Fundamental Research Mumbai DOI Pre-print Media Attached File Attached | ||
16:18 21mTalk | Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq CPP DOI Pre-print Media Attached | ||
15:35 - 17:45 | |||
14:30 2hMeeting | Working Sessions II HASE | ||
16:30 75mDay closing | Closing Plenary HASE | ||
15:35 - 17:45 | |||
15:35 30mTalk | Coinductive Trees for Exact Inference of Probabilistic Programs LAFI Alexander Bagnall Ohio University, Gordon Stewart Ohio University, Anindya Banerjee IMDEA Software Institute | ||
16:05 30mTalk | Name generation and Higher-order Probabilistic Programming (Or is new=rnd?) LAFI File Attached | ||
16:35 30mTalk | Density Functions of Statistical Probabilistic Programs LAFI | ||
17:05 30mTalk | Probabilistic Programming around Gaussian Processes LAFI David Tolpin PUB+ | ||
17:35 10mDay closing | Closing LAFI | ||
15:35 - 17:45 | |||
15:35 2h10mOther | Panel "The Future of Software Verification" at VMCAI VMCAI Lenore Zuck UIC, Michael Whalen Amazon Web Services and the University of Minnesota, Natarajan Shankar SRI International, USA, Andreas Podelski University of Freiburg, Germany, Dirk Beyer LMU Munich | ||
16:50 - 17:56 | |||
16:50 22mTalk | The Poincaré-Bendixson Theorem in Isabelle/HOL CPP DOI Pre-print Media Attached | ||
17:12 22mTalk | A Formal Proof of the Independence of the Continuum Hypothesis CPP DOI Pre-print Media Attached | ||
17:34 22mTalk | The Lean mathematical library CPP DOI Pre-print Media Attached File Attached | ||
Wed 22 JanDisplayed time zone: Saskatchewan, Central America change
Wed 22 Jan
Displayed time zone: Saskatchewan, Central America change
07:45 - 08:45 | |||
07:45 60mSocial Event | Mentoring BreakfastMentoring Event Mentoring Breakfasts | ||
08:45 - 09:00 | Welcome + SIGPLAN Award CeremonyResearch Papers at Ile de France II (IDF II) Chair(s): Lars Birkedal Aarhus University, Jens Palsberg University of California, Los Angeles, Brigitte Pientka McGill University | ||
08:45 15mDay opening | Welcome + SIGPLAN Award Ceremony Research Papers Media Attached | ||
09:00 - 10:00 | Invited TalkResearch Papers at Ile de France II (IDF II) Chair(s): Brigitte Pientka McGill University | ||
09:00 60mTalk | Can Programming Languages Research impact Deep Learning 2.0?Invited Talk Research Papers Martin Vechev ETH Zürich Media Attached | ||
10:30 - 11:35 | Probabilistic ProgrammingResearch Papers at Ile de France II (IDF II) Chair(s): Alexandra Silva University College London | ||
10:30 21mTalk | Towards Verified Stochastic Variational Inference for Probabilistic Programs Research Papers Link to publication DOI Media Attached | ||
10:51 21mTalk | Trace Types and Denotational Semantics for Sound Programmable Inference in Probabilistic Languages Research Papers Alexander K. Lew Massachusetts Institute of Technology, USA, Marco Cusumano-Towner MIT-CSAIL, Benjamin Sherman Massachusetts Institute of Technology, USA, Michael Carbin Massachusetts Institute of Technology, Vikash K. Mansinghka MIT Link to publication DOI Media Attached | ||
11:13 21mTalk | Semantics of Higher-Order Probabilistic Programs with Conditioning Research Papers Link to publication DOI Media Attached File Attached | ||
10:30 - 11:35 | Complexity / Decision ProceduresResearch Papers at Ile de France III (IDF III) Chair(s): Roopsha Samanta Purdue University | ||
10:30 21mTalk | The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space Research Papers Yannick Forster Saarland University, Fabian Kunze Saarland University, Marc Roth Saarland University and MMCI and Merton College, Oxford University Link to publication DOI Pre-print Media Attached | ||
10:51 21mTalk | Complexity and Information in Invariant Inference Research Papers Yotam M. Y. Feldman Tel Aviv University, Neil Immerman University of Massachusetts, Amherst, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv university Link to publication DOI Media Attached | ||
11:13 21mTalk | Parameterized Verification under TSO is PSPACE-Complete Research Papers Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Sweden, Rojin Rezvan Sharif University Link to publication DOI | ||
11:45 - 12:30 | Reasoning about Program Complexity/EfficiencyResearch Papers at Ile de France II (IDF II) Chair(s): Thomas Wies New York University | ||
11:45 22mTalk | Recurrence Extraction for Functional Programs through Call-by-Push-Value Research Papers Alex Kavvos Aarhus University, Edward Morehouse Wesleyan University, Daniel R. Licata Wesleyan University, Norman Danner Wesleyan University Link to publication DOI File Attached | ||
12:07 22mTalk | Liquidate Your Assets: Reasoning About Resource Usage in Liquid Haskell Research Papers Martin Adam Thomas Handley University of Nottingham, Niki Vazou IMDEA Software Institute, Graham Hutton University of Nottingham, UK Link to publication DOI Media Attached File Attached | ||
11:45 - 12:30 | SynthesisResearch Papers at Ile de France III (IDF III) Chair(s): Mohsen Lesani University of California, Riverside | ||
11:45 22mTalk | Program Synthesis by Type-Guided Abstraction Refinement Research Papers Zheng Guo University of California, San Diego, Michael B. James University of California, San Diego, David Justo University of California, San Diego, Jiaxiao Zhou University of California, San Diego, Ziteng Wang University of California, San Diego, Ranjit Jhala University of California, San Diego, Nadia Polikarpova University of California, San Diego Link to publication DOI Media Attached File Attached | ||
12:07 22mTalk | Synthesizing Replacement Classes Research Papers Link to publication DOI Media Attached File Attached | ||
12:30 - 14:00 | |||
12:30 90mLunch | LGBTQ LunchMentoring Event LGBTQ Lunch | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:05 | |||
14:00 21mTalk | The Future is Ours: Prophecy Variables in Separation Logic Research Papers Ralf Jung MPI-SWS, Rodolphe Lepigre MPI-SWS, Gaurav Parthasarathy ETH Zurich, Marianna Rapoport University of Waterloo, Amin Timany imec-Distrinet KU-Leuven, Derek Dreyer MPI-SWS, Bart Jacobs imec-DistriNet, Dept. CS, KU Leuven Link to publication DOI Media Attached | ||
14:21 21mTalk | Spy Game: Verifying a Local Generic Solver in Iris Research Papers Paulo Emílio de Vilhena Inria, François Pottier Inria, France, Jacques-Henri Jourdan CNRS, LRI, Université Paris-Sud Link to publication DOI Media Attached File Attached | ||
14:43 21mTalk | Actris: Session-Type Based Reasoning in Separation Logic Research Papers Jonas Kastberg Hinrichsen IT University of Copenhagen, Jesper Bengtson IT University of Copenhagen, Robbert Krebbers Delft University of Technology Link to publication DOI Media Attached File Attached | ||
14:00 - 15:05 | Gradual Typing / Language DesignResearch Papers at Ile de France III (IDF III) Chair(s): Jeremy G. Siek Indiana University, USA | ||
14:00 21mTalk | What is Decidable about Gradual Types? Research Papers Zeina Migeed University of California, Los Angeles, Jens Palsberg University of California, Los Angeles Link to publication DOI Media Attached File Attached | ||
14:21 21mTalk | Graduality and Parametricity: Together Again for the First Time Research Papers Max S. New Northeastern University, Dustin Jamner Northeastern University, USA, Amal Ahmed Northeastern University, USA Link to publication DOI Media Attached | ||
14:43 21mTalk | Does Blame Shifting Work? Research Papers Lukas Lazarek Northwestern University, Alexis King Northwestern University, Samanvitha Sundar Northwestern University, Robert Bruce Findler Northwestern University, USA, Christos Dimoulas PLT @ Northwestern University Link to publication DOI Media Attached | ||
15:35 - 16:40 | Automatic Differentiation / Kleene AlgebraResearch Papers at Ile de France II (IDF II) Chair(s): Lars Birkedal Aarhus University | ||
15:35 21mTalk | A Simple Differentiable Programming Language Research Papers Link to publication DOI Media Attached | ||
15:56 21mTalk | Backpropagation in the Simply Typed Lambda-calculus with Linear Negation Research Papers Link to publication DOI Media Attached File Attached | ||
16:18 21mTalk | Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear TimeDistinguished Paper Research Papers Steffen Smolka Cornell University, Nate Foster Cornell University, Justin Hsu University of Wisconsin-Madison, USA, Tobias Kappé University College London, Dexter Kozen Cornell University, Alexandra Silva University College London Link to publication DOI Media Attached | ||
15:35 - 16:40 | Concurrency / MemoryResearch Papers at Ile de France III (IDF III) Chair(s): Susmit Sarkar University of St. Andrews | ||
15:35 21mTalk | Persistency Semantics of the Intel-x86 Architecture Research Papers Azalea Raad MPI-SWS, Germany, John Wickerson Imperial College London, Gil Neiger Intel Corporation, Viktor Vafeiadis MPI-SWS, Germany Link to publication DOI Media Attached | ||
15:56 21mTalk | Reductions for Safety Proofs Research Papers Link to publication DOI Media Attached | ||
16:18 21mTalk | RustBelt Meets Relaxed Memory Research Papers Hoang-Hai Dang MPI-SWS, Jacques-Henri Jourdan CNRS, LRI, Université Paris-Sud, Jan-Oliver Kaiser MPI-SWS, Derek Dreyer MPI-SWS Link to publication DOI Media Attached | ||
16:50 - 17:35 | Synthesis and Decision ProceduresResearch Papers at Ile de France II (IDF II) Chair(s): Roopsha Samanta Purdue University | ||
16:50 22mTalk | Visualization by Example Research Papers Chenglong Wang University of Washington, USA, Yu Feng University of California, Santa Barbara, Rastislav Bodík University of Washington, Alvin Cheung University of California, Berkeley, Işıl Dillig University of Texas Austin Link to publication DOI Media Attached | ||
17:12 22mTalk | Deciding Memory Safety for Single-Pass Heap-Manipulating Programs Research Papers Umang Mathur University of Illinois at Urbana-Champaign, Adithya Murali University of Illinois at Urbana-Champaign, Paul Krogmeier University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign, Mahesh Viswanathan University of Illinois at Urbana-Champaign Link to publication DOI Pre-print Media Attached File Attached | ||
16:50 - 19:00 | |||
16:50 2h10mPoster | SRC Poster Session Student Research Competition | ||
17:35 - 18:35 | |||
17:35 60mSocial Event | Social Hour (Supported by Facebook) Research Papers | ||
Thu 23 JanDisplayed time zone: Saskatchewan, Central America change
Thu 23 Jan
Displayed time zone: Saskatchewan, Central America change
07:45 - 09:00 | |||
07:45 75mSocial Event | Mentoring BreakfastMentoring Event Mentoring Breakfasts | ||
09:00 - 10:00 | Invited TalkResearch Papers at Ile de France II (IDF II) Chair(s): Brigitte Pientka McGill University | ||
09:00 60mTalk | What is a Secure Programming Language? Invited Talk Research Papers Cristina Cifuentes Oracle Labs Link to publication Media Attached | ||
10:30 - 11:35 | Types and EffectsResearch Papers at Ile de France II (IDF II) Chair(s): Dominique Devriese Vrije Universiteit Brussel | ||
10:30 21mTalk | Binders by Day, Labels by Night: Effect Instances via Lexically Scoped Handlers Research Papers Dariusz Biernacki University of Wrocław, Maciej Piróg University of Wrocław, Piotr Polesiuk University of Wrocław, Filip Sieczkowski University of Wrocław Link to publication DOI Media Attached | ||
10:51 21mTalk | The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects Research Papers Link to publication DOI Media Attached | ||
11:13 21mTalk | SyTeCi: Automating Contextual Equivalence for Higher-Order Programs with References Research Papers Guilhem Jaber LS2N, Université de Nantes Link to publication DOI Media Attached | ||
11:45 - 12:30 | Dynamic Program AnalysisResearch Papers at Ile de France II (IDF II) Chair(s): Peter Thiemann University of Freiburg, Germany | ||
11:45 22mTalk | Fast, Sound, and Effectively Complete Dynamic Race Prediction Research Papers Andreas Pavlogiannis Aarhus University Link to publication DOI Media Attached File Attached | ||
12:07 22mTalk | Detecting Floating-Point Errors via Atomic Conditions Research Papers Daming Zou Peking University, Muhan Zeng Peking University, Yingfei Xiong Peking University, Zhoulai Fu IT University of Copenhagen, Denmark, Lu Zhang Peking University, Zhendong Su ETH Zurich Link to publication DOI Media Attached File Attached | ||
11:45 - 12:30 | Datalog, OO + Functional ProgrammingResearch Papers at Ile de France III (IDF III) Chair(s): Brigitte Pientka McGill University | ||
11:45 22mTalk | Seminaïve Evaluation for a Higher-Order Functional LanguageDistinguished Paper Research Papers Neel Krishnaswami Computer Laboratory, University of Cambridge, Michael Arntzenius University of Birmingham, UK Link to publication DOI Media Attached File Attached | ||
12:07 22mTalk | Decomposition Diversity with Symmetric Data and Codata Research Papers David Binder University of Tübingen, Julian Jabs University of Tübingen, Ingo Skupin University of Tübingen, Klaus Ostermann University of Tübingen, Germany Link to publication DOI Media Attached | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:05 | Type SystemsResearch Papers at Ile de France II (IDF II) Chair(s): Peter Thiemann University of Freiburg, Germany | ||
14:00 21mTalk | Undecidability of D<: and Its Decidable FragmentsDistinguished Paper Research Papers Link to publication DOI Media Attached File Attached | ||
14:21 21mTalk | Decidable Subtyping for Path Dependent Types Research Papers Julian Mackay Victoria University of Wellington, Alex Potanin Victoria University of Wellington, Jonathan Aldrich Carnegie Mellon University, Lindsay Groves Victoria University of Wellington Link to publication DOI Media Attached | ||
14:43 21mTalk | Dependent Type Systems as Macros Research Papers Stephen Chang Northeastern University, Michael Ballantyne PLT @ Northeastern University, Milo Turner PLT @ Northeastern University, William J. Bowman University of British Columbia Link to publication DOI Media Attached File Attached | ||
14:00 - 15:30 | |||
14:00 90mTalk | SRC Finalists Presentations Student Research Competition | ||
15:35 - 16:40 | Program LogicsResearch Papers at Ile de France II (IDF II) Chair(s): Chung-Kil Hur Seoul National University | ||
15:35 21mTalk | Deductive Verification with Ghost Monitors Research Papers Martin Clochard ETH Zürich, Claude Marché Inria Saclay & Université Paris-Saclay, Andrei Paskevich LRI, Université Paris-Sud & CNRS Link to publication DOI Media Attached | ||
15:56 21mTalk | The Next 700 Relational Program Logics Research Papers Kenji Maillard Inria Nantes & University of Chile, Cătălin Hriţcu Inria Paris, Exequiel Rivas Inria Paris, Antoine Van Muylder Inria Paris and Paris 7 Link to publication DOI Media Attached File Attached | ||
16:18 21mTalk | Incorrectness Logic Research Papers Peter O'Hearn Facebook Link to publication DOI Media Attached | ||
15:35 - 16:40 | Probabilistic ProgrammingResearch Papers at Ile de France III (IDF III) Chair(s): Ohad Kammar University of Edinburgh | ||
15:35 21mTalk | A Language for Probabilistically Oblivious Computation Research Papers David Darais University of Vermont, Ian Sweet University of Maryland, Chang Liu Citadel Securities, Michael Hicks University of Maryland Link to publication DOI Media Attached File Attached | ||
15:56 21mTalk | PλωNK: Functional Probabilistic NetKAT Research Papers Link to publication DOI Media Attached File Attached | ||
16:18 21mTalk | Optimal Approximate Sampling From Discrete Probability Distributions Research Papers Feras Saad Massachusetts Institute of Technology, Cameron Freer Massachusetts Institute of Technology, Martin C. Rinard MIT, Vikash K. Mansinghka MIT Link to publication DOI Media Attached File Attached | ||
16:50 - 18:00 | |||
16:50 70mMeeting | Business Meeting & SRC Awards Research Papers Media Attached | ||
18:00 - 19:00 | |||
18:00 60mSocial Event | Social Hour (Supported by Microsoft) Research Papers | ||
19:00 - 21:00 | |||
19:00 2hDinner | W@POPL DinnerMentoring Event W@POPL Dinner | ||
Fri 24 JanDisplayed time zone: Saskatchewan, Central America change
Fri 24 Jan
Displayed time zone: Saskatchewan, Central America change
07:45 - 09:00 | |||
07:45 75mSocial Event | Mentoring BreakfastMentoring Event Mentoring Breakfasts | ||
09:00 - 10:00 | |||
09:00 60mTalk | Probabilistic ProgrammingInvited Talk Research Papers Hongseok Yang KAIST Media Attached File Attached | ||
10:30 - 11:35 | Type SystemsResearch Papers at Ile de France II (IDF II) Chair(s): Dominique Devriese Vrije Universiteit Brussel | ||
10:30 21mTalk | Kind Inference for DatatypesDistinguished Paper Research Papers Ningning Xie University of Toronto, Richard A. Eisenberg Bryn Mawr College, USA, Bruno C. d. S. Oliveira The University of Hong Kong, Hong Kong Link to publication DOI Media Attached | ||
10:51 21mTalk | Partial Type Constructors: Or, Making Ad Hoc Datatypes Less Ad Hoc Research Papers Mark Jones Portland State University, J. Garrett Morris University of Kansas, USA, Richard A. Eisenberg Bryn Mawr College, USA Link to publication DOI Media Attached File Attached | ||
11:13 21mTalk | Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation Research Papers Link to publication DOI Media Attached File Attached | ||
11:45 - 12:30 | Concurrent Programming & Session TypesResearch Papers at Ile de France II (IDF II) Chair(s): Susmit Sarkar University of St. Andrews | ||
11:45 22mTalk | Label-Dependent Session Types Research Papers Link to publication DOI Media Attached | ||
12:07 22mTalk | Par means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs Research Papers Link to publication DOI Media Attached | ||
11:45 - 12:30 | Probabilistic Reasoning and VerificationResearch Papers at Ile de France III (IDF III) Chair(s): Arthur Azevedo de Amorim Carnegie Mellon University, USA | ||
11:45 22mTalk | Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time Research Papers Peixin Wang Shanghai Jiao Tong University, Hongfei Fu Shanghai Jiao Tong University, Krishnendu Chatterjee IST Austria, Yuxin Deng East China Normal University, Ming Xu East China Normal University Link to publication DOI Media Attached | ||
12:07 22mTalk | Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification Research Papers Marcel Hark RWTH Aachen University, Germany, Benjamin Lucien Kaminski RWTH Aachen University, Germany, Jürgen Giesl RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University Link to publication DOI Media Attached File Attached | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:05 | Semantics of Probabilistic & Quantum ProgrammingResearch Papers at Ile de France II (IDF II) Chair(s): Alexandra Silva University College London | ||
14:00 21mTalk | Full Abstraction for the Quantum Lambda-Calculus Research Papers Link to publication DOI Media Attached File Attached | ||
14:21 21mTalk | Relational Proofs for Quantum Programs Research Papers Gilles Barthe MPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Justin Hsu University of Wisconsin-Madison, USA, Mingsheng Ying University of Technology Sydney, Australia / Institute of Software at Chinese Academy of Sciences, China/ Department of Computer Science and Technology, Tsinghua University., Nengkun Yu University of Technology Sydney, Australia, Li Zhou Max Planck Institute for Security and Privacy/Tsinghua University Link to publication DOI Pre-print Media Attached File Attached | ||
14:43 21mTalk | A Probabilistic Separation Logic Research Papers Gilles Barthe MPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Justin Hsu University of Wisconsin-Madison, USA, Kevin Liao Max Planck Institute for Security and Privacy Link to publication DOI Media Attached | ||
14:00 - 15:05 | Language DesignResearch Papers at Ile de France III (IDF III) Chair(s): Amin Timany imec-Distrinet KU-Leuven | ||
14:00 21mTalk | Stacked Borrows: An Aliasing Model for Rust Research Papers Link to publication DOI Media Attached File Attached | ||
14:21 21mTalk | Executable Formal Semantics for the POSIX Shell Research Papers Link to publication DOI Media Attached File Attached | ||
14:43 21mTalk | Disentanglement in Nested-Parallel Programs Research Papers Sam Westrick Carnegie Mellon University, Rohan Yadav Carnegie Mellon University, Matthew Fluet Rochester Institute of Technology, Umut A. Acar Carnegie Mellon University Link to publication DOI Media Attached File Attached | ||
15:35 - 16:40 | Semantics & Type TheoryResearch Papers at Ile de France II (IDF II) Chair(s): Arthur Azevedo de Amorim Carnegie Mellon University, USA | ||
15:35 21mTalk | Taylor Subsumes Scott, Berry, Kahn and PlotkinDistinguished Paper Research Papers Link to publication DOI Media Attached File Attached | ||
15:56 21mTalk | Reduction Monads and Their Signatures Research Papers Benedikt Ahrens University of Birmingham, United Kingdom, André Hirschowitz Université Côte d'Azur, Ambroise Lafont Inria, France, Marco Maggesi Università di Firenze Link to publication DOI Media Attached | ||
16:18 21mTalk | Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq Research Papers Matthieu Sozeau Inria, Simon Boulier Inria, Yannick Forster Saarland University, Nicolas Tabareau Inria, Théo Winterhalter Inria — LS2N Link to publication DOI Media Attached File Attached | ||
16:40 - 17:40 | |||
16:40 60mSocial Event | Social Hour (Supported by Tezos) Research Papers | ||
Sat 25 JanDisplayed time zone: Saskatchewan, Central America change
Sat 25 Jan
Displayed time zone: Saskatchewan, Central America change
09:00 - 10:00 | |||
09:00 60mTalk | SMTCoq: Safe and efficient automation in Coq (Keynote) CoqPL Chantal Keller LRI, Université Paris-Sud File Attached | ||
09:00 - 10:00 | |||
09:00 30mTalk | Gradual Typing as if Types Mattered WGT Pre-print | ||
09:30 30mTalk | Fully Abstract from Static to Gradual WGT Koen Jacobs KU Leuven, Amin Timany imec-Distrinet KU-Leuven, Dominique Devriese Vrije Universiteit Brussel Pre-print | ||
09:00 - 10:00 | |||
09:00 5mDay opening | PriSC Introduction PriSC Dominique Devriese Vrije Universiteit Brussel File Attached | ||
09:05 55mIndustry talk | Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing PriSC Media Attached | ||
10:30 - 12:30 | |||
10:30 30mTalk | Deriving Instances with Dependent Types CoqPL Arthur Azevedo de Amorim Carnegie Mellon University, USA File Attached | ||
11:00 30mTalk | The use of Coq for Common Criteria Evaluations CoqPL Yves Bertot INRIA, Maxime Dénès Inria, Vincent Laporte Inria, Arnaud Fontaine ANSSI, Thomas Letan ANSSI File Attached | ||
11:30 30mTalk | Verifying concurrent Go code in Coq with Goose CoqPL Tej Chajed Massachusetts Institute of Technology, USA, Joseph Tassarotti Boston College, M. Frans Kaashoek Massachusetts Institute of Technology, USA, Nickolai Zeldovich Massachusetts Institute of Technology, USA Link to publication File Attached | ||
12:00 30mTalk | A Tutorial on Equations CoqPL Matthieu Sozeau Inria Media Attached File Attached | ||
10:30 - 12:30 | |||
10:30 30mTalk | Gradual Algebraic Data Types WGT Michael Greenberg Pomona College, Stefan Malewski University of Santiago de Chile, Éric Tanter University of Chile Pre-print File Attached | ||
11:00 30mTalk | Gradual Typing for Extensibility by Rows WGT Pre-print | ||
11:30 30mTalk | Foreign Function Typing: Semantic Type Soundness for FFIs WGT Pre-print | ||
12:00 30mTalk | Space-Efficient Monotonic References WGT Pre-print | ||
12:30 - 14:00 | |||
12:30 90mLunch | Lunch Catering | ||
14:00 - 15:05 | |||
14:00 60mTalk | Autosubst 2: Mechanising binders in Coq (Keynote) CoqPL Kathrin Stark Princeton University, USA File Attached | ||
14:00 - 15:05 | |||
14:00 32mTalk | Hypercoercions and a Framework for Equivalence of Cast Calculi WGT Kuang-Chen Lu Indiana University Bloomington, Jeremy G. Siek Indiana University, USA, Andre Kuhlenschmidt Indiana University Pre-print | ||
14:32 32mTalk | Space-Efficient Gradual Typing in Coercion-Passing Style WGT Yuya Tsuda Kyoto University, Atsushi Igarashi Kyoto University, Japan, Tomoya Tabuchi Kyoto University Pre-print | ||
14:00 - 15:05 | |||
14:00 24mTalk | Exploits as Insecure Compilation PriSC Jennifer Paykin Galois, Inc., Eric Mertens Galois, Inc., Mark Tullsen Galois, Inc, Luke Maurer Galois, Inc, Benoit Razet Galois, Inc, Alexander Bakst Galois, Inc, Scott Moore Galois, Inc Pre-print Media Attached File Attached | ||
14:24 24mTalk | Universal Composability is Secure Compilation PriSC Marco Patrignani Stanford University & CISPA , Riad S. Wahby Stanford University, USA, Robert Künnemann CISPA, Saarland University Media Attached File Attached | ||
14:48 8mTalk | Short Talk: Automatically Eliminating Speculative Leaks With Blade PriSC Marco Vassena CISPA Helmholtz Center for Information Security, Klaus v. Gleissenthall University of California at San Diego, USA, Rami Gökhan Kıcı University of California at San Diego, USA Media Attached File Attached | ||
14:56 8mTalk | Short Talk: Everparse PriSC Tahina Ramananandro Microsoft Research, n.n. Media Attached | ||
15:35 - 17:45 | Contributed Talks & Coq DevelopersCoqPL at Maurepas Chair(s): Robbert Krebbers Delft University of Technology, Joseph Tassarotti Boston College | ||
15:35 30mTalk | Towards Formally Verified Just-in-Time compilation CoqPL Aurèle Barrière Univ Rennes, IRISA, Sandrine Blazy Univ Rennes- IRISA, David Pichardie Univ Rennes, ENS Rennes, IRISA File Attached | ||
16:05 30mTalk | A Coq Library of Undecidable Problems CoqPL Yannick Forster Saarland University, Dominique Larchey-Wendling CNRS, LORIA, Andrej Dudenhefner Saarland University, Edith Heiter Saarland University, Dominik Kirst Saarland University, Fabian Kunze Saarland University, Gert Smolka Saarland University, Simon Spies Saarland University, Dominik Wehr Saarland University, Universiteit van Amsterdam, Maximilian Wuttke Saarland University Media Attached File Attached | ||
16:35 15mBreak | Short break CoqPL | ||
16:50 45mDemonstration | Session with the Coq Development Team CoqPL | ||
15:35 - 17:45 | |||
15:35 32mTalk | Gradual Verification of Recursive Heap Data Structures WGT Jenna DiVincenzo (Wise) Carnegie Mellon University, Johannes Bader Facebook, Jonathan Aldrich Carnegie Mellon University, Éric Tanter University of Chile, Joshua Sunshine Carnegie Mellon University Pre-print | ||
16:07 33mTalk | Gradual Program Analysis WGT Samuel Estep Liberty University, Jenna DiVincenzo (Wise) Carnegie Mellon University, Jonathan Aldrich Carnegie Mellon University, Éric Tanter University of Chile, Johannes Bader Facebook, Joshua Sunshine Carnegie Mellon University Pre-print | ||
16:40 10mBreak | Minibreak WGT | ||
16:50 30mTalk | Blame tracking at higher fidelity WGT Jakub Zalewski University of Edinburgh, James McKinna University of Edinburgh, J. Garrett Morris University of Kansas, USA, Philip Wadler University of Edinburgh, UK Pre-print | ||
17:20 25mDay closing | Discussion on gradual typing and WGT21 WGT | ||
15:35 - 17:45 | Compartmentalization, memory safety, and isolationPriSC at Rosalie Chair(s): Marco Patrignani Stanford University & CISPA , Jonathan Protzenko Microsoft Research, Redmond | ||
15:35 24mTalk | Flexible Tag-based Policies for Compartmentalized C PriSC Sean Anderson Portland State University, Andrew Tolmach Portland State University, CHR Chhak Portland State University Media Attached File Attached | ||
15:59 24mTalk | Mechanized Reasoning about a Capability Machine PriSC Media Attached | ||
16:23 24mTalk | Securing Interruptible Enclaves PriSC Matteo Busi Università di Pisa - Dipartimento di Informatica, Job Noorman imec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium, Jo Van Bulck imec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium, Letterio Galletta IMT School for Advanced Studies, Pierpaolo Degano Università di Pisa - Dipartimento di Informatica, Jan Tobias Mühlberg imec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium, Frank Piessens KU Leuven Media Attached File Attached | ||
16:47 10mBreak | Mini-break PriSC | ||
16:57 24mTalk | WebAssembly as an Intermediate Language for Provably-Safe Software Sandboxing PriSC Jay Bosamiya Carnegie Mellon University, Benjamin Lim Carnegie Mellon University, Bryan Parno Carnegie Mellon University Media Attached File Attached | ||
17:21 24mTalk | Memory Safety Preservation for WebAssembly PriSC Marco Vassena CISPA Helmholtz Center for Information Security, Marco Patrignani Stanford University & CISPA Link to publication Media Attached File Attached | ||