Conference Dates
Conference Dates are in time zone (GMT-06:00) Saskatchewan, Central America, and may differ from the viewed time zone.
Rooms
Tracks
Badges
Your Program
Sun 19 Jan Times are displayed in time zone: Saskatchewan, Central America change
Sun 19 Jan
Times are displayed in time zone: Saskatchewan, Central America change
09:00 - 10:00: Introduction and Invited TalksPLanQC at Maurepas Chair(s): Robert RandUniversity of Maryland | |||
| 09:00 - 09:30 Talk | Invited Talk: Quantum Computing for Programming Languages Researchers PLanQC Media Attached File Attached | ||
| 09:30 - 10:00 Talk | Invited Talk: Dependently Typed Quantum Programming in Proto-Quipper PLanQC Media Attached | ||
| 09:00 - 10:00 Talk | The Siren Song of Temporal Synthesis VMCAI Moshe VardiRice University | ||
| 10:30 - 11:00 Talk | Invited Talk: Q# - Going Beyond Quantum Circuits PLanQC Media Attached | ||
| 11:00 - 11:30 Talk | Invited Talk: Resource-Efficient Quantum Computing by Breaking Abstractions PLanQC Media Attached File Attached | ||
| 11:30 - 11:50 Talk | Tuning up entanglement through the cloud using Qiskit-OpenPulse PLanQC Thomas AlexanderIBM T.J. Watson Research Center, New York, USA, Naoki KanazawaIBM Research, Tokyo, Japan, Daniel EggerIBM Research, Zurich, Switzerland, Ali Javadi-AbhariIBM T.J. Watson Research Center, New York, USA, David C. McKayIBM T.J. Watson Research Center, New York, USA | ||
| 11:50 - 12:10 Talk | Tracking Errors through Types in Quantum Programs PLanQC Kesha HietalaUniversity of Maryland, Robert RandUniversity of Maryland, Michael HicksUniversity of Maryland Pre-print Media Attached File Attached | ||
| 12:10 - 12:30 Talk | Quantum CPOs PLanQC | ||
| 10:30 - 11:00 Talk | Witnessing Secure Compilation VMCAI | ||
| 11:00 - 11:30 Talk | BackFlow: Backward Context-sensitive Flow Reconstruction of Taint Analysis Results VMCAI Pietro FerraraUniversità Ca' Foscari, Venezia, Italy, Luca OlivieriJuliaSoft SRL, Fausto SpotoU. Verona | ||
| 11:30 - 12:00 Coffee break | Mini Break VMCAI | ||
| 12:00 - 12:30 Talk | Fixing Code That Explodes Under Symbolic Evaluation VMCAI Sorawee PorncharoenwaseUniversity of Washington, James BornholtUniversity of Texas at Austin, Emina TorlakUniversity of Washington | ||
| 12:30 - 14:00 Lunch | Lunch Catering | ||
| 14:00 - 14:20 Talk | Runtime Analysis of Quantum Programs: A Formal Approach PLanQC Pre-print File Attached | ||
| 14:20 - 14:40 Talk | Qbricks: formal verification in quantum computing PLanQC Christopĥe CharetonCEA, LIST, France, Sebastien BardinCEA LIST, François BobotCEA, Valentin PerrelleCEA, LIST, France, Benoit ValironLRI, CentraleSupelec, Univ. Paris Saclay File Attached | ||
| 14:40 - 15:05 Talk | Merged Talk: A Verified Optimizer for Quantum Circuits & Verified Translation Between Low-Level Quantum Languages PLanQC Kesha HietalaUniversity of Maryland, Kartik SinghalUniversity of Chicago, Robert RandUniversity of Maryland, Shih-Han HungUniversity of Maryland, Xiaodi WuUniversity of Maryland, College Park, Michael HicksUniversity of Maryland Media Attached | ||
| 14:00 - 15:05 Talk | Safety and Robustness for Deep Learning with Provable Guarantees VMCAI Marta KwiatkowskaUniversity of Oxford | ||
| 15:35 - 15:55 Talk | Optimal Two-Qubit Circuits for Universal Fault-Tolerant Quantum Computation PLanQC Andrew N. GlaudellUniversity of Maryland, Neil Julien RossDalhousie University, Jacob M. TaylorUniversity of Maryland Pre-print Media Attached File Attached | ||
| 15:55 - 16:15 Talk | Context-Sensitive and Duration-Aware Qubit Mapping for Various NISQ Devices PLanQC Yu ZhangUniversity of Science and Technology of China, Haowei DengUniversity of Science and Technology of China, Quanxi LiUniversity of Science and Technology of China Pre-print Media Attached | ||
| 16:15 - 16:35 Talk | Quingo: A Domain Specific Language for Quantum Computing with NISQ Features PLanQC Xiang FuInstitute for Quantum Information & State Key Laboratory of High Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Jintao YuState Key Laboratory of Mathematical Engineering and Advanced Computing, Zhengzhou, China, Xing SuCollege of Meteorology and Oceanography, National University of Defense Technology, Changsha, China, Hanru JiangCenter for Quantum Computing, Peng Cheng Laboratory, Shenzhen, China, Hua WuShanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China, Dong ChenDepartment of Computing Science, College of Computer, National University of Defense Technology, Changsha, China, Fucheng ChengCenter for Quantum Computing, Peng Cheng Laboratory, Shenzhen, China, Xi DengCenter for Quantum Computing, Peng Cheng Laboratory, Shenzhen, China, Jinrong ZhangCenter for Quantum Computing, Peng Cheng Laboratory, Shenzhen, China, Lei JinSchool of Information Engineering, Zhengzhou University, Zhengzhou, China, Yihang YangSchool of Information Engineering, Zhengzhou University, Zhengzhou, China, Le XuSchool of Information Engineering, Zhengzhou University, Zhengzhou, China, Chunchao HuSchool of Information Engineering, Zhengzhou University, Zhengzhou, China, Anqi HuangInstitute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Guangyao HuangInstitute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Xiaogang QiangInstitute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Mingtang DengInstitute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Ping XuInstitute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Wanwei LiuNational University of Defense Technology, Yuxin DengEast China Normal University, Junjie WuInstitute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Yuan FengCentre for Quantum Software and Information, University of Technology Sydney, Australia File Attached | ||
| 15:35 - 16:07 Talk | The Correctness of a Code Generator for a Functional Language VMCAI | ||
| 16:07 - 16:40 Talk | Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification VMCAI Jack GarzellaUniversity of Utah, Marek S. BaranowskiUniversity of Utah, Shaobo HeUniversity of Utah, Zvonimir RakamaricUniversity of Utah | ||
| 16:40 - 17:12 Coffee break | Mini Break VMCAI | ||
| 17:12 - 17:45 Talk | Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction VMCAI Oren Ish-ShalomTel Aviv University, Israel, Shachar ItzhakyTechnion, Israel, Noam RinetzkyTel Aviv University, Sharon ShohamTel Aviv university | ||
16:50 - 17:50: Quantum-Classical CommunicationPLanQC at Maurepas Chair(s): Michael HicksUniversity of Maryland | |||
| 16:50 - 17:10 Talk | Extending Modern C++ for Heterogeneous Quantum-Classical Computing PLanQC Alexander McCaskeyOak Ridge National Laboratory, Tiffany MintzOak Ridge National Laboratory, Eugene DumitrescuOak Ridge National Laboratory, Sarah PowersOak Ridge National Laboratory, Shirley MooreOak Ridge National Laboratory, Pavel LougovskiOak Ridge National Laboratory | ||
| 17:10 - 17:30 Talk | Formalization of a Programming Language for Quantum Circuits with Measurement and Classical Control PLanQC Dongho LEELRI / CEA LIST, Univ Paris Saclay, Sebastien BardinCEA LIST, Valentin PerrelleCEA, LIST, France, Benoit ValironLRI, CentraleSupelec, Univ. Paris Saclay File Attached | ||
| 17:30 - 17:50 Talk | Automated distribution of quantum circuits via hypergraph partitioning PLanQC Link to publication DOI Pre-print Media Attached File Attached | ||
Mon 20 Jan Times are displayed in time zone: Saskatchewan, Central America change
Mon 20 Jan
Times are displayed in time zone: Saskatchewan, Central America change
08:30 - 10:00: Logical Engines and ApplicationsPADL at Bacchus Chair(s): Ekaterina KomendantskayaHeriot-Watt University, UK | |||
| 08:30 - 08:45 Day opening | Opening PADL | ||
| 08:45 - 09:35 Talk | Invited Talk: Logical Engines for Cloud Configurations PADL | ||
| 09:35 - 10:00 Talk | Interactive Text Graph Mining with a Prolog-based Dialog Engine PADL | ||
| 09:00 - 10:00 Tutorial | [T6] Verifying Probabilistic Properties with Couplings TutorialFest Justin HsuUniversity of Wisconsin-Madison, USA File Attached | ||
| 09:00 - 10:00 Talk | Relational reasoning using concurrent separation logic ADSL Media Attached File Attached | ||
| 09:00 - 10:00 Tutorial | [T2] Verified Quantum Computing TutorialFest Robert RandUniversity of Maryland Pre-print | ||
09:00 - 10:00: Opening & Keynote Talk 1PEPM at Frontenac Chair(s): Casper Bach PoulsenDelft University of Technology, Zhenjiang HuPeking University | |||
| 09:00 - 09:05 Day opening | Opening PEPM | ||
| 09:05 - 10:00 Talk | Network Verification: Past, Present, and Future PEPM Nate FosterCornell University | ||
| 09:00 - 10:00 Talk | Invited talk: Matching Logic: The Foundation of the K Framework CPP Grigore RoşuUniversity of Illinois at Urbana-Champaign, Xiaohong ChenUniversity of Illinois at Urbana-Champaign DOI Media Attached | ||
| 09:00 - 10:00 Tutorial | [T1] Building Program Reasoning Tools using LLVM and Z3 TutorialFest Elizabeth DinellaUniversity of Pennsylvania, Pardis PashakhanlooUniversity of Pennsylvania, Anthony Canino, Mayur NaikUniversity of Pennsylvania Pre-print | ||
| 09:00 - 10:00 Tutorial | [T3] Synthesizing Programs from Types TutorialFest Nadia PolikarpovaUniversity of California, San Diego Link to publication File Attached | ||
| 09:00 - 10:00 Talk | Model Checking for Safe Autonomy VMCAI Rajeev AlurUniversity of Pennsylvania | ||
| 10:30 - 12:30 Tutorial | [T6] Verifying Probabilistic Properties with Couplings TutorialFest Justin HsuUniversity of Wisconsin-Madison, USA File Attached | ||
10:30 - 12:00: Answer Set Programming SystemsPADL at Bacchus Chair(s): Neng-Fa ZhouCUNY Brooklyn College and Graduate Center | |||
| 10:30 - 10:55 Talk | AQuA: ASP-based Visual Question Answering PADL | ||
| 10:55 - 11:10 Short-paper | Diagnosing Data Pipeline Failures Using Action Languages: A Progress Report PADL | ||
| 11:10 - 11:25 Short-paper | VRASP: A Virtual Reality Environment for Learning Answer Set Programming PADL Vinh The NguyenTexas Tech University, Yuanlin Zhang, Kwanghee Jung, Wanli Xing, Tommy DangTexas Tech University | ||
| 11:25 - 12:00 Other | Panel: Programming with logic for the masses PADL Nikolaj BjørnerMicrosoft Research, Paul TarauUniversity of North Texas, Eduardo Blanco, Kinjal Basu, Farhad Shakerin, Gopal Gupta, Alex Brik, Jeffrey XuUCLA, Vinh The NguyenTexas Tech University, Yuanlin Zhang, Kwanghee Jung, Wanli Xing, Tommy DangTexas Tech University | ||
| 10:30 - 11:00 Research paper | Extending the Profile Abstraction for Complete Entailment Checking of Symbolic Heaps of Bounded Treewidth ADSL File Attached | ||
| 11:00 - 11:30 Research paper | Steel: scaling up memory reasoning for F* ADSL File Attached | ||
| 11:30 - 12:00 Research paper | Strong-Separation Logic ADSL File Attached | ||
| 12:00 - 12:30 Research paper | The Lower Bound of Decidable Entailments in Separation Logic with Inductive Definitions ADSL Pre-print File Attached | ||
| 10:30 - 12:30 Tutorial | [T2] Verified Quantum Computing TutorialFest Robert RandUniversity of Maryland Pre-print | ||
10:30 - 12:30: Sessions 1 & 2PEPM at Frontenac Chair(s): Ohad KammarUniversity of Edinburgh, Walid Taha | |||
| 10:30 - 11:05 Talk | Dependently-Typed Multi-Stage Programming Revisited (invited talk) PEPM Atsushi IgarashiKyoto University, Japan | ||
| 11:05 - 11:30 Research paper | High-Fidelity Metaprogramming with Separator Syntax Trees PEPM DOI | ||
| 11:30 - 11:45 Break | Mini Break 1 PEPM | ||
| 11:45 - 12:10 Research paper | Module Generation without Regret PEPM Yuhi SatoUniversity of Tsukuba, Yukiyoshi KameyamaUniversity of Tsukuba, Japan, Takahisa WatanabeUniversity of Tsukuba, Japan DOI | ||
| 12:10 - 12:30 Short-paper | GOOL: A Generic Object-Oriented Language PEPM Jacques CaretteMcMaster University, Brooks MacLachlanMcMaster University, Spencer SmithMcMaster University, Computing and Software Department DOI Pre-print File Attached | ||
| 10:30 - 10:51 Talk | A Verified Packrat Parser Interpreter for Parsing Expression Grammars CPP DOI Pre-print Media Attached | ||
| 10:51 - 11:13 Talk | Proof Pearl: Braun Trees CPP DOI Pre-print Media Attached | ||
| 11:13 - 11:35 Talk | FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq CPP DOI Pre-print Media Attached | ||
| 10:30 - 12:30 Tutorial | [T1] Building Program Reasoning Tools using LLVM and Z3 TutorialFest Elizabeth DinellaUniversity of Pennsylvania, Pardis PashakhanlooUniversity of Pennsylvania, Anthony Canino, Mayur NaikUniversity of Pennsylvania Pre-print | ||
| 10:30 - 12:30 Tutorial | [T3] Synthesizing Programs from Types TutorialFest Nadia PolikarpovaUniversity of California, San Diego Link to publication File Attached | ||
| 10:30 - 11:00 Research paper | A Systematic Approach to Abstract Interpretation of Program Transformations VMCAI Pre-print | ||
| 11:00 - 11:30 Talk | Sharing Ghost Variables in a Collection of Abstract Domains VMCAI | ||
| 11:30 - 12:00 Coffee break | Mini Break VMCAI | ||
| 12:00 - 12:30 Talk | Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Manipulating Procedures for Automatic Test Generation VMCAI Oren Ish-ShalomTel Aviv University, Israel, Shachar ItzhakyTechnion, Israel, Roman ManevichMellanox Technologies, Noam RinetzkyTel Aviv University | ||
| 11:45 - 12:07 Talk | Verifying x86 Instruction Implementations CPP Shilpi GoelCentaur Technology, Inc., Anna SlobodovaCentaur Technology, Inc., Rob SumnersCentaur Technology, Inc., Sol SwordsCentaur Technology, Inc. DOI Pre-print File Attached | ||
| 12:07 - 12:30 Talk | Frying the Egg, Roasting The Chicken: Unit Deletions in DRAT Proofs CPP DOI Pre-print Media Attached | ||
| 12:30 - 14:00 Lunch | Lunch Catering | ||
13:30 - 15:00: Memory and Real-Time in Functional ProgrammingPADL at Bacchus Chair(s): John HughesChalmers University of Technology, Sweden | |||
| 13:30 - 13:55 Talk | On the Effects of Integrating Region-based Memory Managemen and Generational Garbage Collection in ML PADL | ||
| 13:55 - 14:20 Talk | RTMLton: An SML Runtime for Real-Time Systems PADL | ||
| 14:20 - 14:45 Talk | A Timed IO Monad PADL David JaninBordeaux INP / CNRS LaBRI / Bordeaux University | ||
| 14:45 - 15:00 Other | Panel: Memory and real-time programming in practice PADL Martin ElsmanUniversity of Copenhagen, Denmark, Niels Hallenberg, Bhargav Shivkumar, Jeffrey Murphy, Lukasz ZiarekSUNY Buffalo, USA, David JaninBordeaux INP / CNRS LaBRI / Bordeaux University | ||
| 14:00 - 15:05 Talk | 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 - 15:05 Tutorial | [T5] Stateless Model Checking Algorithms and Tools for Strong and Weak Memory Models TutorialFest Konstantinos (Kostis) SagonasUppsala University, Sweden | ||
14:00 - 15:05: Keynote Talk 2PEPM at Frontenac Chair(s): Casper Bach PoulsenDelft University of Technology | |||
| 14:00 - 15:00 Talk | Reasoning about Progress of Concurrent Objects PEPM Xinyu FengNanjing University | ||
| 14:00 - 14:21 Talk | An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction CPP Yannick ZakowskiUniversity of Pennsylvania, Paul HeUniversity of Pennsylvania, Chung-Kil HurSeoul National University, Steve ZdancewicUniversity of Pennsylvania DOI Pre-print Media Attached File Attached | ||
| 14:21 - 14:43 Talk | Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar CPP Qingxiang WangUniversity of Innsbruck, Chad BrownCzech Technical University in Prague, Cezary KaliszykUniversity of Innsbruck, Josef UrbanCzech Technical University in Prague DOI Pre-print | ||
| 14:43 - 15:05 Talk | REPLICA: REPL Instrumentation for Coq Analysis CPP Talia RingerUniversity of Washington, Alex Sanchez-SternUniversity of California, San Diego, Dan GrossmanUniversity of Washington, Sorin LernerUniversity of California, San Diego DOI Pre-print Media Attached | ||
| 14:00 - 15:05 Tutorial | [T4] Proving Semantic Type Soundness in Iris TutorialFest Derek DreyerMPI-SWS, Robbert KrebbersDelft University of Technology, Amin Timanyimec-Distrinet KU-Leuven Link to publication File Attached | ||
14:00 - 15:05: Programming and Reasoning with Kleene Algebra with Tests (I)TutorialFest at SHANGRI-LA | |||
| 14:00 - 15:05 Tutorial | [T7] Programming and Reasoning with Kleene Algebra with Tests TutorialFest Nate FosterCornell University, Dexter KozenCornell University, Alexandra SilvaUniversity College London File Attached | ||
| 14:00 - 14:32 Talk | Synthesizing Environment Invariants for Modular Hardware Verification VMCAI Hongce ZhangPrinceton University, Weikun YangPrinceton University, Grigory FedyukovichFlorida State University, Aarti GuptaPrinceton University, Sharad MalikPrinceton University | ||
| 14:32 - 15:05 Talk | Systematic Classification of Attackers via Bounded Model Checking VMCAI Eric Rothstein-MorrisSingapore University of Technology and Design, Jun SunSingapore Management University, Singapore, Sudipta ChattopadhyaySingapore University of Technology and Design | ||
| 15:30 - 15:55 Talk | Flexible Graph Matching and Graph Edit Distance Using Answer Set Programming PADL | ||
| 15:55 - 16:20 Talk | On Repairing Web Services Workflows PADL | ||
| 16:20 - 17:00 Talk | Competitive Programming with PiCat PADL Neng-Fa ZhouCUNY Brooklyn College and Graduate Center | ||
| 15:35 - 16:40 Talk | Programs Synthesis with Separation Logic ADSL Nadia PolikarpovaUniversity of California, San Diego | ||
| 16:40 - 17:45 Talk | Local Reasoning for Global Graph Properties ADSL Thomas WiesNew York University | ||
15:35 - 17:35: Stateless Model Checking Algorithms and Tools for Strong and Weak Memory Models (II)TutorialFest at Endymion | |||
| 15:35 - 17:35 Tutorial | [T5] Stateless Model Checking Algorithms and Tools for Strong and Weak Memory Models TutorialFest Konstantinos (Kostis) SagonasUppsala University, Sweden | ||
15:35 - 17:45: Sessions 3 & 4PEPM at Frontenac Chair(s): Jeremy YallopUniversity of Cambridge, UK, Atsushi IgarashiKyoto University, Japan | |||
| 15:35 - 16:10 Talk | Frex: Free extensions for normalisation by evaluation (invited talk) PEPM Ohad KammarUniversity of Edinburgh Media Attached | ||
| 16:10 - 16:35 Research paper | Symbolic Bisimulation for Open and Parameterized System PEPM DOI File Attached | ||
| 16:35 - 16:50 Break | Mini Break 2 PEPM | ||
| 16:50 - 17:25 Talk | Acumen: A Domain-Specific Language for Cyber-Physical Systems (invited talk) PEPM | ||
| 17:25 - 17:45 Short-paper | An approach to generating text-based IDEs with syntax completion from syntax specification PEPM Isao SasanoShibaura Institute of Technology DOI | ||
15:35 - 16:40: Decidability and complexityCPP at Maurepas Chair(s): Kathrin StarkPrinceton University, USA | |||
| 15:35 - 15:56 Talk | Verified Programming of Turing Machines in Coq CPP Yannick ForsterSaarland University, Fabian KunzeSaarland University, Maximilian WuttkeSaarland University DOI Pre-print Media Attached | ||
| 15:56 - 16:18 Talk | A Functional Proof Pearl: Inverting the Ackermann Hierarchy CPP Linh TranNational University of Singapore, Anshuman MohanNational University of Singapore, Aquinas HoborNational University of Singapore DOI Pre-print Media Attached | ||
| 16:18 - 16:40 Talk | Undecidability of Higher-Order Unification Formalised in Coq CPP DOI Pre-print Media Attached | ||
| 15:35 - 17:35 Tutorial | [T4] Proving Semantic Type Soundness in Iris TutorialFest Derek DreyerMPI-SWS, Robbert KrebbersDelft University of Technology, Amin Timanyimec-Distrinet KU-Leuven Link to publication File Attached | ||
15:35 - 17:35: Programming and Reasoning with Kleene Algebra with Tests (II)TutorialFest at SHANGRI-LA | |||
| 15:35 - 17:35 Tutorial | [T7] Programming and Reasoning with Kleene Algebra with Tests TutorialFest Nate FosterCornell University, Dexter KozenCornell University, Alexandra SilvaUniversity College London File Attached | ||
| 15:35 - 16:07 Talk | Cheap CTL Compassion in NuSMV VMCAI Daniel HausmannFriedrich-Alexander-Universität Erlangen-Nürnberg, Tadeusz LitakFAU Erlangen-Nuremberg, INF 8, Christoph RauchFAU Erlangen-Nürnberg, Lehrstuhl 8, Matthias ZinnerFAU Erlangen-Nürnberg | ||
| 16:07 - 16:40 Talk | A Cooperative Parallelization Approach for Property-Directed k-Induction VMCAI Martin BlichaUniversità della Svizzera italiana, Antti HyvärinenUniversità della Svizzera Italiana, Matteo MarescottiUniversità della Svizzera Italiana, Natasha SharyginaUSI Lugano, Switzerland | ||
| 16:40 - 17:12 Coffee break | Mini Break VMCAI | ||
| 17:12 - 17:45 Talk | 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 DoornUniversity of Pittsburgh | |||
| 16:50 - 17:12 Talk | Cubical Synthetic Homotopy Theory CPP Anders MörtbergDepartment of Mathematics, Stockholm University, Loïc PujetGallinette Project-Team, Inria DOI Pre-print Media Attached File Attached | ||
| 17:12 - 17:34 Talk | Three equivalent ordinal notation systems in Cubical Agda CPP Fredrik Nordvall ForsbergUniversity of Strathclyde, Chuangjie XuLudwig-Maximilians-Universität München, Neil GhaniUniversity of Strathclyde DOI Pre-print Media Attached File Attached | ||
| 17:34 - 17:56 Talk | PC Chairs' report CPP DOI Media Attached File Attached | ||
Tue 21 Jan Times are displayed in time zone: Saskatchewan, Central America change
Tue 21 Jan
Times are displayed in time zone: Saskatchewan, Central America change
08:30 - 10:00: Reasoning and Efficient ImplementationPADL at Bacchus Chair(s): Y. Annie LiuStony Brook University | |||
| 08:30 - 09:20 Talk | Invited Talk: Symbolic Reasoning About Machine Learning Systems PADL Adnan DarwicheUCLA | ||
| 09:20 - 09:45 Talk | Exploiting Database Systems and Treewidth for Counting PADL | ||
| 09:45 - 10:00 Short-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 BalzerCarnegie Mellon University, USA | |||
| 09:00 - 09:10 Day opening | Opening PLMW Brigitte PientkaMcGill University | ||
| 09:10 - 10:00 Talk | How to Write Papers So People Can Read ThemMentoring Event PLMW Derek DreyerMPI-SWS File Attached | ||
| 09:00 - 10:00 Talk | Invited talk: Proof Assistants at the Hardware-Software Interface CPP Adam ChlipalaMassachusetts Institute of Technology DOI Media Attached | ||
| 09:00 - 09:10 Day opening | Opening Plenary HASE | ||
| 09:10 - 10:10 Tutorial | Interactive Knowledge Shares HASE Peter O'HearnFacebook, Philippa GardnerImperial College London, Muralidaran VijayaraghavanSiFive, Peter SewellUniversity of Cambridge | ||
| 09:00 - 10:00 Talk | Invited talk: Nonstandard Interpretation in Pyro LAFI Pre-print | ||
| 09:00 - 09:30 Talk | How to Win First-Order Safety Games VMCAI Helmut SeidlTechnische Universität München, Christian MüllerTechnical University of Munich, Bernd FinkbeinerSaarland University | ||
| 09:30 - 10:00 Talk | Improving Parity Game Solvers with Justifications VMCAI Ruben LapauwKatholieke Universiteit Leuven, Maurice BruynoogheKatholieke Universiteit Leuven, Marc DeneckerKatholieke Universiteit Leuven | ||
10:30 - 12:00: Small Languages and ImplementationPADL at Bacchus Chair(s): James CheneyUniversity of Edinburgh, UK | |||
| 10:30 - 10:55 Talk | Explanations for Dynamic Programming PADL | ||
| 10:55 - 11:20 Talk | A DSL for Integer Range Reasoning: Partition, Interval and Mapping Diagrams PADL | ||
| 11:20 - 11:35 Short-paper | Variability-aware Datalog PADL | ||
| 11:35 - 12:00 Other | Panel: Reasoning for machine learning at large PADL Adnan DarwicheUCLA, Johannes K. FichteTU Dresden, Markus Hecher, Patrick Thier, Stefan Woltran, Farhad Shakerin, Gopal Gupta, Martin ErwigOregon State University, Prashant Kumar, Alan Fern, Johannes Eriksson, Masoumeh Parsa, Ramy Shahin, Marsha ChechikUniversity of Toronto | ||
| 10:30 - 12:30 Other | Ally Skills SessionMentoring Event Ally Skills Session | ||
10:30 - 12:30: Morning 2PLMW at Ile de France III (IDF III) Chair(s): Robbert KrebbersDelft University of Technology | |||
| 10:30 - 11:10 Talk | Making Progress Under Uncertainty in SMT Solving, Research, and LifeMentoring Event PLMW Lindsey KuperUniversity of California, Santa Cruz Media Attached | ||
| 11:10 - 11:50 Talk | Research as a collaborative effortMentoring Event PLMW Marco GaboardiBoston University Media Attached File Attached | ||
| 11:50 - 12:30 Talk | Theorem provers are a P.L. researcher's best friendMentoring Event PLMW Xavier LeroyCollège de France Media Attached File Attached | ||
10:30 - 11:35: Mechanized metatheoryCPP at Maurepas Chair(s): Benjamin C. PierceUniversity of Pennsylvania | |||
| 10:30 - 10:51 Talk | Coq à la Carte - A Practical Approach to Modular Syntax with Binders CPP DOI Pre-print Media Attached | ||
| 10:51 - 11:13 Talk | A Mechanized Formalization of GraphQL CPP Tomás DíazIMFD Chile, Federico OlmedoUniversity of Chile & IMFD Chile, Éric TanterUniversity of Chile DOI Pre-print Media Attached File Attached | ||
| 11:13 - 11:35 Talk | ConCert: A Smart Contract Certification Framework in Coq CPP Danil AnnenkovConcordium Blockchain Research Center, Aarhus University, Jakob Botsch NielsenConcordium Blockchain Research Center, Aarhus University, Bas SpittersConcordium Blockchain Research Center, Aarhus University DOI Pre-print Media Attached File Attached | ||
| 10:30 - 12:30 Meeting | Working Sessions I HASE | ||
| 10:30 - 11:00 Talk | A Differential-form Pullback Programming Language for Higher-order Reverse-mode Automatic Differentiation LAFI | ||
| 11:00 - 11:30 Talk | A Monad for Point Processes LAFI File Attached | ||
| 11:30 - 12:00 Talk | Denotational Semantics for Differentiable Programming with Manifolds LAFI Jesse SigalUniversity of Edinburgh | ||
| 12:00 - 12:30 Talk | Backpropagation in the Simply Typed Lambda-calculus with Linear Negation LAFI | ||
| 10:30 - 11:00 Talk | Language Inclusion for Finite Prime Event Structures VMCAI Andreas FellnerAIT - Austrian Institute of Technology, Thorsten TarrachAustrian Institute of Technology, Georg WeissenbacherTechnische Universität Wien | ||
| 11:00 - 11:30 Talk | Promptness and Bounded Fairness in Concurrent and Parameterized Systems VMCAI Swen JacobsCISPA Helmholtz Center for Information Security, Mouhammad SakrSaarland University, Martin ZimmermannUniversity of Liverpool | ||
| 11:30 - 12:00 Coffee break | Mini Break VMCAI | ||
| 12:00 - 12:30 Talk | Solving LIA* Using Approximations VMCAI Maxwell LevatichYale, Nikolaj BjørnerMicrosoft Research, Ruzica PiskacYale University, USA, Sharon ShohamTel Aviv university | ||
11:45 - 12:30: Verified cryptographyCPP at Maurepas Chair(s): Adam ChlipalaMassachusetts Institute of Technology | |||
| 11:45 - 12:07 Talk | Formalising Oblivious Transfer in the Semi-Honest and Malicious Model in CryptHOL CPP David ButlerAlan Turing Institute, David AspinallUniversity of Edinburgh, Adria GasconAlan Turing Institute DOI Pre-print Media Attached | ||
| 12:07 - 12:30 Talk | Verified Security of BLT Signature Scheme CPP Denis FirsovGuardtime AS, Ahto BuldasTallinn University of Technology, Ahto TruuGuardtime AS, Risto LaanojaGuardtime AS DOI Pre-print Media Attached File Attached | ||
| 12:30 - 14:00 Lunch | Lunch Catering | ||
13:30 - 15:00: Invited Experience and Direction SessionPADL at Bacchus Chair(s): David WarrenStony Brook University, Konstantinos (Kostis) SagonasUppsala University, Sweden | |||
| 13:30 - 14:00 Talk | Invited Talk: Relational Artificial Intelligence PADL Molham ArefRelational.ai | ||
| 14:00 - 14:30 Talk | Invited Talk: Learning Interpretable Rules from Structured Data PADL Mayur NaikUniversity of Pennsylvania | ||
| 14:30 - 15:00 Talk | Invited Talk: An Introduction to the Imandra Automated Reasoning System PADL Grant PassmoreImandra Inc. | ||
14:00 - 15:05: Afternoon 1PLMW at Ile de France III (IDF III) Chair(s): Justin HsuUniversity of Wisconsin-Madison, USA | |||
| 14:00 - 15:05 Talk | PanelMentoring Event PLMW William J. BowmanUniversity of British Columbia, Kenny FonerGalois, Andrew HirschMax Planck Institute for Software Systems, Taro SekiyamaNational Institute of Informatics, Juliana FrancoMicrosoft Research, Cambridge, Hannah GommerstadtVassar College Media Attached | ||
| 14:00 - 14:21 Talk | Formalizing Determinacy of Concurrent Revisions CPP Roy OverbeekVrije Universiteit Amsterdam DOI Pre-print Media Attached | ||
| 14:21 - 14:43 Talk | Formalizing π-calculus in Guarded Cubical Agda CPP DOI Pre-print Media Attached File Attached | ||
| 14:43 - 15:05 Talk | Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages CPP Arjen RouvoetDelft University of Technology, Casper Bach PoulsenDelft University of Technology, Robbert KrebbersDelft University of Technology, Eelco VisserDelft University of Technology DOI Pre-print Media Attached File Attached | ||
| 13:30 - 14:15 Tutorial | Peer Skillshare HASE Sarah de HaasGoogle Research | ||
| 14:00 - 14:30 Talk | Divide, Conquer, and Combine: a New Inference Strategy for Probabilistic Programs with Stochastic Support LAFI Yuan ZhouUniversity of Oxford, Hongseok YangKAIST, Yee Whye TehUniversity of Oxford, Tom RainforthDepartment of Statistics, University of Oxford | ||
| 14:32 - 14:47 Talk | MetaPPL: Inference Algorithms as First-Class Generative Models LAFI Alexander K. LewMassachusetts Institute of Technology, USA, Benjamin ShermanMassachusetts Institute of Technology, USA, Marco Cusumano-TownerMIT-CSAIL, Austin GarrettMIT, Ben ZinbergMIT, Vikash MansinghkaMIT, Michael CarbinMassachusetts Institute of Technology File Attached | ||
| 14:49 - 15:05 Talk | Monte Carlo Semantic Differencing of Probabilistic Programs LAFI | ||
| 14:00 - 14:32 Talk | Formalizing and Checking Multilevel Consistency VMCAI Ahmed BouajjaniIRIF, Université Paris Diderot, Constantin EneaIRIF, University Paris Diderot & CNRS, Madhavan MukundChennai Mathematical Institute, Gautham Shenoy RChennai Mathematical Institute, S.P. SureshChennai Mathematical Institute | ||
| 14:32 - 15:05 Talk | Practical Abstractions for Automated Verification of Shared-Memory Concurrency VMCAI Wytse OortwijnETH Zürich, Dilian GurovKTH Royal Institute of Technology, Marieke HuismanUniversity of Twente | ||
15:30 - 17:00: Invited Experience and Direction Session (Continued)PADL at Bacchus Chair(s): Y. Annie LiuStony Brook University, David WarrenStony Brook University, Konstantinos (Kostis) SagonasUppsala University, Sweden | |||
| 15:30 - 16:00 Talk | Invited Talk: We Are All Poor Schmucks: On the Value of Gradual Types PADL Philip WadlerUniversity of Edinburgh, UK | ||
| 16:00 - 16:45 Other | Panel: Experience and Direction PADL I: Molham ArefRelational.ai, I: Mayur NaikUniversity of Pennsylvania, I: Grant PassmoreImandra Inc., I: Philip WadlerUniversity of Edinburgh, UK | ||
| 16:45 - 17:00 Day closing | Closing PADL | ||
15:35 - 17:45: POPLmark 15 Year Retrospective PanelPOPLmark 15 Year Retrospective Panel at Frontenac | |||
| 15:35 - 17:35 Other | POPLmark 15 Year Retrospective Panel POPLmark 15 Year Retrospective Panel | ||
15:35 - 17:45: Afternoon 2PLMW at Ile de France III (IDF III) Chair(s): Nobuko YoshidaImperial College London | |||
| 15:40 - 16:40 Talk | How Can I Academia When My Brain Can't Even? Mental Health in Grad School and BeyondMentoring Event PLMW Kenny FonerGalois Media Attached | ||
| 16:40 - 16:50 Coffee break | Mini break PLMW | ||
| 16:50 - 17:35 Talk | Automated Program Verification using Abductive ReasoningMentoring Event PLMW Isil DilligUniversity of Texas Austin Media Attached | ||
15:35 - 16:40: Formalized mathematics 1CPP at Maurepas Chair(s): Robert Y. LewisVrije Universiteit Amsterdam | |||
| 15:35 - 15:56 Talk | Formalising perfectoid spaces CPP Patrick MassotUniversité Paris Sud, Kevin BuzzardImperial College London, Johan CommelinUniversität Freiburg DOI Pre-print Media Attached File Attached | ||
| 15:56 - 16:18 Talk | A Constructive Formalization of the Weak Perfect Graph Theorem CPP Abhishek Kr SinghTata Institute of Fundamental Research Mumbai, Raja NatarajanTata Institute of Fundamental Research Mumbai DOI Pre-print Media Attached File Attached | ||
| 16:18 - 16:40 Talk | Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq CPP DOI Pre-print Media Attached | ||
| 14:30 - 16:30 Meeting | Working Sessions II HASE | ||
| 16:30 - 17:45 Day closing | Closing Plenary HASE | ||
| 15:35 - 16:05 Talk | Coinductive Trees for Exact Inference of Probabilistic Programs LAFI Alexander BagnallOhio University, Gordon StewartOhio University, Anindya BanerjeeIMDEA Software Institute | ||
| 16:05 - 16:35 Talk | Name generation and Higher-order Probabilistic Programming (Or is new=rnd?) LAFI File Attached | ||
| 16:35 - 17:05 Talk | Density Functions of Statistical Probabilistic Programs LAFI | ||
| 17:05 - 17:35 Talk | Probabilistic Programming around Gaussian Processes LAFI David TolpinPUB+ | ||
| 17:35 - 17:45 Day closing | Closing LAFI | ||
| 15:35 - 17:45 Other | Panel "The Future of Software Verification" at VMCAI VMCAI Lenore ZuckUIC, Michael WhalenAmazon Web Services and the University of Minnesota, Natarajan ShankarSRI International, USA, Andreas PodelskiUniversity of Freiburg, Germany, Dirk BeyerLMU Munich | ||
16:50 - 17:56: Formalized mathematics 2CPP at Maurepas Chair(s): Tobias NipkowTechnische Universität München | |||
| 16:50 - 17:12 Talk | The Poincaré-Bendixson Theorem in Isabelle/HOL CPP DOI Pre-print Media Attached | ||
| 17:12 - 17:34 Talk | A Formal Proof of the Independence of the Continuum Hypothesis CPP DOI Pre-print Media Attached | ||
| 17:34 - 17:56 Talk | The Lean mathematical library CPP DOI Pre-print Media Attached File Attached | ||
Wed 22 Jan Times are displayed in time zone: Saskatchewan, Central America change
Wed 22 Jan
Times are displayed in time zone: Saskatchewan, Central America change
| 07:45 - 08:45 Social Event | Mentoring BreakfastMentoring Event Mentoring Breakfasts | ||
08:45 - 09:00: Welcome + SIGPLAN Award CeremonyResearch Papers at Ile de France II (IDF II) Chair(s): Brigitte PientkaMcGill University, Jens PalsbergUniversity of California, Los Angeles, Lars BirkedalAarhus University | |||
| 08:45 - 09:00 Day 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 PientkaMcGill University | |||
| 09:00 - 10:00 Talk | Can Programming Languages Research impact Deep Learning 2.0?Invited Talk Research Papers Martin VechevETH Zürich Media Attached | ||
10:30 - 11:35: Probabilistic ProgrammingResearch Papers at Ile de France II (IDF II) Chair(s): Alexandra SilvaUniversity College London | |||
| 10:30 - 10:51 Talk | Towards Verified Stochastic Variational Inference for Probabilistic Programs Research Papers Link to publication DOI Media Attached | ||
| 10:51 - 11:13 Talk | Trace Types and Denotational Semantics for Sound Programmable Inference in Probabilistic Languages Research Papers Alexander K. LewMassachusetts Institute of Technology, USA, Marco Cusumano-TownerMIT-CSAIL, Benjamin ShermanMassachusetts Institute of Technology, USA, Michael CarbinMassachusetts Institute of Technology, Vikash MansinghkaMIT Link to publication DOI Media Attached | ||
| 11:13 - 11:35 Talk | 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 SamantaPurdue University | |||
| 10:30 - 10:51 Talk | The Weak Call-By-Value λ-Calculus is Reasonable for Both Time and Space Research Papers Yannick ForsterSaarland University, Fabian KunzeSaarland University, Marc RothSaarland University and MMCI and Merton College, Oxford University Link to publication DOI Pre-print Media Attached | ||
| 10:51 - 11:13 Talk | Complexity and Information in Invariant Inference Research Papers Yotam M. Y. FeldmanTel Aviv University, Neil ImmermanUniversity of Massachusetts, Amherst, Mooly SagivTel Aviv University, Sharon ShohamTel Aviv university Link to publication DOI Media Attached | ||
| 11:13 - 11:35 Talk | Parameterized Verification under TSO is PSPACE-Complete Research Papers Parosh Aziz AbdullaUppsala University, Sweden, Mohamed Faouzi AtigUppsala University, Sweden, Rojin RezvanSharif 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 WiesNew York University | |||
| 11:45 - 12:07 Talk | Recurrence Extraction for Functional Programs through Call-by-Push-Value Research Papers Alex KavvosAarhus University, Edward MorehouseWesleyan University, Dan LicataWesleyan University, Norman DannerWesleyan University Link to publication DOI File Attached | ||
| 12:07 - 12:30 Talk | Liquidate Your Assets: Reasoning About Resource Usage in Liquid Haskell Research Papers Martin Adam Thomas HandleyUniversity of Nottingham, Niki VazouIMDEA Software Institute, Graham HuttonUniversity 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 LesaniUniversity of California, Riverside | |||
| 11:45 - 12:07 Talk | Program Synthesis by Type-Guided Abstraction Refinement Research Papers Zheng GuoUniversity of California, San Diego, Michael B. JamesUniversity of California, San Diego, David JustoUniversity of California, San Diego, Jiaxiao ZhouUniversity of California, San Diego, Ziteng WangUniversity of California, San Diego, Ranjit JhalaUniversity of California, San Diego, Nadia PolikarpovaUniversity of California, San Diego Link to publication DOI Media Attached File Attached | ||
| 12:07 - 12:30 Talk | Synthesizing Replacement Classes Research Papers Link to publication DOI Media Attached File Attached | ||
| 12:30 - 14:00 Lunch | LGBTQ LunchMentoring Event LGBTQ Lunch | ||
| 12:30 - 14:00 Lunch | Lunch Catering | ||
14:00 - 15:05: Program LogicsResearch Papers at Ile de France II (IDF II) Chair(s): Azalea RaadMPI-SWS, Germany | |||
| 14:00 - 14:21 Talk | The Future is Ours: Prophecy Variables in Separation Logic Research Papers Ralf JungMPI-SWS, Rodolphe LepigreMPI-SWS, Gaurav ParthasarathyETH Zurich, Marianna RapoportUniversity of Waterloo, Amin Timanyimec-Distrinet KU-Leuven, Derek DreyerMPI-SWS, Bart Jacobsimec-DistriNet, Dept. CS, KU Leuven Link to publication DOI Media Attached | ||
| 14:21 - 14:43 Talk | Spy Game: Verifying a Local Generic Solver in Iris Research Papers Paulo Emílio de VilhenaInria, François PottierInria, France, Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud Link to publication DOI Media Attached File Attached | ||
| 14:43 - 15:05 Talk | Actris: Session-Type Based Reasoning in Separation Logic Research Papers Jonas Kastberg HinrichsenIT University of Copenhagen, Jesper BengtsonIT University of Copenhagen, Robbert KrebbersDelft 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. SiekIndiana University, USA | |||
| 14:00 - 14:21 Talk | What is Decidable about Gradual Types? Research Papers Zeina MigeedUniversity of California, Los Angeles, Jens PalsbergUniversity of California, Los Angeles Link to publication DOI Media Attached File Attached | ||
| 14:21 - 14:43 Talk | Graduality and Parametricity: Together Again for the First Time Research Papers Max NewNortheastern University, Dustin JamnerNortheastern University, USA, Amal AhmedNortheastern University, USA Link to publication DOI Media Attached | ||
| 14:43 - 15:05 Talk | Does Blame Shifting Work? Research Papers Lukas LazarekNorthwestern University, Alexis KingNorthwestern University, Samanvitha SundarNorthwestern University, Robby FindlerNorthwestern University, USA, Christos DimoulasPLT @ 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 BirkedalAarhus University | |||
| 15:35 - 15:56 Talk | A Simple Differentiable Programming Language Research Papers Link to publication DOI Media Attached | ||
| 15:56 - 16:18 Talk | Backpropagation in the Simply Typed Lambda-calculus with Linear Negation Research Papers Link to publication DOI Media Attached File Attached | ||
| 16:18 - 16:40 Talk | Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear TimeDistinguished Paper Research Papers Steffen SmolkaCornell University, Nate FosterCornell University, Justin HsuUniversity of Wisconsin-Madison, USA, Tobias KappéUniversity College London, Dexter KozenCornell University, Alexandra SilvaUniversity 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 SarkarUniversity of St. Andrews | |||
| 15:35 - 15:56 Talk | Persistency Semantics of the Intel-x86 Architecture Research Papers Azalea RaadMPI-SWS, Germany, John WickersonImperial College London, Gil NeigerIntel Corporation, Viktor VafeiadisMPI-SWS, Germany Link to publication DOI Media Attached | ||
| 15:56 - 16:18 Talk | Reductions for Safety Proofs Research Papers Link to publication DOI Media Attached | ||
| 16:18 - 16:40 Talk | RustBelt Meets Relaxed Memory Research Papers Hoang-Hai DangMPI-SWS, Jacques-Henri JourdanCNRS, LRI, Université Paris-Sud, Jan-Oliver KaiserMPI-SWS, Derek DreyerMPI-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 SamantaPurdue University | |||
| 16:50 - 17:12 Talk | Visualization by Example Research Papers Chenglong WangUniversity of Washington, USA, Yu FengUniversity of California, Santa Barbara, Rastislav BodikUniversity of Washington, Alvin CheungUniversity of California, Berkeley, Isil DilligUniversity of Texas Austin Link to publication DOI Media Attached | ||
| 17:12 - 17:35 Talk | Deciding Memory Safety for Single-Pass Heap-Manipulating Programs Research Papers Umang MathurUniversity of Illinois at Urbana-Champaign, Adithya MuraliUniversity of Illinois at Urbana-Champaign, Paul KrogmeierUniversity of Illinois at Urbana-Champaign, P. MadhusudanUniversity of Illinois at Urbana-Champaign, Mahesh ViswanathanUniversity of Illinois at Urbana-Champaign Link to publication DOI Pre-print Media Attached File Attached | ||
| 16:50 - 19:00 Poster | SRC Poster Session Student Research Competition | ||
| 17:35 - 18:35 Social Event | Social Hour (Supported by Facebook) Research Papers | ||
Thu 23 Jan Times are displayed in time zone: Saskatchewan, Central America change
Thu 23 Jan
Times are displayed in time zone: Saskatchewan, Central America change
| 07:45 - 09:00 Social Event | Mentoring BreakfastMentoring Event Mentoring Breakfasts | ||
09:00 - 10:00: Invited TalkResearch Papers at Ile de France II (IDF II) Chair(s): Brigitte PientkaMcGill University | |||
| 09:00 - 10:00 Talk | What is a Secure Programming Language? Invited Talk Research Papers Cristina CifuentesOracle Labs Link to publication Media Attached | ||
10:30 - 11:35: Types and EffectsResearch Papers at Ile de France II (IDF II) Chair(s): Dominique DevrieseVrije Universiteit Brussel | |||
| 10:30 - 10:51 Talk | Binders by Day, Labels by Night: Effect Instances via Lexically Scoped Handlers Research Papers Dariusz BiernackiUniversity of Wrocław, Maciej PirógUniversity of Wrocław, Piotr PolesiukUniversity of Wrocław, Filip SieczkowskiUniversity of Wrocław Link to publication DOI Media Attached | ||
| 10:51 - 11:13 Talk | The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects Research Papers Link to publication DOI Media Attached | ||
| 11:13 - 11:35 Talk | SyTeCi: Automating Contextual Equivalence for Higher-Order Programs with References Research Papers Guilhem JaberLS2N, 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 ThiemannUniversity of Freiburg, Germany | |||
| 11:45 - 12:07 Talk | Fast, Sound, and Effectively Complete Dynamic Race Prediction Research Papers Andreas PavlogiannisAarhus University Link to publication DOI Media Attached File Attached | ||
| 12:07 - 12:30 Talk | Detecting Floating-Point Errors via Atomic Conditions Research Papers Daming ZouPeking University, Muhan ZengPeking University, Yingfei XiongPeking University, Zhoulai FuIT University of Copenhagen, Denmark, Lu ZhangPeking University, Zhendong SuETH 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 PientkaMcGill University | |||
| 11:45 - 12:07 Talk | Seminaïve Evaluation for a Higher-Order Functional LanguageDistinguished Paper Research Papers Neel KrishnaswamiComputer Laboratory, University of Cambridge, Michael ArntzeniusUniversity of Birmingham, UK Link to publication DOI Media Attached File Attached | ||
| 12:07 - 12:30 Talk | Decomposition Diversity with Symmetric Data and Codata Research Papers David BinderUniversity of Tübingen, Julian JabsUniversity of Tübingen, Ingo SkupinUniversity of Tübingen, Klaus OstermannUniversity of Tübingen, Germany Link to publication DOI Media Attached | ||
| 12:30 - 14:00 Lunch | Lunch Catering | ||
14:00 - 15:05: Type SystemsResearch Papers at Ile de France II (IDF II) Chair(s): Peter ThiemannUniversity of Freiburg, Germany | |||
| 14:00 - 14:21 Talk | Undecidability of D<: and Its Decidable FragmentsDistinguished Paper Research Papers Link to publication DOI Media Attached File Attached | ||
| 14:21 - 14:43 Talk | Decidable Subtyping for Path Dependent Types Research Papers Julian MackayVictoria University of Wellington, Alex PotaninVictoria University of Wellington, Jonathan AldrichCarnegie Mellon University, Lindsay GrovesVictoria University of Wellington Link to publication DOI Media Attached | ||
| 14:43 - 15:05 Talk | Dependent Type Systems as Macros Research Papers Stephen ChangNortheastern University, Michael BallantynePLT @ Northeastern University, Milo TurnerPLT @ Northeastern University, William J. BowmanUniversity of British Columbia Link to publication DOI Media Attached File Attached | ||
| 14:00 - 15:30 Talk | SRC Finalists Presentations Student Research Competition | ||
15:35 - 16:40: Program LogicsResearch Papers at Ile de France II (IDF II) Chair(s): Chung-Kil HurSeoul National University | |||
| 15:35 - 15:56 Talk | Deductive Verification with Ghost Monitors Research Papers Martin ClochardETH Zürich, Claude MarchéInria Saclay & Université Paris-Saclay, Andrei PaskevichLRI, Université Paris-Sud & CNRS Link to publication DOI Media Attached | ||
| 15:56 - 16:18 Talk | The Next 700 Relational Program Logics Research Papers Kenji MaillardInria Nantes & University of Chile, Cătălin HriţcuInria Paris, Exequiel RivasInria Paris, Antoine Van MuylderInria Paris and Paris 7 Link to publication DOI Media Attached File Attached | ||
| 16:18 - 16:40 Talk | Incorrectness Logic Research Papers Peter O'HearnFacebook Link to publication DOI Media Attached | ||
15:35 - 16:40: Probabilistic ProgrammingResearch Papers at Ile de France III (IDF III) Chair(s): Ohad KammarUniversity of Edinburgh | |||
| 15:35 - 15:56 Talk | A Language for Probabilistically Oblivious Computation Research Papers David DaraisUniversity of Vermont, Ian SweetUniversity of Maryland, Chang LiuCitadel Securities, Michael HicksUniversity of Maryland Link to publication DOI Media Attached File Attached | ||
| 15:56 - 16:18 Talk | PλωNK: Functional Probabilistic NetKAT Research Papers Link to publication DOI Media Attached File Attached | ||
| 16:18 - 16:40 Talk | Optimal Approximate Sampling From Discrete Probability Distributions Research Papers Feras SaadMassachusetts Institute of Technology, Cameron FreerMassachusetts Institute of Technology, Martin RinardMIT, Vikash MansinghkaMIT Link to publication DOI Media Attached File Attached | ||
| 16:50 - 18:00 Meeting | Business Meeting & SRC Awards Research Papers Media Attached | ||
| 18:00 - 19:00 Social Event | Social Hour (Supported by Microsoft) Research Papers | ||
| 19:00 - 21:00 Dinner | W@POPL DinnerMentoring Event W@POPL Dinner | ||
Fri 24 Jan Times are displayed in time zone: Saskatchewan, Central America change
Fri 24 Jan
Times are displayed in time zone: Saskatchewan, Central America change
| 07:45 - 09:00 Social Event | Mentoring BreakfastMentoring Event Mentoring Breakfasts | ||
09:00 - 10:00: Invited TalkResearch Papers at Ile de France II (IDF II) Chair(s): Lars BirkedalAarhus University | |||
| 09:00 - 10:00 Talk | Probabilistic ProgrammingInvited Talk Research Papers Hongseok YangKAIST Media Attached File Attached | ||
10:30 - 11:35: Type SystemsResearch Papers at Ile de France II (IDF II) Chair(s): Dominique DevrieseVrije Universiteit Brussel | |||
| 10:30 - 10:51 Talk | Kind Inference for DatatypesDistinguished Paper Research Papers Ningning XieThe University of Hong Kong, Richard A. EisenbergBryn Mawr College, USA, Bruno C. d. S. OliveiraThe University of Hong Kong, Hong Kong Link to publication DOI Media Attached | ||
| 10:51 - 11:13 Talk | Partial Type Constructors: Or, Making Ad Hoc Datatypes Less Ad Hoc Research Papers Mark JonesPortland State University, J. Garrett MorrisUniversity of Kansas, USA, Richard A. EisenbergBryn Mawr College, USA Link to publication DOI Media Attached File Attached | ||
| 11:13 - 11:35 Talk | 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 SarkarUniversity of St. Andrews | |||
| 11:45 - 12:07 Talk | Label-Dependent Session Types Research Papers Link to publication DOI Media Attached | ||
| 12:07 - 12:30 Talk | 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 AmorimCarnegie Mellon University, USA | |||
| 11:45 - 12:07 Talk | Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time Research Papers Peixin WangShanghai Jiao Tong University, Hongfei FuShanghai Jiao Tong University, Krishnendu ChatterjeeIST Austria, Yuxin DengEast China Normal University, Ming XuEast China Normal University Link to publication DOI Media Attached | ||
| 12:07 - 12:30 Talk | Aiming Low Is Harder: Induction for Lower Bounds in Probabilistic Program Verification Research Papers Marcel HarkRWTH Aachen University, Germany, Benjamin Lucien KaminskiRWTH Aachen University, Germany, Jürgen GieslRWTH Aachen University, Joost-Pieter KatoenRWTH Aachen University Link to publication DOI Media Attached File Attached | ||
| 12:30 - 14:00 Lunch | Lunch Catering | ||
14:00 - 15:05: Semantics of Probabilistic & Quantum ProgrammingResearch Papers at Ile de France II (IDF II) Chair(s): Alexandra SilvaUniversity College London | |||
| 14:00 - 14:21 Talk | Full Abstraction for the Quantum Lambda-Calculus Research Papers Link to publication DOI Media Attached File Attached | ||
| 14:21 - 14:43 Talk | Relational Proofs for Quantum Programs Research Papers Gilles BartheMPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Justin HsuUniversity of Wisconsin-Madison, USA, Mingsheng YingUniversity of Technology Sydney, Australia / Institute of Software at Chinese Academy of Sciences, China/ Department of Computer Science and Technology, Tsinghua University., Nengkun YuUniversity of Technology Sydney, Australia, Li ZhouMax Planck Institute for Security and Privacy/Tsinghua University Link to publication DOI Pre-print Media Attached File Attached | ||
| 14:43 - 15:05 Talk | A Probabilistic Separation Logic Research Papers Gilles BartheMPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Justin HsuUniversity of Wisconsin-Madison, USA, Kevin LiaoMax 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 Timanyimec-Distrinet KU-Leuven | |||
| 14:00 - 14:21 Talk | Stacked Borrows: An Aliasing Model for Rust Research Papers Link to publication DOI Media Attached File Attached | ||
| 14:21 - 14:43 Talk | Executable Formal Semantics for the POSIX Shell Research Papers Link to publication DOI Media Attached File Attached | ||
| 14:43 - 15:05 Talk | Disentanglement in Nested-Parallel Programs Research Papers Sam WestrickCarnegie Mellon University, Rohan YadavCarnegie Mellon University, Matthew FluetRochester Institute of Technology, Umut A. AcarCarnegie 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 AmorimCarnegie Mellon University, USA | |||
| 15:35 - 15:56 Talk | Taylor Subsumes Scott, Berry, Kahn and PlotkinDistinguished Paper Research Papers Link to publication DOI Media Attached File Attached | ||
| 15:56 - 16:18 Talk | Reduction Monads and Their Signatures Research Papers Benedikt AhrensUniversity of Birmingham, United Kingdom, André HirschowitzUniversité Côte d'Azur, Ambroise LafontInria, France, Marco MaggesiUniversità di Firenze Link to publication DOI Media Attached | ||
| 16:18 - 16:40 Talk | Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq Research Papers Matthieu SozeauInria, Simon BoulierInria, Yannick ForsterSaarland University, Nicolas TabareauInria, Théo WinterhalterInria — LS2N Link to publication DOI Media Attached File Attached | ||
| 16:40 - 17:40 Social Event | Social Hour (Supported by Tezos) Research Papers | ||
Sat 25 Jan Times are displayed in time zone: Saskatchewan, Central America change
Sat 25 Jan
Times are displayed in time zone: Saskatchewan, Central America change
09:00 - 10:00: Invited TalkCoqPL at Maurepas Chair(s): Robbert KrebbersDelft University of Technology | |||
| 09:00 - 10:00 Talk | SMTCoq: Safe and efficient automation in Coq (Keynote) CoqPL Chantal KellerLRI, Université Paris-Sud File Attached | ||
| 09:00 - 09:30 Talk | Gradual Typing as if Types Mattered WGT Pre-print | ||
| 09:30 - 10:00 Talk | Fully Abstract from Static to Gradual WGT Koen JacobsKU Leuven, Amin Timanyimec-Distrinet KU-Leuven, Dominique DevrieseVrije Universiteit Brussel Pre-print | ||
| 09:00 - 09:05 Day opening | PriSC Introduction PriSC Dominique DevrieseVrije Universiteit Brussel File Attached | ||
| 09:05 - 10:00 Industry talk | Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing PriSC Media Attached | ||
| 10:30 - 11:00 Talk | Deriving Instances with Dependent Types CoqPL Arthur Azevedo de AmorimCarnegie Mellon University, USA File Attached | ||
| 11:00 - 11:30 Talk | The use of Coq for Common Criteria Evaluations CoqPL File Attached | ||
| 11:30 - 12:00 Talk | Verifying concurrent Go code in Coq with Goose CoqPL Tej ChajedMassachusetts Institute of Technology, USA, Joseph TassarottiBoston College, M. Frans KaashoekMassachusetts Institute of Technology, USA, Nickolai ZeldovichMassachusetts Institute of Technology, USA Link to publication File Attached | ||
| 12:00 - 12:30 Talk | A Tutorial on Equations CoqPL Matthieu SozeauInria Media Attached File Attached | ||
10:30 - 12:30: Programming featuresWGT at Orleans Chair(s): Giuseppe CastagnaCNRS - Université de Paris, France | |||
| 10:30 - 11:00 Talk | Gradual Algebraic Data Types WGT Michael GreenbergPomona College, Stefan MalewskiUniversity of Santiago de Chile, Éric TanterUniversity of Chile Pre-print File Attached | ||
| 11:00 - 11:30 Talk | Gradual Typing for Extensibility by Rows WGT Pre-print | ||
| 11:30 - 12:00 Talk | Foreign Function Typing: Semantic Type Soundness for FFIs WGT Pre-print | ||
| 12:00 - 12:30 Talk | Space-Efficient Monotonic References WGT Pre-print | ||
| 12:30 - 14:00 Lunch | Lunch Catering | ||
| 14:00 - 15:00 Talk | Autosubst 2: Mechanising binders in Coq (Keynote) CoqPL Kathrin StarkPrinceton University, USA File Attached | ||
| 14:00 - 14:32 Talk | Hypercoercions and a Framework for Equivalence of Cast Calculi WGT Kuang-Chen LuIndiana University Bloomington, Jeremy G. SiekIndiana University, USA, Andre KuhlenschmidtIndiana University Pre-print | ||
| 14:32 - 15:05 Talk | Space-Efficient Gradual Typing in Coercion-Passing Style WGT Pre-print | ||
14:00 - 15:05: New outlooks on secure compilationPriSC at Rosalie Chair(s): Cristina CifuentesOracle Labs | |||
| 14:00 - 14:24 Talk | Exploits as Insecure Compilation PriSC Jennifer PaykinGalois, Inc., Eric MertensGalois, Inc., Mark TullsenGalois, Inc, Luke MaurerGalois, Inc, Benoit RazetGalois, Inc, Alexander BakstGalois, Inc, Scott MooreGalois, Inc Pre-print Media Attached File Attached | ||
| 14:24 - 14:48 Talk | Universal Composability is Secure Compilation PriSC Marco PatrignaniStanford University & CISPA , Riad S. WahbyStanford University, USA, Robert KünnemannCISPA, Saarland University Media Attached File Attached | ||
| 14:48 - 14:56 Talk | Short Talk: Automatically Eliminating Speculative Leaks With Blade PriSC Marco VassenaCISPA Helmholtz Center for Information Security, Klaus v. GleissenthallUniversity of California at San Diego, USA, Rami Gökhan KıcıUniversity of California at San Diego, USA Media Attached File Attached | ||
| 14:56 - 15:04 Talk | Short Talk: Everparse PriSC Tahina RamananandroMicrosoft Research, n.n. Media Attached | ||
15:35 - 17:45: Contributed Talks & Coq DevelopersCoqPL at Maurepas Chair(s): Joseph TassarottiBoston College, Robbert KrebbersDelft University of Technology | |||
| 15:35 - 16:05 Talk | Towards Formally Verified Just-in-Time compilation CoqPL Aurèle BarrièreUniv Rennes, IRISA, Sandrine BlazyUniv Rennes- IRISA, David PichardieUniv Rennes, ENS Rennes, IRISA File Attached | ||
| 16:05 - 16:35 Talk | A Coq Library of Undecidable Problems CoqPL Yannick ForsterSaarland University, Dominique Larchey-WendlingCNRS, LORIA, Andrej DudenhefnerSaarland University, Edith HeiterSaarland University, Dominik KirstSaarland University, Fabian KunzeSaarland University, Gert SmolkaSaarland University, Simon SpiesSaarland University, Dominik WehrSaarland University, Universiteit van Amsterdam, Maximilian WuttkeSaarland University Media Attached File Attached | ||
| 16:35 - 16:50 Break | Short break CoqPL | ||
| 16:50 - 17:35 Demonstration | Session with the Coq Development Team CoqPL | ||
15:35 - 17:45: Analysis, verification, blameWGT at Orleans Chair(s): Niki VazouIMDEA Software Institute | |||
| 15:35 - 16:07 Talk | Gradual Verification of Recursive Heap Data Structures WGT Jenna WiseCarnegie Mellon University, Johannes BaderFacebook, Jonathan AldrichCarnegie Mellon University, Éric TanterUniversity of Chile, Joshua SunshineCarnegie Mellon University Pre-print | ||
| 16:07 - 16:40 Talk | Gradual Program Analysis WGT Samuel EstepLiberty University, Jenna WiseCarnegie Mellon University, Jonathan AldrichCarnegie Mellon University, Éric TanterUniversity of Chile, Johannes BaderFacebook, Joshua SunshineCarnegie Mellon University Pre-print | ||
| 16:40 - 16:50 Break | Minibreak WGT | ||
| 16:50 - 17:20 Talk | Blame tracking at higher fidelity WGT Jakub ZalewskiUniversity of Edinburgh, James McKinnaUniversity of Edinburgh, J. Garrett MorrisUniversity of Kansas, USA, Philip WadlerUniversity of Edinburgh, UK Pre-print | ||
| 17:20 - 17:45 Day closing | Discussion on gradual typing and WGT21 WGT | ||
15:35 - 17:45: Compartmentalization, memory safety, and isolationPriSC at Rosalie Chair(s): Marco PatrignaniStanford University & CISPA , Jonathan ProtzenkoMicrosoft Research, Redmond | |||
| 15:35 - 15:59 Talk | Flexible Tag-based Policies for Compartmentalized C PriSC Sean AndersonPortland State University, Andrew TolmachPortland State University, CHR ChhakPortland State University Media Attached File Attached | ||
| 15:59 - 16:23 Talk | Mechanized Reasoning about a Capability Machine PriSC Media Attached | ||
| 16:23 - 16:47 Talk | Securing Interruptible Enclaves PriSC Matteo BusiUniversità di Pisa - Dipartimento di Informatica, Job Noormanimec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium, Jo Van Bulckimec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium, Letterio GallettaIMT School for Advanced Studies, Pierpaolo DeganoUniversità di Pisa - Dipartimento di Informatica, Jan Tobias Mühlbergimec-DistriNet, Dept. of Computer Science, KU Leuven, Belgium, Frank PiessensKU Leuven Media Attached File Attached | ||
| 16:47 - 16:57 Break | Mini-break PriSC | ||
| 16:57 - 17:21 Talk | WebAssembly as an Intermediate Language for Provably-Safe Software Sandboxing PriSC Jay BosamiyaCarnegie Mellon University, Benjamin LimCarnegie Mellon University, Bryan ParnoCarnegie Mellon University Media Attached File Attached | ||
| 17:21 - 17:45 Talk | Memory Safety Preservation for WebAssembly PriSC Marco VassenaCISPA Helmholtz Center for Information Security, Marco PatrignaniStanford University & CISPA Link to publication Media Attached File Attached | ||
Sun 19 Jan Times are displayed in time zone: Saskatchewan, Central America change
Sun 19 Jan
Times are displayed in time zone: Saskatchewan, Central America change
| Room | 9:00 | 30 | 10:00 | 30 | 11:00 | 30 | 12:00 | 30 | 13:00 | 30 | 14:00 | 30 | 15:00 | 30 | 16:00 | 30 | 17:00 | 30 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|