Maurepas - HASE 2020

VenueJW Marriott New Orleans

Room nameMaurepas

Floor3

Room InformationNo extra information available

Program

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
Displayed time zone: Saskatchewan, Central America change

09:00 - 10:00	Introduction and Invited TalksPLanQC at Maurepas Chair(s): Robert Rand University of Maryland

09:00 30m Talk		Invited Talk: Quantum Computing for Programming Languages Researchers PLanQC I: Jennifer Paykin Galois, Inc. Media Attached File Attached
09:30 30m Talk		Invited Talk: Dependently Typed Quantum Programming in Proto-Quipper PLanQC I: Peter Selinger Dalhousie University Media Attached

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 Heim Microsoft Media Attached
11:00 30m Talk		Invited Talk: Resource-Efficient Quantum Computing by Breaking Abstractions PLanQC I: Frederic T. Chong University of Chicago Media Attached File Attached
11:30 20m Talk		Tuning up entanglement through the cloud using Qiskit-OpenPulse PLanQC Thomas Alexander IBM T.J. Watson Research Center, New York, USA, Naoki Kanazawa IBM Research, Tokyo, Japan, Daniel Egger IBM Research, Zurich, Switzerland, Ali Javadi-Abhari IBM T.J. Watson Research Center, New York, USA, David C. McKay IBM T.J. Watson Research Center, New York, USA
11:50 20m Talk		Tracking Errors through Types in Quantum Programs PLanQC Kesha Hietala University of Maryland, Robert Rand University of Maryland, Michael Hicks University of Maryland Pre-print Media Attached File Attached
12:10 20m Talk		Quantum CPOs PLanQC Andre Kornell Tulane University, Bert Lindenhovius Tulane University, Michael Mislove Tulane

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

14:00 20m Talk		Runtime Analysis of Quantum Programs: A Formal Approach PLanQC Federico Olmedo University of Chile & IMFD Chile, Alejandro Díaz-Caro ICC (UBA-CONICET) & UNQ Pre-print File Attached
14:20 20m Talk		Qbricks: formal verification in quantum computing PLanQC Christopĥe Chareton CEA, LIST, France, Sébastien Bardin CEA LIST, François Bobot CEA, Valentin Perrelle CEA, LIST, France, Benoit Valiron LRI, CentraleSupelec, Univ. Paris Saclay File Attached
14:40 25m Talk		Merged Talk: A Verified Optimizer for Quantum Circuits & Verified Translation Between Low-Level Quantum Languages PLanQC Kesha Hietala University of Maryland, Kartik Singhal University of Chicago, Robert Rand University of Maryland, Shih-Han Hung University of Maryland, Xiaodi Wu University of Maryland, College Park, Michael Hicks University of Maryland Media Attached

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

15:35 20m Talk		Optimal Two-Qubit Circuits for Universal Fault-Tolerant Quantum Computation PLanQC Andrew N. Glaudell University of Maryland, Neil Julien Ross Dalhousie University, Jacob M. Taylor University of Maryland Pre-print Media Attached File Attached
15:55 20m Talk		Context-Sensitive and Duration-Aware Qubit Mapping for Various NISQ Devices PLanQC Yu Zhang University of Science and Technology of China, Haowei Deng University of Science and Technology of China, Quanxi Li University of Science and Technology of China Pre-print Media Attached
16:15 20m Talk		Quingo: A Domain Specific Language for Quantum Computing with NISQ Features PLanQC Xiang Fu Institute for Quantum Information & State Key Laboratory of High Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Jintao Yu State Key Laboratory of Mathematical Engineering and Advanced Computing, Zhengzhou, China, Xing Su College of Meteorology and Oceanography, National University of Defense Technology, Changsha, China, Hanru Jiang Center for Quantum Computing, Peng Cheng Laboratory, Shenzhen, China, Hua Wu Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China, Dong Chen Department of Computing Science, College of Computer, National University of Defense Technology, Changsha, China, Fucheng Cheng Center for Quantum Computing, Peng Cheng Laboratory, Shenzhen, China, Xi Deng Center for Quantum Computing, Peng Cheng Laboratory, Shenzhen, China, Jinrong Zhang Center for Quantum Computing, Peng Cheng Laboratory, Shenzhen, China, Lei Jin School of Information Engineering, Zhengzhou University, Zhengzhou, China, Yihang Yang School of Information Engineering, Zhengzhou University, Zhengzhou, China, Le Xu School of Information Engineering, Zhengzhou University, Zhengzhou, China, Chunchao Hu School of Information Engineering, Zhengzhou University, Zhengzhou, China, Anqi Huang Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Guangyao Huang Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Xiaogang Qiang Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Mingtang Deng Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Ping Xu Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Wanwei Liu National University of Defense Technology, Yuxin Deng East China Normal University, Junjie Wu Institute for Quantum Information & State Key Laboratory of High-Performance Computing, College of Computer, National University of Defense Technology, Changsha, China, Yuan Feng Centre for Quantum Software and Information, University of Technology Sydney, Australia File Attached

16:50 - 17:50	Quantum-Classical CommunicationPLanQC at Maurepas Chair(s): Michael Hicks University of Maryland

16:50 20m Talk		Extending Modern C++ for Heterogeneous Quantum-Classical Computing PLanQC Alexander McCaskey Oak Ridge National Laboratory, Tiffany Mintz Oak Ridge National Laboratory, Eugene Dumitrescu Oak Ridge National Laboratory, Sarah Powers Oak Ridge National Laboratory, Shirley Moore Oak Ridge National Laboratory, Pavel Lougovski Oak Ridge National Laboratory
17:10 20m Talk		Formalization of a Programming Language for Quantum Circuits with Measurement and Classical Control PLanQC Dongho LEE LRI / CEA LIST, Univ Paris Saclay, Sébastien Bardin CEA LIST, Valentin Perrelle CEA, LIST, France, Benoit Valiron LRI, CentraleSupelec, Univ. Paris Saclay File Attached
17:30 20m Talk		Automated distribution of quantum circuits via hypergraph partitioning PLanQC Pablo Andres-Martinez University of Edinburgh, Chris Heunen University of Edinburgh Link to publication DOI Pre-print Media Attached File Attached

Mon 20 Jan
Displayed time zone: Saskatchewan, Central America change

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

09:00 60m Talk		Invited talk: Matching Logic: The Foundation of the K Framework CPP Grigore Roşu University of Illinois at Urbana-Champaign, Xiaohong Chen University of Illinois at Urbana-Champaign DOI Media Attached

10:30 - 11:35	Program verificationCPP at Maurepas Chair(s): Nikhil Swamy Microsoft Research

10:30 21m Talk		A Verified Packrat Parser Interpreter for Parsing Expression Grammars CPP Clément Blaudeau Ecole Polytechnique, Natarajan Shankar SRI International, USA DOI Pre-print Media Attached
10:51 22m Talk		Proof Pearl: Braun Trees CPP Tobias Nipkow Technische Universität München, Thomas Sewell Chalmers University of Technology, Sweden DOI Pre-print Media Attached
11:13 22m Talk		FreeSpec: Specifying, Verifying and Executing Impure Computations in Coq CPP Thomas Letan ANSSI, Yann Régis-Gianas IRIF, University Paris Diderot and CNRS, France / INRIA PI.R2 DOI Pre-print Media Attached

11:45 - 12:30	Automated verification and SAT solvingCPP at Maurepas Chair(s): Ori Lahav Tel Aviv University

11:45 22m Talk		Verifying x86 Instruction Implementations CPP Shilpi Goel Centaur Technology, Inc., Anna Slobodova Centaur Technology, Inc., Rob Sumners Centaur Technology, Inc., Sol Swords Centaur Technology, Inc. DOI Pre-print File Attached
12:07 22m Talk		Frying the Egg, Roasting The Chicken: Unit Deletions in DRAT Proofs CPP Adrian Rebola Pardo TU Wien, Johannes Altmanninger TU Wien DOI Pre-print Media Attached

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

14:00 21m Talk		An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction CPP Yannick Zakowski University of Pennsylvania, Paul He University of Pennsylvania, Chung-Kil Hur Seoul National University, Steve Zdancewic University of Pennsylvania DOI Pre-print Media Attached File Attached
14:21 21m Talk		Exploration of Neural Machine Translation in Autoformalization of Mathematics in Mizar CPP Qingxiang Wang University of Innsbruck, Chad Brown Czech Technical University in Prague, Cezary Kaliszyk University of Innsbruck, Josef Urban Czech Technical University in Prague DOI Pre-print
14:43 21m Talk		REPLICA: REPL Instrumentation for Coq Analysis CPP Talia Ringer University of Washington, Alex Sanchez-Stern University of California, San Diego, Dan Grossman University of Washington, Sorin Lerner University of California, San Diego DOI Pre-print Media Attached

15:35 - 16:40	Decidability and complexityCPP at Maurepas Chair(s): Kathrin Stark Princeton University, USA

15:35 21m Talk		Verified Programming of Turing Machines in Coq CPP Yannick Forster Saarland University, Fabian Kunze Saarland University, Maximilian Wuttke Saarland University DOI Pre-print Media Attached
15:56 21m Talk		A Functional Proof Pearl: Inverting the Ackermann Hierarchy CPP Linh Tran National University of Singapore, Anshuman Mohan National University of Singapore, Aquinas Hobor National University of Singapore DOI Pre-print Media Attached
16:18 21m Talk		Undecidability of Higher-Order Unification Formalised in Coq CPP Simon Spies Saarland University, Yannick Forster Saarland University DOI Pre-print Media Attached

16:50 - 17:56	Homotopy Type Theory and PC chairs' reportCPP at Maurepas Chair(s): Floris van Doorn University of Pittsburgh

16:50 22m Talk		Cubical Synthetic Homotopy Theory CPP Anders Mörtberg Department of Mathematics, Stockholm University, Loïc Pujet Gallinette Project-Team, Inria DOI Pre-print Media Attached File Attached
17:12 22m Talk		Three equivalent ordinal notation systems in Cubical Agda CPP Fredrik Nordvall Forsberg University of Strathclyde, Chuangjie Xu Ludwig-Maximilians-Universität München, Neil Ghani University of Strathclyde DOI Pre-print Media Attached File Attached
17:34 22m Talk		PC Chairs' report CPP Jasmin Blanchette Vrije Universiteit Amsterdam, Cătălin Hriţcu Inria Paris DOI Media Attached File Attached

Tue 21 Jan
Displayed time zone: Saskatchewan, Central America change

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

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

10:30 - 11:35	Mechanized metatheoryCPP at Maurepas Chair(s): Benjamin C. Pierce University of Pennsylvania

10:30 21m Talk		Coq à la Carte - A Practical Approach to Modular Syntax with Binders CPP Yannick Forster Saarland University, Kathrin Stark Princeton University, USA DOI Pre-print Media Attached
10:51 21m Talk		A Mechanized Formalization of GraphQL CPP Tomás Díaz IMFD Chile, Federico Olmedo University of Chile & IMFD Chile, Éric Tanter University of Chile DOI Pre-print Media Attached File Attached
11:13 21m Talk		ConCert: A Smart Contract Certification Framework in Coq CPP Danil Annenkov Concordium Blockchain Research Center, Aarhus University, Jakob Botsch Nielsen Concordium Blockchain Research Center, Aarhus University, Bas Spitters Concordium Blockchain Research Center, Aarhus University DOI Pre-print Media Attached File Attached

11:45 - 12:30	Verified cryptographyCPP at Maurepas Chair(s): Adam Chlipala Massachusetts Institute of Technology

11:45 22m Talk		Formalising Oblivious Transfer in the Semi-Honest and Malicious Model in CryptHOL CPP David Butler Alan Turing Institute, David Aspinall University of Edinburgh, Adria Gascon Alan Turing Institute DOI Pre-print Media Attached
12:07 22m Talk		Verified Security of BLT Signature Scheme CPP Denis Firsov Guardtime AS, Ahto Buldas Tallinn University of Technology, Ahto Truu Guardtime AS, Risto Laanoja Guardtime AS DOI Pre-print Media Attached File Attached

14:00 - 15:05	Concurrency and linearityCPP at Maurepas Chair(s): Zhong Shao Yale University

14:00 21m Talk		Formalizing Determinacy of Concurrent Revisions CPP Roy Overbeek Vrije Universiteit Amsterdam DOI Pre-print Media Attached
14:21 21m Talk		Formalizing π-calculus in Guarded Cubical Agda CPP Niccolò Veltri Tallinn University of Technology, Andrea Vezzosi IT University Copenhagen DOI Pre-print Media Attached File Attached
14:43 21m Talk		Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages CPP Arjen Rouvoet Delft University of Technology, Casper Bach Poulsen Delft University of Technology, Robbert Krebbers Delft University of Technology, Eelco Visser Delft University of Technology DOI Pre-print Media Attached File Attached

15:35 - 16:40	Formalized mathematics 1CPP at Maurepas Chair(s): Robert Y. Lewis Vrije Universiteit Amsterdam

15:35 21m Talk		Formalising perfectoid spaces CPP Patrick Massot Université Paris Sud, Kevin Buzzard Imperial College London, Johan Commelin Universität Freiburg DOI Pre-print Media Attached File Attached
15:56 21m Talk		A Constructive Formalization of the Weak Perfect Graph Theorem CPP Abhishek Kr Singh Tata Institute of Fundamental Research Mumbai, Raja Natarajan Tata Institute of Fundamental Research Mumbai DOI Pre-print Media Attached File Attached
16:18 21m Talk		Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq CPP Christian Doczkal Université Côte d'Azur, Damien Pous CNRS, ENS Lyon DOI Pre-print Media Attached

16:50 - 17:56	Formalized mathematics 2CPP at Maurepas Chair(s): Tobias Nipkow Technische Universität München

16:50 22m Talk		The Poincaré-Bendixson Theorem in Isabelle/HOL CPP Fabian Immler Carnegie Mellon University, Yong Kiam Tan Carnegie 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 Han University of Pittsburgh, Floris van Doorn University 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

Sat 25 Jan
Displayed time zone: Saskatchewan, Central America change

09:00 - 10:00	Invited TalkCoqPL at Maurepas Chair(s): Robbert Krebbers Delft University of Technology

09:00 60m Talk		SMTCoq: Safe and efficient automation in Coq (Keynote) CoqPL Chantal Keller LRI, Université Paris-Sud File Attached

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

10:30 30m Talk		Deriving Instances with Dependent Types CoqPL Arthur Azevedo de Amorim Carnegie Mellon University, USA File Attached
11:00 30m Talk		The use of Coq for Common Criteria Evaluations CoqPL Yves Bertot INRIA, Maxime Dénès Inria, Vincent Laporte Inria, Arnaud Fontaine ANSSI, Thomas Letan ANSSI File Attached
11:30 30m Talk		Verifying concurrent Go code in Coq with Goose CoqPL Tej Chajed Massachusetts Institute of Technology, USA, Joseph Tassarotti Boston College, M. Frans Kaashoek Massachusetts Institute of Technology, USA, Nickolai Zeldovich Massachusetts Institute of Technology, USA Link to publication File Attached
12:00 30m Talk		A Tutorial on Equations CoqPL Matthieu Sozeau Inria Media Attached File Attached

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

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

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

15:35 30m Talk		Towards Formally Verified Just-in-Time compilation CoqPL Aurèle Barrière Univ Rennes, IRISA, Sandrine Blazy Univ Rennes- IRISA, David Pichardie Univ Rennes, ENS Rennes, IRISA File Attached
16:05 30m Talk		A Coq Library of Undecidable Problems CoqPL Yannick Forster Saarland University, Dominique Larchey-Wendling CNRS, LORIA, Andrej Dudenhefner Saarland University, Edith Heiter Saarland University, Dominik Kirst Saarland University, Fabian Kunze Saarland University, Gert Smolka Saarland University, Simon Spies Saarland University, Dominik Wehr Saarland University, Universiteit van Amsterdam, Maximilian Wuttke Saarland University Media Attached File Attached
16:35 15m Break		Short break CoqPL
16:50 45m Demonstration		Session with the Coq Development Team CoqPL Maxime Dénès Inria, Matthieu Sozeau Inria

Sun 19 Jan
Displayed 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
Maurepas	PLanQC Introduction and Invited Talks																		PLanQC Invited Talks, Pulses, Errors and Categories																																										PLanQC Formal Methods																			PLanQC NISQ															PLanQC Quantum-Classical Communication

Mon 20 Jan
Displayed 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
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

Tue 21 Jan
Displayed 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
Maurepas	CPP Invited talk																		CPP Mechanized metatheory															CPP Verified cryptography																											CPP Concurrency and linearity																			CPP Formalized mathematics 1															CPP Formalized mathematics 2

Sat 25 Jan
Displayed 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
Maurepas	CoqPL Invited Talk																		CoqPL Contributed Talks																																										CoqPL Invited Talk																			CoqPL Contributed Talks & Coq Developers

Sun 19 Jan
Displayed 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
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

Mon 20 Jan
Displayed 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
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

Tue 21 Jan
Displayed 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
Maurepas	CPP Invited talk: Proof Assistants at the Hardware-Software Interface 09:00 - 10:00																		CPP Coq à la Carte - A Practical Approach to Modular Syntax with Binders 10:30 - 10:51				CPP A Mechanized Formalization of GraphQL 10:51 - 11:13					CPP ConCert: A Smart Contract Certification Framework in Coq 11:13 - 11:35						CPP Formalising Oblivious Transfer in the Semi-Honest and Malicious Model i ... 11:45 - 12:07				CPP Verified Security of BLT Signature Scheme 12:07 - 12:30																							CPP Formalizing Determinacy of Concurrent Revisions 14:00 - 14:21				CPP Formalizing π-calculus in Guarded Cubical Agda 14:21 - 14:43					CPP Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed ... 14:43 - 15:05										CPP Formalising perfectoid spaces 15:35 - 15:56				CPP A Constructive Formalization of the Weak Perfect Graph Theorem 15:56 - 16:18					CPP Completeness of an Axiomatization of Graph Isomorphism via Graph Rewrit ... 16:18 - 16:40						CPP The Poincaré-Bendixson Theorem in Isabelle/HOL 16:50 - 17:12				CPP A Formal Proof of the Independence of the Continuum Hypothesis 17:12 - 17:34					CPP The Lean mathematical library 17:34 - 17:56

Sat 25 Jan
Displayed 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
Maurepas	CoqPL SMTCoq: Safe and efficient automation in Coq (Keynote) 09:00 - 10:00																		CoqPL Deriving Instances with Dependent Types 10:30 - 11:00						CoqPL The use of Coq for Common Criteria Evaluations 11:00 - 11:30						CoqPL Verifying concurrent Go code in Coq with Goose 11:30 - 12:00						CoqPL A Tutorial on Equations 12:00 - 12:30																								CoqPL Autosubst 2: Mechanising binders in Coq (Keynote) 14:00 - 15:00																			CoqPL Towards Formally Verified Just-in-Time compilation 15:35 - 16:05						CoqPL A Coq Library of Undecidable Problems 16:05 - 16:35						CoqPL Short break 16:35 - 16:50			CoqPL Session with the Coq Development Team 16:50 - 17:35

Room information: Maurepas

Sun 19 Jan
Displayed time zone: Saskatchewan, Central America change

Mon 20 Jan
Displayed time zone: Saskatchewan, Central America change

Tue 21 Jan
Displayed time zone: Saskatchewan, Central America change

Sat 25 Jan
Displayed time zone: Saskatchewan, Central America change

Sun 19 Jan
Displayed time zone: Saskatchewan, Central America change

PLanQC

PLanQC

PLanQC

PLanQC

PLanQC

Mon 20 Jan
Displayed time zone: Saskatchewan, Central America change

CPP

CPP

CPP

CPP

CPP

CPP

Tue 21 Jan
Displayed time zone: Saskatchewan, Central America change

CPP

CPP

CPP

CPP

CPP

CPP

Sat 25 Jan
Displayed time zone: Saskatchewan, Central America change

CoqPL

CoqPL

CoqPL

CoqPL

Sun 19 Jan
Displayed time zone: Saskatchewan, Central America change

Mon 20 Jan
Displayed time zone: Saskatchewan, Central America change

Tue 21 Jan
Displayed time zone: Saskatchewan, Central America change

Sat 25 Jan
Displayed time zone: Saskatchewan, Central America change

Tracks

Room information: Maurepas

Program Display Configuration

Sun 19 JanDisplayed time zone: Saskatchewan, Central America change

Mon 20 JanDisplayed time zone: Saskatchewan, Central America change

Tue 21 JanDisplayed time zone: Saskatchewan, Central America change

Sat 25 JanDisplayed time zone: Saskatchewan, Central America change

Sun 19 JanDisplayed time zone: Saskatchewan, Central America change

PLanQC

PLanQC

PLanQC

PLanQC

PLanQC

Mon 20 JanDisplayed time zone: Saskatchewan, Central America change

CPP

CPP

CPP

CPP

CPP

CPP

Tue 21 JanDisplayed time zone: Saskatchewan, Central America change

CPP

CPP

CPP

CPP

CPP

CPP

Sat 25 JanDisplayed time zone: Saskatchewan, Central America change

CoqPL

CoqPL

CoqPL

CoqPL

Sun 19 JanDisplayed time zone: Saskatchewan, Central America change

Mon 20 JanDisplayed time zone: Saskatchewan, Central America change

Tue 21 JanDisplayed time zone: Saskatchewan, Central America change

Sat 25 JanDisplayed time zone: Saskatchewan, Central America change

Sun 19 Jan
Displayed time zone: Saskatchewan, Central America change

Mon 20 Jan
Displayed time zone: Saskatchewan, Central America change

Tue 21 Jan
Displayed time zone: Saskatchewan, Central America change

Sat 25 Jan
Displayed time zone: Saskatchewan, Central America change

Sun 19 Jan
Displayed time zone: Saskatchewan, Central America change

Mon 20 Jan
Displayed time zone: Saskatchewan, Central America change

Tue 21 Jan
Displayed time zone: Saskatchewan, Central America change

Sat 25 Jan
Displayed time zone: Saskatchewan, Central America change

Sun 19 Jan
Displayed time zone: Saskatchewan, Central America change

Mon 20 Jan
Displayed time zone: Saskatchewan, Central America change

Tue 21 Jan
Displayed time zone: Saskatchewan, Central America change

Sat 25 Jan
Displayed time zone: Saskatchewan, Central America change