Program - POPL 2020

Time Zone

The program is currently displayed in (GMT-06:00) Saskatchewan, Central America.

Use conference time zone: (GMT-06:00) Saskatchewan, Central AmericaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

You're viewing the program in a time zone which is different from your device's time zone - change time zone

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 30m Talk		Invited Talk: Quantum Computing for Programming Languages Researchers PLanQC I: Jennifer PaykinGalois, Inc. Media Attached File Attached
09:30 30m Talk		Invited Talk: Dependently Typed Quantum Programming in Proto-Quipper PLanQC I: Peter SelingerDalhousie University Media Attached

09:00 - 10:00	Invited 1VMCAI at St Jerome Chair(s): Dirk BeyerLMU Munich

09:00 60m Talk		The Siren Song of Temporal Synthesis VMCAI Moshe VardiRice University

10:00 - 10:30	Sunday Morning BreakCatering at Break

10:00 30m Coffee break		Break Catering

10:30 - 12:30	Invited Talks, Pulses, Errors and CategoriesPLanQC at Maurepas Chair(s): Frank Fu

10:30 30m Talk		Invited Talk: Q# - Going Beyond Quantum Circuits PLanQC I: Bettina HeimMicrosoft Media Attached
11:00 30m Talk		Invited Talk: Resource-Efficient Quantum Computing by Breaking Abstractions PLanQC I: Fred ChongUniversity of Chicago Media Attached File Attached
11:30 20m 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 20m 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 20m Talk		Quantum CPOs PLanQC Andre KornellTulane University, Bert LindenhoviusTulane University, Michael MisloveTulane

10:30 - 12:30	Papers 1VMCAI at St Jerome Chair(s): Natasha SharyginaUSI Lugano, Switzerland

10:30 30m Talk		Witnessing Secure Compilation VMCAI Kedar NamjoshiBell Labs, Nokia, Lucas M. TabajaraRice University
11:00 30m 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 30m Coffee break		Mini Break VMCAI
12:00 30m 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	Sunday LunchCatering at Lunch Room

12:30 90m Lunch		Lunch Catering

14:00 - 15:05	Formal MethodsPLanQC at Maurepas Chair(s): Dominique UnruhUniversity of Tartu

14:00 20m Talk		Runtime Analysis of Quantum Programs: A Formal Approach PLanQC Federico OlmedoUniversity of Chile & IMFD Chile, Alejandro Díaz-CaroICC (UBA-CONICET) & UNQ Pre-print File Attached
14:20 20m Talk		Qbricks: formal verification in quantum computing PLanQC Christopĥe CharetonCEA, LIST, France, Sébastien BardinCEA LIST, François BobotCEA, Valentin PerrelleCEA, LIST, France, Benoit ValironLRI, CentraleSupelec, Univ. Paris Saclay File Attached
14:40 25m 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	Invited 2VMCAI at St Jerome Chair(s): Damien ZuffereyMPI-SWS

14:00 65m Talk		Safety and Robustness for Deep Learning with Provable Guarantees VMCAI Marta KwiatkowskaUniversity of Oxford

	15:05 - 15:35	Sunday Afternoon BreakCatering at Break

15:35 - 16:35	NISQPLanQC at Maurepas Chair(s): Will ZengUnitary Fund

15:35 20m 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 20m 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 20m 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 - 17:45	Papers 2VMCAI at St Jerome Chair(s): Kedar NamjoshiBell Labs, Nokia

15:35 32m Talk		The Correctness of a Code Generator for a Functional Language VMCAI Nathanaël CourantINRIA, Antoine SereEcole Polytechnique, Natarajan ShankarSRI International, USA
16:07 32m 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 32m Coffee break		Mini Break VMCAI
17:12 32m 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 20m 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 20m Talk		Formalization of a Programming Language for Quantum Circuits with Measurement and Classical Control PLanQC Dongho LEELRI / CEA LIST, Univ Paris Saclay, Sébastien BardinCEA LIST, Valentin PerrelleCEA, LIST, France, Benoit ValironLRI, CentraleSupelec, Univ. Paris Saclay File Attached
17:30 20m Talk		Automated distribution of quantum circuits via hypergraph partitioning PLanQC Pablo Andres-MartinezUniversity of Edinburgh, Chris HeunenUniversity of Edinburgh Link to publication DOI Pre-print Media Attached File Attached

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 15m Day opening		Opening PADL Gopal Gupta
08:45 50m Talk		Invited Talk: Logical Engines for Cloud Configurations PADL I: Nikolaj BjørnerMicrosoft Research
09:35 25m Talk		Interactive Text Graph Mining with a Prolog-based Dialog Engine PADL Paul TarauUniversity of North Texas, Eduardo Blanco

09:00 - 10:00	Verifying Probabilistic Properties with Couplings (I)TutorialFest at Babylon

09:00 60m Tutorial		[T6] Verifying Probabilistic Properties with Couplings TutorialFest Justin HsuUniversity of Wisconsin-Madison, USA File Attached

09:00 - 10:00	Morning KeynoteADSL at Conde

09:00 60m Talk		Relational reasoning using concurrent separation logic ADSL A: Robbert KrebbersDelft University of Technology Media Attached File Attached

09:00 - 10:00	Verified Quantum Computing (I)TutorialFest at Endymion

09:00 60m 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 5m Day opening		Opening PEPM Casper Bach PoulsenDelft University of Technology, Zhenjiang HuPeking University
09:05 55m Talk		Network Verification: Past, Present, and Future PEPM Nate FosterCornell University

09:00 - 10:00	Invited talkCPP at Maurepas Chair(s): Cătălin HriţcuInria Paris

09:00 60m 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	Building Program Reasoning Tools using LLVM and Z3 (I)TutorialFest at Muses

09:00 60m 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	Synthesizing Programs from Types (I)TutorialFest at SHANGRI-LA

09:00 60m Tutorial		[T3] Synthesizing Programs from Types TutorialFest Nadia PolikarpovaUniversity of California, San Diego Link to publication File Attached

09:00 - 10:00	Invited 3VMCAI at St Jerome Chair(s): Damien ZuffereyMPI-SWS

09:00 60m Talk		Model Checking for Safe Autonomy VMCAI Rajeev AlurUniversity of Pennsylvania

	10:00 - 10:30	Monday Morning BreakCatering at Break

10:30 - 12:30	Verifying Probabilistic Properties with Couplings (II)TutorialFest at Babylon

10:30 2h 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 25m Talk		AQuA: ASP-based Visual Question Answering PADL Kinjal Basu, Farhad Shakerin, Gopal Gupta
10:55 15m Short-paper		Diagnosing Data Pipeline Failures Using Action Languages: A Progress Report PADL Alex Brik, Jeffrey XuUCLA
11:10 15m 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 35m 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 - 12:30	Research PapersADSL at Conde

10:30 30m Research paper		Extending the Profile Abstraction for Complete Entailment Checking of Symbolic Heaps of Bounded Treewidth ADSL A: Florian ZulegerTU Vienna, A: Jens Katelaan File Attached
11:00 30m Research paper		Steel: scaling up memory reasoning for F* ADSL Denis MerigouxINRIA, Aymeric FromherzCarnegie Mellon University File Attached
11:30 30m Research paper		Strong-Separation Logic ADSL A: Florian ZulegerTU Vienna, A: Jens Katelaan File Attached
12:00 30m Research paper		The Lower Bound of Decidable Entailments in Separation Logic with Inductive Definitions ADSL Mnacho Echenim, Radu IosifVERIMAG, CNRS, Université Grenoble-Alpes, Nicolas Peltier Pre-print File Attached

10:30 - 12:30	Verified Quantum Computing (II)TutorialFest at Endymion

10:30 2h 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 35m Talk		Dependently-Typed Multi-Stage Programming Revisited (invited talk) PEPM Atsushi IgarashiKyoto University, Japan
11:05 25m Research paper		High-Fidelity Metaprogramming with Separator Syntax Trees PEPM Rodin AarssenCWI, Netherlands, Tijs van der StormCWI & University of Groningen, Netherlands DOI
11:30 15m Break		Mini Break 1 PEPM
11:45 25m Research paper		Module Generation without Regret PEPM Yuhi SatoUniversity of Tsukuba, Yukiyoshi KameyamaUniversity of Tsukuba, Japan, Takahisa WatanabeUniversity of Tsukuba, Japan DOI
12:10 20m 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 - 11:35	Program verificationCPP at Maurepas Chair(s): Nikhil SwamyMicrosoft Research

10:30 21m Talk		A Verified Packrat Parser Interpreter for Parsing Expression Grammars CPP Clement BlaudeauEcole Polytechnique, Natarajan ShankarSRI International, USA DOI Pre-print Media Attached
10:51 22m Talk		Proof Pearl: Braun Trees CPP Tobias NipkowTechnische Universität München, Thomas SewellChalmers University of Technology, Sweden DOI Pre-print Media Attached
11:13 22m Talk		FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq CPP Thomas LetanANSSI, Yann Régis-GianasIRIF, University Paris Diderot and CNRS, France / INRIA PI.R2 DOI Pre-print Media Attached

10:30 - 12:30	Building Program Reasoning Tools using LLVM and Z3 (II)TutorialFest at Muses

10:30 2h 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	Synthesizing Programs from Types (II)TutorialFest at SHANGRI-LA

10:30 2h Tutorial		[T3] Synthesizing Programs from Types TutorialFest Nadia PolikarpovaUniversity of California, San Diego Link to publication File Attached

10:30 - 12:30	Papers 3VMCAI at St Jerome Chair(s): Dirk BeyerLMU Munich

10:30 30m Research paper		A Systematic Approach to Abstract Interpretation of Program Transformations VMCAI Sven KeidelJGU Mainz, Sebastian ErdwegJGU Mainz Pre-print
11:00 30m Talk		Sharing Ghost Variables in a Collection of Abstract Domains VMCAI Marc ChevalierENS, CNRS, PSL University, INRIA, Jerome FeretINRIA Paris
11:30 30m Coffee break		Mini Break VMCAI
12:00 30m 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:30	Automated verification and SAT solvingCPP at Maurepas Chair(s): Ori LahavTel Aviv University

11:45 22m 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 22m Talk		Frying the Egg, Roasting The Chicken: Unit Deletions in DRAT Proofs CPP Adrian Rebola PardoTU Wien, Johannes AltmanningerTU Wien DOI Pre-print Media Attached

12:30 - 14:00	Monday LunchCatering at Lunch Room

12:30 90m 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 25m Talk		On the Effects of Integrating Region-based Memory Managemen and Generational Garbage Collection in ML PADL Martin ElsmanUniversity of Copenhagen, Denmark, Niels Hallenberg
13:55 25m Talk		RTMLton: An SML Runtime for Real-Time Systems PADL Bhargav Shivkumar, Jeffrey Murphy, Lukasz ZiarekSUNY Buffalo, USA
14:20 25m Talk		A Timed IO Monad PADL David JaninBordeaux INP / CNRS LaBRI / Bordeaux University
14:45 15m 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	Afternoon KeynoteADSL at Conde

14:00 65m Talk		SLEdge: Bounded Model Checking in Separation Logic ADSL A: Josh BerdineFacebook File Attached

14:00 - 15:05	Stateless Model Checking Algorithms and Tools for Strong and Weak Memory Models (I)TutorialFest at Endymion

14:00 65m 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 60m Talk		Reasoning about Progress of Concurrent Objects PEPM Xinyu FengNanjing University

14:00 - 15:05	Proof engineering and user interactionCPP at Maurepas Chair(s): Yves BertotINRIA

14:00 21m 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 21m 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 21m 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	Proving Semantic Type Soundness in Iris (I)TutorialFest at Muses

14:00 65m 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 65m 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 - 15:05	Papers 4VMCAI at St Jerome Chair(s): Ruzica PiskacYale University, USA

14:00 32m 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 32m 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:05 - 15:35	Monday Afternoon BreakCatering at Break

15:30 - 17:00	Answer Set Programming Applications and Competitive programming experiencePADL at Bacchus Chair(s): Alex Brik

15:30 25m Talk		Flexible Graph Matching and Graph Edit Distance Using Answer Set Programming PADL Sheung Chi Chan, James CheneyUniversity of Edinburgh, UK
15:55 25m Talk		On Repairing Web Services Workflows PADL Thanh Hai Nguyen, Enrico PontelliNew Mexico State University, Tran Cao Son
16:20 40m Talk		Competitive Programming with PiCat PADL Neng-Fa ZhouCUNY Brooklyn College and Graduate Center

15:35 - 17:45	Closing SessionADSL at Conde

15:35 65m Talk		Programs Synthesis with Separation Logic ADSL Nadia PolikarpovaUniversity of California, San Diego
16:40 65m 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 2h 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 35m Talk		Frex: Free extensions for normalisation by evaluation (invited talk) PEPM Ohad KammarUniversity of Edinburgh Media Attached
16:10 25m Research paper		Symbolic Bisimulation for Open and Parameterized System PEPM Zechen HouEast China Normal University, Eric MadelaineINRIA DOI File Attached
16:35 15m Break		Mini Break 2 PEPM
16:50 35m Talk		Acumen: A Domain-Specific Language for Cyber-Physical Systems (invited talk) PEPM Walid Taha
17:25 20m 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 21m 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 21m 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 21m Talk		Undecidability of Higher-Order Unification Formalised in Coq CPP Simon SpiesSaarland University, Yannick ForsterSaarland University DOI Pre-print Media Attached

15:35 - 17:35	Proving Semantic Type Soundness in Iris (II)TutorialFest at Muses

15:35 2h 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 2h 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 - 17:45	Papers 5VMCAI at St Jerome Chair(s): Nikolaj BjørnerMicrosoft Research

15:35 32m 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 32m 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 32m Coffee break		Mini Break VMCAI
17:12 32m Talk		Generalized Property-Directed Reachability for Hybrid Systems VMCAI Kohei SuenagaGraduate School of Informatics, Kyoto University, Takuya IshizawaKyoto University 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 22m 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 22m 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 22m Talk		PC Chairs' report CPP Jasmin BlanchetteVrije Universiteit Amsterdam, Cătălin HriţcuInria Paris DOI Media Attached File Attached

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 50m Talk		Invited Talk: Symbolic Reasoning About Machine Learning Systems PADL Adnan DarwicheUCLA
09:20 25m Talk		Exploiting Database Systems and Treewidth for Counting PADL Johannes K. FichteTU Dresden, Markus Hecher, Patrick Thier, Stefan Woltran
09:45 15m Short-paper		Whitebox Induction of Default Rules Using High-Utility Itemset Mining PADL Farhad Shakerin, Gopal Gupta

09:00 - 10:00	Morning 1PLMW at Ile de France III (IDF III) Chair(s): Stephanie BalzerCarnegie Mellon University, USA

09:00 10m Day opening		Opening PLMW Brigitte PientkaMcGill University
09:10 50m Talk		How to Write Papers So People Can Read ThemMentoring Event PLMW Derek DreyerMPI-SWS File Attached

09:00 - 10:00	Invited talkCPP at Maurepas Chair(s): Jasmin BlanchetteVrije Universiteit Amsterdam

09:00 60m Talk		Invited talk: Proof Assistants at the Hardware-Software Interface CPP Adam ChlipalaMassachusetts Institute of Technology DOI Media Attached

09:00 - 10:00	Opening & Interactive Knowledge SharesHASE at Orpheus

09:00 10m Day opening		Opening Plenary HASE
09:10 60m Tutorial		Interactive Knowledge Shares HASE Peter O'HearnFacebook, Philippa GardnerImperial College London, Muralidaran VijayaraghavanSiFive, Peter SewellUniversity of Cambridge

09:00 - 10:00	ALAFI at St Claude

09:00 60m Talk		Invited talk: Nonstandard Interpretation in Pyro LAFI I: Fritz Obermeyer Pre-print

09:00 - 10:00	Papers 6VMCAI at St Jerome Chair(s): Andreas PodelskiUniversity of Freiburg, Germany

09:00 30m 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 30m Talk		Improving Parity Game Solvers with Justifications VMCAI Ruben LapauwKatholieke Universiteit Leuven, Maurice BruynoogheKatholieke Universiteit Leuven, Marc DeneckerKatholieke Universiteit Leuven

	10:00 - 10:30	Tuesday Morning BreakCatering at Break

10:30 - 12:00	Small Languages and ImplementationPADL at Bacchus Chair(s): James CheneyUniversity of Edinburgh, UK

10:30 25m Talk		Explanations for Dynamic Programming PADL Martin ErwigOregon State University, Prashant Kumar, Alan Fern
10:55 25m Talk		A DSL for Integer Range Reasoning: Partition, Interval and Mapping Diagrams PADL Johannes Eriksson, Masoumeh Parsa
11:20 15m Short-paper		Variability-aware Datalog PADL Ramy Shahin, Marsha ChechikUniversity of Toronto
11:35 25m 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	Ally Skills SessionAlly Skills Session at Frontenac

10:30 2h 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 40m Talk		Making Progress Under Uncertainty in SMT Solving, Research, and LifeMentoring Event PLMW Lindsey KuperUniversity of California, Santa Cruz Media Attached
11:10 40m Talk		Research as a collaborative effortMentoring Event PLMW Marco GaboardiBoston University Media Attached File Attached
11:50 40m 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 21m Talk		Coq à la Carte - A Practical Approach to Modular Syntax with Binders CPP Yannick ForsterSaarland University, Kathrin StarkPrinceton University, USA DOI Pre-print Media Attached
10:51 21m 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 21m 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	Working Sessions IHASE at Orpheus

10:30 2h Meeting		Working Sessions I HASE Ben LaurieGoogle Research, Hong-Seok Kim, Jonathan ProtzenkoMicrosoft Research, Redmond

10:30 - 12:30	BLAFI at St Claude

10:30 30m Talk		A Differential-form Pullback Programming Language for Higher-order Reverse-mode Automatic Differentiation LAFI Carol MakUniversity of Oxford, C.-H. Luke OngUniversity of Oxford
11:00 30m Talk		A Monad for Point Processes LAFI Swaraj DashUniversity of Oxford, Sam StatonUniversity of Oxford File Attached
11:30 30m Talk		Denotational Semantics for Differentiable Programming with Manifolds LAFI Jesse SigalUniversity of Edinburgh
12:00 30m Talk		Backpropagation in the Simply Typed Lambda-calculus with Linear Negation LAFI Aloïs BrunelDeepomatic, Damiano MazzaCNRS, Michele PaganiIRIF - Université de Paris

10:30 - 12:30	Papers 7VMCAI at St Jerome Chair(s): Thomas WiesNew York University

10:30 30m 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 30m 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 30m Coffee break		Mini Break VMCAI
12:00 30m 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 22m 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 22m 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	Tuesday LunchCatering at Lunch Room

12:30 90m 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 30m Talk		Invited Talk: Relational Artificial Intelligence PADL Molham ArefRelational.ai
14:00 30m Talk		Invited Talk: Learning Interpretable Rules from Structured Data PADL Mayur NaikUniversity of Pennsylvania
14:30 30m 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 65m 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 - 15:05	Concurrency and linearityCPP at Maurepas Chair(s): Zhong ShaoYale University

14:00 21m Talk		Formalizing Determinacy of Concurrent Revisions CPP Roy OverbeekVrije Universiteit Amsterdam DOI Pre-print Media Attached
14:21 21m Talk		Formalizing π-calculus in Guarded Cubical Agda CPP Niccolò VeltriTallinn University of Technology, Andrea VezzosiIT University Copenhagen DOI Pre-print Media Attached File Attached
14:43 21m 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

14:00 - 15:05	Peer SkillshareHASE at Orpheus

13:30 45m Tutorial		Peer Skillshare HASE Sarah de HaasGoogle Research

14:00 - 15:05	CLAFI at St Claude

14:00 30m 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 15m 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 16m Talk		Monte Carlo Semantic Differencing of Probabilistic Programs LAFI Marco Cusumano-TownerMIT-CSAIL, Vikash MansinghkaMIT

14:00 - 15:05	Papers 8VMCAI at St Jerome Chair(s): Ori LahavTel Aviv University

14:00 32m 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 32m 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:05 - 15:35	Tuesday Afternoon BreakCatering at Break

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 30m Talk		Invited Talk: We Are All Poor Schmucks: On the Value of Gradual Types PADL Philip WadlerUniversity of Edinburgh, UK
16:00 45m 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 15m Day closing		Closing PADL Ekaterina KomendantskayaHeriot-Watt University, UK, Y. Annie LiuStony Brook University

15:35 - 17:45	POPLmark 15 Year Retrospective PanelPOPLmark 15 Year Retrospective Panel at Frontenac

15:35 2h 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 60m 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 10m Coffee break		Mini break PLMW
16:50 45m 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 21m 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 21m 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 21m Talk		Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq CPP Christian DoczkalUniversité Côte d'Azur, Damien PousCNRS, ENS Lyon DOI Pre-print Media Attached

15:35 - 17:45	Afternoon SessionHASE at Orpheus

14:30 2h Meeting		Working Sessions II HASE Ben LaurieGoogle Research, Satnam SinghGoogle Research
16:30 75m Day closing		Closing Plenary HASE

15:35 - 17:45	DLAFI at St Claude

15:35 30m Talk		Coinductive Trees for Exact Inference of Probabilistic Programs LAFI Alexander BagnallOhio University, Gordon StewartOhio University, Anindya BanerjeeIMDEA Software Institute
16:05 30m Talk		Name generation and Higher-order Probabilistic Programming (Or is new=rnd?) LAFI Dario SteinUniversity of Oxford, Sam StatonUniversity of Oxford, Michael WolmanMcGill University File Attached
16:35 30m Talk		Density Functions of Statistical Probabilistic Programs LAFI Tom MattinsonUniversity of Oxford, C.-H. Luke OngUniversity of Oxford
17:05 30m Talk		Probabilistic Programming around Gaussian Processes LAFI David TolpinPUB+
17:35 10m Day closing		Closing LAFI

15:35 - 17:45	Panel SessionVMCAI at St Jerome Chair(s): Dirk BeyerLMU Munich

15:35 2h10m 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 22m Talk		The Poincaré-Bendixson Theorem in Isabelle/HOL CPP Fabian ImmlerCarnegie Mellon University, Yong Kiam TanCarnegie Mellon University, USA DOI Pre-print Media Attached
17:12 22m Talk		A Formal Proof of the Independence of the Continuum Hypothesis CPP Jesse Michael HanUniversity of Pittsburgh, Floris van DoornUniversity of Pittsburgh DOI Pre-print Media Attached
17:34 22m Talk		The Lean mathematical library CPP The mathlib Community DOI Pre-print Media Attached File Attached

Wed 22 Jan
Times are displayed in time zone: Saskatchewan, Central America change

07:45 - 08:45	Wednesday Mentoring BreakfastMentoring Breakfasts at Breakfast Room

07:45 60m 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 15m 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 60m Talk		Can Programming Languages Research impact Deep Learning 2.0?Invited Talk Research Papers Martin VechevETH Zürich Media Attached

	10:00 - 10:30	Wednesday Morning BreakCatering at Break

10:30 - 11:35	Probabilistic ProgrammingResearch Papers at Ile de France II (IDF II) Chair(s): Alexandra SilvaUniversity College London

10:30 21m Talk		Towards Verified Stochastic Variational Inference for Probabilistic Programs Research Papers Wonyeol LeeKAIST, Hangyeol YuKAIST, Xavier RivalINRIA/CNRS/ENS Paris, Hongseok YangKAIST Link to publication DOI Media Attached
10:51 21m 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 21m Talk		Semantics of Higher-Order Probabilistic Programs with Conditioning Research Papers Fredrik DahlqvistUniversity College London, Dexter KozenCornell University 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 21m 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 21m 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 21m 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 22m 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 22m 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 22m 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 22m Talk		Synthesizing Replacement Classes Research Papers Malavika SamakCSAIL, MIT, Deokhwan KimCSAIL, MIT, Martin RinardMIT Link to publication DOI Media Attached File Attached

12:30 - 14:00	LGBTQ LunchLGBTQ Lunch at Endymion

12:30 90m Lunch		LGBTQ LunchMentoring Event LGBTQ Lunch

12:30 - 14:00	Wednesday LunchCatering at Lunch Room

12:30 90m 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 21m 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 21m 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 21m 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 21m 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 21m 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 21m 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:05 - 15:35	Wednesday Afternoon BreakCatering at Break

15:35 - 16:40	Automatic Differentiation / Kleene AlgebraResearch Papers at Ile de France II (IDF II) Chair(s): Lars BirkedalAarhus University

15:35 21m Talk		A Simple Differentiable Programming Language Research Papers Gordon PlotkinGoogle, Martín AbadiGoogle Link to publication DOI Media Attached
15:56 21m Talk		Backpropagation in the Simply Typed Lambda-calculus with Linear Negation Research Papers Aloïs BrunelDeepomatic, Damiano MazzaCNRS, Michele PaganiIRIF - Université de Paris Link to publication DOI Media Attached File Attached
16:18 21m 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 21m 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 21m Talk		Reductions for Safety Proofs Research Papers Azadeh FarzanUniversity of Toronto, Anthony VandikasUniversity of Toronto Link to publication DOI Media Attached
16:18 21m 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 22m 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 22m 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	SRC Poster SessionStudent Research Competition at SRC

16:50 2h10m Poster		SRC Poster Session Student Research Competition

17:35 - 18:35	Social Hour (Supported by Facebook)Research Papers at Social Hour

17:35 60m Social Event		Social Hour (Supported by Facebook) Research Papers

Thu 23 Jan
Times are displayed in time zone: Saskatchewan, Central America change

07:45 - 09:00	Thursday Mentoring BreakfastMentoring Breakfasts at Breakfast Room

07:45 75m 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 60m Talk		What is a Secure Programming Language? Invited Talk Research Papers Cristina CifuentesOracle Labs Link to publication Media Attached

	10:00 - 10:30	Thursday Morning BreakCatering at Break

10:30 - 11:35	Types and EffectsResearch Papers at Ile de France II (IDF II) Chair(s): Dominique DevrieseVrije Universiteit Brussel

10:30 21m 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 21m Talk		The Fire Triangle: How to Mix Substitution, Dependent Elimination, and Effects Research Papers Pierre-Marie PédrotINRIA, Nicolas TabareauInria Link to publication DOI Media Attached
11:13 21m Talk		SyTeCi: Automating Contextual Equivalence for Higher-Order Programs with References Research Papers Guilhem JaberLS2N, Université de Nantes Link to publication DOI Media Attached

10:30 - 11:35	SynthesisResearch Papers at Ile de France III (IDF III) Chair(s): Mohsen LesaniUniversity of California, Riverside

10:30 21m Talk		Synthesis of Coordination Programs from Linear Temporal Specifications Research Papers Suguman BansalRice University, USA, Kedar NamjoshiBell Labs, Nokia, Yaniv Sa'arNokia Bell Labs, Kfar Saba, Israel Link to publication DOI Media Attached File Attached
10:51 21m Talk		Augmented Example-based Synthesis using Relational Perturbation Properties Research Papers Shengwei AnPurdue University, Rishabh SinghGoogle Brain, Sasa MisailovicUniversity of Illinois at Urbana-Champaign, Roopsha SamantaPurdue University Link to publication DOI Media Attached File Attached
11:13 21m Talk		Provenance-Guided Synthesis of Datalog Programs Research Papers Mukund RaghothamanUniversity of Southern California, Jonathan MendelsonUniversity of Pennsylvania, David ZhaoThe University of Sydney, Mayur NaikUniversity of Pennsylvania, Bernhard ScholzUniversity of Sydney, Australia Link to publication DOI Media Attached File 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 22m Talk		Fast, Sound, and Effectively Complete Dynamic Race Prediction Research Papers Andreas PavlogiannisAarhus University Link to publication DOI Media Attached File Attached
12:07 22m 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 22m 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 22m 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	Thursday LunchCatering at Lunch Room

12:30 90m 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 21m Talk		Undecidability of D<: and Its Decidable FragmentsDistinguished Paper Research Papers Jason Z.S. HuMcGill University, Ondřej LhotákUniversity of Waterloo Link to publication DOI Media Attached File Attached
14:21 21m 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 21m 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:05	Abstract InterpretationResearch Papers at Ile de France III (IDF III) Chair(s): Xavier RivalINRIA/CNRS/ENS Paris

14:00 21m Talk		Abstract Extensionality: On the Properties of Incomplete Abstract Interpretations Research Papers Roberto BruniUniversity of Pisa, Roberto GiacobazziUniversity of Verona and IMDEA Software Institute, Roberta GoriUniversity of Pisa, Isabel Garcia-ContrerasIMDEA Software Institute, Dusko PavlovicUniversity of Hawaii Link to publication DOI Media Attached File Attached
14:21 21m Talk		Abstract Interpretation of Distributed Network Control Planes Research Papers Ryan BeckettMicrosoft Research, Aarti GuptaPrinceton University, Ratul MahajanUniversity of Washington, Intentionet, David WalkerPrinceton University Link to publication DOI Media Attached File Attached
14:43 21m Talk		Deterministic Parallel Fixpoint Computation Research Papers Sung Kook KimUniversity of California, Davis, Arnaud J. VenetFacebook, Aditya V. ThakurUniversity of California, Davis Link to publication DOI Pre-print Media Attached File Attached

14:00 - 15:30	SRC Finalists PresentationsStudent Research Competition at St Jerome

14:00 90m Talk		SRC Finalists Presentations Student Research Competition

	15:05 - 15:35	Thursday Afternoon BreakCatering at Break

15:35 - 16:40	Program LogicsResearch Papers at Ile de France II (IDF II) Chair(s): Chung-Kil HurSeoul National University

15:35 21m 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 21m 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 21m 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 21m 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 21m Talk		PλωNK: Functional Probabilistic NetKAT Research Papers Alexander VandenbrouckeKU Leuven, Belgium, Tom SchrijversKU Leuven Link to publication DOI Media Attached File Attached
16:18 21m 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	Business Meeting & SRC AwardsResearch Papers at Ile de France II (IDF II)

16:50 70m Meeting		Business Meeting & SRC Awards Research Papers Media Attached

18:00 - 19:00	Social Hour (Supported by Microsoft)Research Papers at Social Hour

18:00 60m Social Event		Social Hour (Supported by Microsoft) Research Papers

19:00 - 21:00	W@POPL DinnerW@POPL Dinner at Palace Cafe

19:00 2h Dinner		W@POPL DinnerMentoring Event W@POPL Dinner

Fri 24 Jan
Times are displayed in time zone: Saskatchewan, Central America change

07:45 - 09:00	Friday Mentoring BreakfastMentoring Breakfasts at Breakfast Room

07:45 75m 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 60m Talk		Probabilistic ProgrammingInvited Talk Research Papers Hongseok YangKAIST Media Attached File Attached

	10:00 - 10:30	Friday Morning BreakCatering at Break

10:30 - 11:35	Type SystemsResearch Papers at Ile de France II (IDF II) Chair(s): Dominique DevrieseVrije Universiteit Brussel

10:30 21m 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 21m 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 21m Talk		Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation Research Papers Roland MeyerTU Braunschweig, Sebastian WolffTU Braunschweig Link to publication DOI Media Attached File Attached

10:30 - 11:35	Verification in Proof AssistantsResearch Papers at Ile de France III (IDF III) Chair(s): Sandrine BlazyUniv Rennes- IRISA

10:30 21m Talk		Virtual Timeline: A Formal Abstraction for Verifying Preemptive Schedulers with Temporal Isolation Research Papers Mengqi LiuYale University, Lionel RiegVerimag, Zhong ShaoYale University, Ronghui GuColumbia University, David CostanzoYale University, Jung-Eun KimYale University, Man-Ki YoonYale University Link to publication DOI Media Attached File Attached
10:51 21m Talk		The High-Level Benefits of Low-Level Sandboxing Research Papers Michael SammlerMPI-SWS, Deepak GargMax Planck Institute for Software Systems, Derek DreyerMPI-SWS, Tadeusz LitakFAU Erlangen-Nuremberg, INF 8 Link to publication DOI Media Attached
11:13 21m Talk		Interaction Trees: Representing Recursive and Impure Programs in CoqDistinguished Paper Research Papers Li-yao XiaUniversity of Pennsylvania, Yannick ZakowskiUniversity of Pennsylvania, Paul HeUniversity of Pennsylvania, Chung-Kil HurSeoul National University, Gregory MalechaBedRock Systems, Benjamin C. PierceUniversity of Pennsylvania, Steve ZdancewicUniversity of Pennsylvania 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 22m Talk		Label-Dependent Session Types Research Papers Peter ThiemannUniversity of Freiburg, Germany, Vasco T. VasconcelosUniversity of Lisbon, Portugal Link to publication DOI Media Attached
12:07 22m Talk		Par means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs Research Papers Federico AschieriTU Wien, Francesco A. GencoIHPST, Université Paris 1 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 22m 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 22m 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	Friday LunchCatering at Lunch Room

12:30 90m 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 21m Talk		Full Abstraction for the Quantum Lambda-Calculus Research Papers Pierre ClairambaultCNRS & ENS Lyon, Marc De VismeENS Lyon Link to publication DOI Media Attached File Attached
14:21 21m 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 21m 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 21m Talk		Stacked Borrows: An Aliasing Model for Rust Research Papers Ralf JungMPI-SWS, Hoang-Hai DangMPI-SWS, Jeehoon KangKAIST, Derek DreyerMPI-SWS Link to publication DOI Media Attached File Attached
14:21 21m Talk		Executable Formal Semantics for the POSIX Shell Research Papers Michael GreenbergPomona College, Austin J. BlattPuppet Labs Link to publication DOI Media Attached File Attached
14:43 21m 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:05 - 15:35	Friday Afternoon BreakCatering at Break

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 21m Talk		Taylor Subsumes Scott, Berry, Kahn and PlotkinDistinguished Paper Research Papers Davide BarbarossaUniversité Paris 13, Giulio ManzonettoUniversité Paris 13 Link to publication DOI Media Attached File Attached
15:56 21m 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 21m 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

15:35 - 16:40	Verified & Secure CompilationResearch Papers at Ile de France III (IDF III) Chair(s): Andrew AppelPrinceton

15:35 21m Talk		Formal Verification of a Constant-Time Preserving C Compiler Research Papers Gilles BartheMPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Sandrine BlazyUniv Rennes- IRISA, Benjamin GregoireINRIA, Rémi HutinIRISA / ENS Rennes, Vincent LaporteInria, David PichardieUniv Rennes, ENS Rennes, IRISA, Alix TrieuAarhus University Link to publication DOI Media Attached File Attached
15:56 21m Talk		CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification Research Papers Youngju SongSeoul National University, Minki ChoSeoul National University, Dongjoo KimSeoul National University, Yonghyun KimSeoul National University, South Korea, Jeehoon KangKAIST, Chung-Kil HurSeoul National University Link to publication DOI Media Attached File Attached
16:18 21m Talk		Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset Research Papers Timothy BourkeInria / École normale supérieure, Lélio BrunENS/Inria, Marc PouzetÉcole normale supérieure Link to publication DOI Media Attached File Attached

16:40 - 17:40	Social Hour (Supported by Tezos)Research Papers at Social Hour

16:40 60m Social Event		Social Hour (Supported by Tezos) Research Papers

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 60m Talk		SMTCoq: Safe and efficient automation in Coq (Keynote) CoqPL Chantal KellerLRI, Université Paris-Sud File Attached

09:00 - 10:00	Gradual CriteriaWGT at Orleans Chair(s): Amal AhmedNortheastern University, USA

09:00 30m Talk		Gradual Typing as if Types Mattered WGT Ronald GarciaUniversity of British Columbia, Éric TanterUniversity of Chile Pre-print
09:30 30m Talk		Fully Abstract from Static to Gradual WGT Koen JacobsKU Leuven, Amin Timanyimec-Distrinet KU-Leuven, Dominique DevrieseVrije Universiteit Brussel Pre-print

09:00 - 10:00	KeynotePriSC at Rosalie

09:00 5m Day opening		PriSC Introduction PriSC Dominique DevrieseVrije Universiteit Brussel File Attached
09:05 55m Industry talk		Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing PriSC K: Tyler McMullenFastly Media Attached

	10:00 - 10:30	Saturday Morning BreakCatering at Break

10:30 - 12:30	Contributed TalksCoqPL at Maurepas Chair(s): Amin Timanyimec-Distrinet KU-Leuven

10:30 30m Talk		Deriving Instances with Dependent Types CoqPL Arthur Azevedo de AmorimCarnegie Mellon University, USA File Attached
11:00 30m Talk		The use of Coq for Common Criteria Evaluations CoqPL Yves BertotINRIA, Maxime DénèsInria, Vincent LaporteInria, Arnaud FontaineANSSI, Thomas LetanANSSI File Attached
11:30 30m 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 30m 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 30m 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 30m Talk		Gradual Typing for Extensibility by Rows WGT Taro SekiyamaNational Institute of Informatics, Atsushi IgarashiKyoto University, Japan Pre-print
11:30 30m Talk		Foreign Function Typing: Semantic Type Soundness for FFIs WGT Daniel PattersonNortheastern University, Amal AhmedNortheastern University, USA Pre-print
12:00 30m Talk		Space-Efficient Monotonic References WGT Deyaaeldeen AlmahallawiIndiana University, Jeremy G. SiekIndiana University, USA Pre-print

10:30 - 12:30	Foundations and timing channelsPriSC at Rosalie Chair(s): Marco VassenaCISPA Helmholtz Center for Information Security

10:30 24m Talk		Exorcising Spectres with Secure Compilers PriSC Marco PatrignaniStanford University & CISPA , Marco GuarnieriIMDEA Software Institute Media Attached File Attached
10:54 24m Talk		Trace-Relating Compiler Correctness and Secure Compilation PriSC Carmine AbateInria Paris, Roberto BlancoInria, Stefan CiobacaAlexandru Ioan Cuza University of Iasi, Deepak GargMax Planck Institute for Software Systems, Cătălin HriţcuInria Paris, Marco PatrignaniStanford University & CISPA , Éric TanterUniversity of Chile, Jérémy ThibaultInria Paris Media Attached File Attached
11:18 24m Talk		Reconciling progress-insensitive noninterference and declassification PriSC Johan BayAarhus University, Aslan AskarovAarhus University Media Attached File Attached
11:42 24m Talk		Hermes: Implementing Cryptography without Side-channels PriSC Ken Friis LarsenDIKU, University of Copenhagen, Torben MogensenDIKU, University of Copenhagen, Michael Kirkedal ThomsenDIKU, University of Copenhagen
12:06 24m Talk		A CompCert Compiler that Preserves Cryptographic Constant-time PriSC Sandrine BlazyUniv Rennes- IRISA, Rémi HutinIRISA / ENS Rennes, David PichardieUniv Rennes, ENS Rennes, IRISA Media Attached

12:30 - 14:00	Saturday LunchCatering at Lunch Room

12:30 90m Lunch		Lunch Catering

14:00 - 15:05	Invited TalkCoqPL at Maurepas Chair(s): Yves BertotINRIA

14:00 60m Talk		Autosubst 2: Mechanising binders in Coq (Keynote) CoqPL Kathrin StarkPrinceton University, USA File Attached

14:00 - 15:05	CoercionsWGT at Orleans Chair(s): Jeremy G. SiekIndiana University, USA

14:00 32m 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 32m Talk		Space-Efficient Gradual Typing in Coercion-Passing Style WGT Yuya TsudaKyoto University, Atsushi IgarashiKyoto University, Japan, Tomoya TabuchiKyoto University Pre-print

14:00 - 15:05	New outlooks on secure compilationPriSC at Rosalie Chair(s): Cristina CifuentesOracle Labs

14:00 24m 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 24m 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 8m 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 8m Talk		Short Talk: Everparse PriSC Tahina RamananandroMicrosoft Research, n.n. Media Attached

	15:05 - 15:35	Saturday Afternoon BreakCatering at Break

15:35 - 17:45	Contributed Talks & Coq DevelopersCoqPL at Maurepas Chair(s): Joseph TassarottiBoston College, Robbert KrebbersDelft University of Technology

15:35 30m 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 30m 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 15m Break		Short break CoqPL
16:50 45m Demonstration		Session with the Coq Development Team CoqPL Maxime DénèsInria, Matthieu SozeauInria

15:35 - 17:45	Analysis, verification, blameWGT at Orleans Chair(s): Niki VazouIMDEA Software Institute

15:35 32m 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 33m 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 10m Break		Minibreak WGT
16:50 30m 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 25m 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 24m 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 24m Talk		Mechanized Reasoning about a Capability Machine PriSC Aina Linn GeorgesAarhus University, Alix TrieuAarhus University, Lars BirkedalAarhus University Media Attached
16:23 24m 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 10m Break		Mini-break PriSC
16:57 24m 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 24m 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


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
Break			Catering Sunday Morning Break											Catering Sunday Afternoon Break
Lunch Room								Catering Sunday Lunch
Maurepas	PLanQC Introduction and Invited Talks			PLanQC Invited Talks, Pulses, Errors and Categories							PLanQC Formal Methods					PLanQC NISQ			PLanQC Quantum-Classical Communication
St Jerome	VMCAI Invited 1			VMCAI Papers 1							VMCAI Invited 2					VMCAI Papers 2

Mon 20 Jan
Times are displayed in time zone: Saskatchewan, Central America change


Room	8:00	30	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
Babylon			TutorialFest Verifying Probabilistic Properties with Couplings (I)			TutorialFest Verifying Probabilistic Properties with Couplings (II)
Bacchus		PADL Logical Engines and Applications				PADL Answer Set Programming Systems							PADL Memory and Real-Time in Functional Programming					PADL Answer Set Programming Applications and Competitive programming experience
Break					Catering Monday Morning Break												Catering Monday Afternoon Break
Conde			ADSL Morning Keynote			ADSL Research Papers								ADSL Afternoon Keynote					ADSL Closing Session
Endymion			TutorialFest Verified Quantum Computing (I)			TutorialFest Verified Quantum Computing (II)								TutorialFest Stateless Model Checking Algorithms and Tools for Strong and Weak Memory Models (I)					TutorialFest Stateless Model Checking Algorithms and Tools for Strong and Weak Memory Models (II)
Frontenac			PEPM Opening & Keynote Talk 1			PEPM Sessions 1 & 2								PEPM Keynote Talk 2					PEPM Sessions 3 & 4
Lunch Room											Catering Monday Lunch
Maurepas			CPP Invited talk			CPP Program verification			CPP Automated verification and SAT solving					CPP Proof engineering and user interaction					CPP Decidability and complexity			CPP Homotopy Type Theory and PC chairs' report
Muses			TutorialFest Building Program Reasoning Tools using LLVM and Z3 (I)			TutorialFest Building Program Reasoning Tools using LLVM and Z3 (II)								TutorialFest Proving Semantic Type Soundness in Iris (I)					TutorialFest Proving Semantic Type Soundness in Iris (II)
SHANGRI-LA			TutorialFest Synthesizing Programs from Types (I)			TutorialFest Synthesizing Programs from Types (II)								TutorialFest Programming and Reasoning with Kleene Algebra with Tests (I)					TutorialFest Programming and Reasoning with Kleene Algebra with Tests (II)
St Jerome			VMCAI Invited 3			VMCAI Papers 3								VMCAI Papers 4					VMCAI Papers 5

Tue 21 Jan
Times are displayed in time zone: Saskatchewan, Central America change


Room	8:00	30	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
Bacchus		PADL Reasoning and Efficient Implementation				PADL Small Languages and Implementation							PADL Invited Experience and Direction Session					PADL Invited Experience and Direction Session (Continued)
Break					Catering Tuesday Morning Break												Catering Tuesday Afternoon Break
Frontenac						Ally Skills Session Ally Skills Session													POPLmark 15 Year Retrospective Panel POPLmark 15 Year Retrospective Panel
Ile de France III (IDF III)			PLMW Morning 1			PLMW Morning 2								PLMW Afternoon 1					PLMW Afternoon 2
Lunch Room											Catering Tuesday Lunch
Maurepas			CPP Invited talk			CPP Mechanized metatheory			CPP Verified cryptography					CPP Concurrency and linearity					CPP Formalized mathematics 1			CPP Formalized mathematics 2
Orpheus			HASE Opening & Interactive Knowledge Shares			HASE Working Sessions I								HASE Peer Skillshare					HASE Afternoon Session
St Claude			LAFI A			LAFI B								LAFI C					LAFI D
St Jerome			VMCAI Papers 6			VMCAI Papers 7								VMCAI Papers 8					VMCAI Panel Session

Wed 22 Jan
Times are displayed in time zone: Saskatchewan, Central America change


Room	7:00	30		8:00	30		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	18:00	30
Break									Catering Wednesday Morning Break													Catering Wednesday Afternoon Break
Breakfast Room			Mentoring Breakfasts Wednesday Mentoring Breakfast
Endymion															LGBTQ Lunch LGBTQ Lunch
Ile de France II (IDF II)						Research Papers Welcome + SIGPLAN Award Ceremony	Research Papers Invited Talk			Research Papers Probabilistic Programming			Research Papers Reasoning about Program Complexity/Efficiency						Research Papers Program Logics					Research Papers Automatic Differentiation / Kleene Algebra			Research Papers Synthesis and Decision Procedures
Ile de France III (IDF III)										Research Papers Complexity / Decision Procedures			Research Papers Synthesis						Research Papers Gradual Typing / Language Design					Research Papers Concurrency / Memory
Lunch Room															Catering Wednesday Lunch
SRC															Student Research Competition SRC Poster Session
Social Hour															Research Papers Social Hour (Supported by Facebook)

Thu 23 Jan
Times are displayed in time zone: Saskatchewan, Central America change


Room	7:00	30		8:00	30	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	18:00	30	19:00	30	20:00	30
Break								Catering Thursday Morning Break													Catering Thursday Afternoon Break
Breakfast Room			Mentoring Breakfasts Thursday Mentoring Breakfast
Ile de France II (IDF II)						Research Papers Invited Talk			Research Papers Types and Effects			Research Papers Dynamic Program Analysis						Research Papers Type Systems					Research Papers Program Logics			Research Papers Business Meeting & SRC Awards
Ile de France III (IDF III)									Research Papers Synthesis			Research Papers Datalog, OO + Functional Programming						Research Papers Abstract Interpretation					Research Papers Probabilistic Programming
Lunch Room														Catering Thursday Lunch
Palace Cafe														W@POPL Dinner W@POPL Dinner
Social Hour														Research Papers Social Hour (Supported by Microsoft)
St Jerome														Student Research Competition SRC Finalists Presentations

Fri 24 Jan
Times are displayed in time zone: Saskatchewan, Central America change


Room	7:00	30		8:00	30	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
Break								Catering Friday Morning Break													Catering Friday Afternoon Break
Breakfast Room			Mentoring Breakfasts Friday Mentoring Breakfast
Ile de France II (IDF II)						Research Papers Invited Talk			Research Papers Type Systems			Research Papers Concurrent Programming & Session Types						Research Papers Semantics of Probabilistic & Quantum Programming					Research Papers Semantics & Type Theory
Ile de France III (IDF III)									Research Papers Verification in Proof Assistants			Research Papers Probabilistic Reasoning and Verification						Research Papers Language Design					Research Papers Verified & Secure Compilation
Lunch Room														Catering Friday Lunch
Social Hour														Research Papers Social Hour (Supported by Tezos)

Sat 25 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
Break			Catering Saturday Morning Break											Catering Saturday Afternoon Break
Lunch Room								Catering Saturday Lunch
Maurepas	CoqPL Invited Talk			CoqPL Contributed Talks							CoqPL Invited Talk					CoqPL Contributed Talks & Coq Developers
Orleans	WGT Gradual Criteria			WGT Programming features							WGT Coercions					WGT Analysis, verification, blame
Rosalie	PriSC Keynote			PriSC Foundations and timing channels							PriSC New outlooks on secure compilation					PriSC Compartmentalization, memory safety, and isolation

Sun 19 Jan
Times are displayed in time zone: Saskatchewan, Central America change


Room	9:00	15	30	45	10:00	15	30	45	11:00	15	30	45		12:00		15	30	45	13:00	15	30	45	14:00	15		30		45	15:00	15	30		45		16:00		15	30		45		17:00		15	30	45
Break					POPL Catering Break 10:00 - 10:30
Lunch Room																	POPL Catering Lunch 12:30 - 14:00
Maurepas	PLanQC Invited Talk: Quantum Computing for Programming Languages Researchers 09:00 - 09:30		PLanQC Invited Talk: Dependently Typed Quantum Programming in Proto-Quipper 09:30 - 10:00				PLanQC Invited Talk: Q# - Going Beyond Quantum Circuits 10:30 - 11:00		PLanQC Invited Talk: Resource-Efficient Quantum Computing by Breaking Abstractions 11:00 - 11:30		PLanQC Tuning up entanglement through the cloud using Qiskit-OpenPulse 11:30 - 11:50		PLanQC Tracking Errors through Types in Quantum Programs 11:50 - 12:10		PLanQC Quantum CPOs 12:10 - 12:30								PLanQC Runtime Analysis of Quantum Programs: A Formal Approach 14:00 - 14:20		PLanQC Qbricks: formal verification in quantum computing 14:20 - 14:40		PLanQC Merged Talk: A Verified Optimizer for Quantum Circuits & Verified Trans ... 14:40 - 15:05					PLanQC Optimal Two-Qubit Circuits for Universal Fault-Tolerant Quantum Computation 15:35 - 15:55		PLanQC Context-Sensitive and Duration-Aware Qubit Mapping for Various NISQ Devices 15:55 - 16:15			PLanQC Quingo: A Domain Specific Language for Quantum Computing with NISQ Features 16:15 - 16:35				PLanQC Extending Modern C++ for Heterogeneous Quantum-Classical Computing 16:50 - 17:10		PLanQC Formalization of a Programming Language for Quantum Circuits with Measu ... 17:10 - 17:30		PLanQC Automated distribution of quantum circuits via hypergraph partitioning 17:30 - 17:50
St Jerome	VMCAI The Siren Song of Temporal Synthesis 09:00 - 10:00						VMCAI Witnessing Secure Compilation 10:30 - 11:00		VMCAI BackFlow: Backward Context-sensitive Flow Reconstruction of Taint Analy ... 11:00 - 11:30		VMCAI Mini Break 11:30 - 12:00			VMCAI Fixing Code That Explodes Under Symbolic Evaluation 12:00 - 12:30									VMCAI Safety and Robustness for Deep Learning with Provable Guarantees 14:00 - 15:05									VMCAI The Correctness of a Code Generator for a Functional Language 15:35 - 16:07				VMCAI Leveraging Compiler Intermediate Representation for Multi- and Cross-La ... 16:07 - 16:40			VMCAI Mini Break 16:40 - 17:12				VMCAI Putting the Squeeze on Array Programs: Loop Verification via Inductive ... 17:12 - 17:45

Mon 20 Jan
Times are displayed in time zone: Saskatchewan, Central America change


Room	8:00	15	30	45	9:00		15	30		45	10:00	15	30	45			11:00			15		30	45	12:00			15	30	45	13:00	15	30	45		14:00	15		30	45	15:00	15	30		45		16:00			15		30			45		17:00		15		30		45
Babylon					POPL TutorialFest [T6] Verifying Probabilistic Properties with Couplings 09:00 - 10:00								POPL TutorialFest [T6] Verifying Probabilistic Properties with Couplings 10:30 - 12:30
Bacchus			PADL Opening 08:30 - 08:45	PADL Invited Talk: Logical Engines for Cloud Configurations 08:45 - 09:35					PADL Interactive Text Graph Mining with a Prolog-based Dialog Engine 09:35 - 10:00				PADL AQuA: ASP-based Visual Question Answering 10:30 - 10:55			PADL Diagnosing Data Pipeline Failures Using Action Languages: A Progress Report 10:55 - 11:10			PADL VRASP: A Virtual Reality Environment for Learning Answer Set Programming 11:10 - 11:25		PADL Panel: Programming with logic for the masses 11:25 - 12:00											PADL On the Effects of Integrating Region-based Memory Managemen and Generat ... 13:30 - 13:55		PADL RTMLton: An SML Runtime for Real-Time Systems 13:55 - 14:20			PADL A Timed IO Monad 14:20 - 14:45		PADL Panel: Memory and real-time programming in practice 14:45 - 15:00			PADL Flexible Graph Matching and Graph Edit Distance Using Answer Set Progra ... 15:30 - 15:55			PADL On Repairing Web Services Workflows 15:55 - 16:20					PADL Competitive Programming with PiCat 16:20 - 17:00
Conde					ADSL Relational reasoning using concurrent separation logic 09:00 - 10:00								ADSL Extending the Profile Abstraction for Complete Entailment Checking of S ... 10:30 - 11:00				ADSL Steel: scaling up memory reasoning for F* 11:00 - 11:30					ADSL Strong-Separation Logic 11:30 - 12:00		ADSL The Lower Bound of Decidable Entailments in Separation Logic with Induc ... 12:00 - 12:30											ADSL SLEdge: Bounded Model Checking in Separation Logic 14:00 - 15:05								ADSL Programs Synthesis with Separation Logic 15:35 - 16:40										ADSL Local Reasoning for Global Graph Properties 16:40 - 17:45
Endymion					POPL TutorialFest [T2] Verified Quantum Computing 09:00 - 10:00								POPL TutorialFest [T2] Verified Quantum Computing 10:30 - 12:30																						POPL TutorialFest [T5] Stateless Model Checking Algorithms and Tools for Strong and Weak ... 14:00 - 15:05								POPL TutorialFest [T5] Stateless Model Checking Algorithms and Tools for Strong and Weak ... 15:35 - 17:35
Frontenac					PEPM Opening 09:00 - 09:05	PEPM Network Verification: Past, Present, and Future 09:05 - 10:00							PEPM Dependently-Typed Multi-Stage Programming Revisited (invited talk) 10:30 - 11:05					PEPM High-Fidelity Metaprogramming with Separator Syntax Trees 11:05 - 11:30				PEPM Mini Break 1 11:30 - 11:45	PEPM Module Generation without Regret 11:45 - 12:10			PEPM GOOL: A Generic Object-Oriented Language 12:10 - 12:30									PEPM Reasoning about Progress of Concurrent Objects 14:00 - 15:00								PEPM Frex: Free extensions for normalisation by evaluation (invited talk) 15:35 - 16:10					PEPM Symbolic Bisimulation for Open and Parameterized System 16:10 - 16:35				PEPM Mini Break 2 16:35 - 16:50			PEPM Acumen: A Domain-Specific Language for Cyber-Physical Systems (invited ... 16:50 - 17:25				PEPM An approach to generating text-based IDEs with syntax completion from s ... 17:25 - 17:45
Lunch Room																												POPL Catering Lunch 12:30 - 14:00
Maurepas					CPP Invited talk: Matching Logic: The Foundation of the K Framework 09:00 - 10:00								CPP A Verified Packrat Parser Interpreter for Parsing Expression Grammars 10:30 - 10:51		CPP Proof Pearl: Braun Trees 10:51 - 11:13					CPP FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq 11:13 - 11:35			CPP Verifying x86 Instruction Implementations 11:45 - 12:07		CPP Frying the Egg, Roasting The Chicken: Unit Deletions in DRAT Proofs 12:07 - 12:30										CPP An Equational Theory for Weak Bisimulation via Generalized Parameterize ... 14:00 - 14:21		CPP Exploration of Neural Machine Translation in Autoformalization of Mathe ... 14:21 - 14:43		CPP REPLICA: REPL Instrumentation for Coq Analysis 14:43 - 15:05				CPP Verified Programming of Turing Machines in Coq 15:35 - 15:56		CPP A Functional Proof Pearl: Inverting the Ackermann Hierarchy 15:56 - 16:18					CPP Undecidability of Higher-Order Unification Formalised in Coq 16:18 - 16:40					CPP Cubical Synthetic Homotopy Theory 16:50 - 17:12		CPP Three equivalent ordinal notation systems in Cubical Agda 17:12 - 17:34				CPP PC Chairs' report 17:34 - 17:56
Muses					POPL TutorialFest [T1] Building Program Reasoning Tools using LLVM and Z3 09:00 - 10:00								POPL TutorialFest [T1] Building Program Reasoning Tools using LLVM and Z3 10:30 - 12:30																						POPL TutorialFest [T4] Proving Semantic Type Soundness in Iris 14:00 - 15:05								POPL TutorialFest [T4] Proving Semantic Type Soundness in Iris 15:35 - 17:35
SHANGRI-LA					POPL TutorialFest [T3] Synthesizing Programs from Types 09:00 - 10:00								POPL TutorialFest [T3] Synthesizing Programs from Types 10:30 - 12:30																						POPL TutorialFest [T7] Programming and Reasoning with Kleene Algebra with Tests 14:00 - 15:05								POPL TutorialFest [T7] Programming and Reasoning with Kleene Algebra with Tests 15:35 - 17:35
St Jerome					VMCAI Model Checking for Safe Autonomy 09:00 - 10:00								VMCAI A Systematic Approach to Abstract Interpretation of Program Transformations 10:30 - 11:00				VMCAI Sharing Ghost Variables in a Collection of Abstract Domains 11:00 - 11:30					VMCAI Mini Break 11:30 - 12:00		VMCAI Harnessing Static Analysis to Help Learn Pseudo-Inverses of String Mani ... 12:00 - 12:30											VMCAI Synthesizing Environment Invariants for Modular Hardware Verification 14:00 - 14:32			VMCAI Systematic Classification of Attackers via Bounded Model Checking 14:32 - 15:05					VMCAI Cheap CTL Compassion in NuSMV 15:35 - 16:07				VMCAI A Cooperative Parallelization Approach for Property-Directed k-Induction 16:07 - 16:40						VMCAI Mini Break 16:40 - 17:12				VMCAI Generalized Property-Directed Reachability for Hybrid Systems 17:12 - 17:45

Tue 21 Jan
Times are displayed in time zone: Saskatchewan, Central America change


Room	8:00	15	30	45	9:00		15		30	45	10:00	15	30	45		11:00		15		30		45		12:00	15	30	45	13:00	15	30	45	14:00	15	30	45	15:00	15	30		45	16:00	15	30	45	17:00	15	30	45
Bacchus			PADL Invited Talk: Symbolic Reasoning About Machine Learning Systems 08:30 - 09:20					PADL Exploiting Database Systems and Treewidth for Counting 09:20 - 09:45		PADL Whitebox Induction of Default Rules Using High-Utility Itemset Mining 09:45 - 10:00			PADL Explanations for Dynamic Programming 10:30 - 10:55		PADL A DSL for Integer Range Reasoning: Partition, Interval and Mapping Diagrams 10:55 - 11:20				PADL Variability-aware Datalog 11:20 - 11:35		PADL Panel: Reasoning for machine learning at large 11:35 - 12:00									PADL Invited Talk: Relational Artificial Intelligence 13:30 - 14:00		PADL Invited Talk: Learning Interpretable Rules from Structured Data 14:00 - 14:30		PADL Invited Talk: An Introduction to the Imandra Automated Reasoning System 14:30 - 15:00				PADL Invited Talk: We Are All Poor Schmucks: On the Value of Gradual Types 15:30 - 16:00			PADL Panel: Experience and Direction 16:00 - 16:45			PADL Closing 16:45 - 17:00
Frontenac													POPL Ally Skills SessionMentoring Event Ally Skills Session 10:30 - 12:30																										POPL mark 15 Year Retrospective Panel POPLmark 15 Year Retrospective Panel 15:35 - 17:35
Ile de France III (IDF III)					PLMW Opening 09:00 - 09:10	PLMWMentoring Event How to Write Papers So People Can Read Them 09:10 - 10:00							PLMWMentoring Event Making Progress Under Uncertainty in SMT Solving, Research, and Life 10:30 - 11:10				PLMWMentoring Event Research as a collaborative effort 11:10 - 11:50						PLMWMentoring Event Theorem provers are a P.L. researcher's best friend

POPL 2020 Program

Filter Program

Program Display Configuration

Sun 19 Jan Times are displayed in time zone: Saskatchewan, Central America change

Mon 20 Jan Times are displayed in time zone: Saskatchewan, Central America change

Tue 21 Jan Times are displayed in time zone: Saskatchewan, Central America change

Wed 22 Jan Times are displayed in time zone: Saskatchewan, Central America change

Thu 23 Jan Times are displayed in time zone: Saskatchewan, Central America change

Fri 24 Jan Times are displayed in time zone: Saskatchewan, Central America change

Sat 25 Jan Times are displayed in time zone: Saskatchewan, Central America change

Sun 19 Jan Times are displayed in time zone: Saskatchewan, Central America change

Catering

Catering

Catering

PLanQC

PLanQC

PLanQC

PLanQC

PLanQC

VMCAI

VMCAI

VMCAI

VMCAI

Mon 20 Jan Times are displayed in time zone: Saskatchewan, Central America change

TutorialFest

TutorialFest

PADL

PADL

PADL

PADL

Catering

Catering

ADSL

ADSL

ADSL

ADSL

TutorialFest

TutorialFest

TutorialFest

TutorialFest

PEPM

PEPM

PEPM

PEPM

Catering

CPP

CPP

CPP

CPP

CPP

CPP

TutorialFest

TutorialFest

TutorialFest

TutorialFest

TutorialFest

TutorialFest

TutorialFest

TutorialFest

VMCAI

VMCAI

VMCAI

VMCAI

Tue 21 Jan Times are displayed in time zone: Saskatchewan, Central America change

PADL

PADL

PADL

PADL

Catering

Catering

Ally Skills Session

POPLmark 15 Year Retrospective Panel

PLMW

PLMW

PLMW

PLMW

Catering

CPP

CPP

CPP

Sun 19 Jan
Times are displayed in time zone: Saskatchewan, Central America change

Mon 20 Jan
Times are displayed in time zone: Saskatchewan, Central America change

Tue 21 Jan
Times are displayed in time zone: Saskatchewan, Central America change

Wed 22 Jan
Times are displayed in time zone: Saskatchewan, Central America change

Thu 23 Jan
Times are displayed in time zone: Saskatchewan, Central America change

Fri 24 Jan
Times are displayed in time zone: Saskatchewan, Central America change

Sat 25 Jan
Times are displayed in time zone: Saskatchewan, Central America change

Sun 19 Jan
Times are displayed in time zone: Saskatchewan, Central America change

Mon 20 Jan
Times are displayed in time zone: Saskatchewan, Central America change

Tue 21 Jan
Times are displayed in time zone: Saskatchewan, Central America change

Wed 22 Jan
Times are displayed in time zone: Saskatchewan, Central America change

Thu 23 Jan
Times are displayed in time zone: Saskatchewan, Central America change

Fri 24 Jan
Times are displayed in time zone: Saskatchewan, Central America change

Sat 25 Jan
Times are displayed in time zone: Saskatchewan, Central America change