Write a Blog >>
VenueJW Marriott New Orleans
Room nameMaurepas
Floor3
Room InformationNo extra information available
Program

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

Conference Day
Sun 19 Jan

Displayed time zone: Saskatchewan, Central America change

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: Frederic T. 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
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
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
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

Conference Day
Mon 20 Jan

Displayed time zone: Saskatchewan, Central America change

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
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
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
DOI Pre-print Media Attached
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
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
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

Conference Day
Tue 21 Jan

Displayed time zone: Saskatchewan, Central America change

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
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
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
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
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
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
DOI Pre-print Media Attached File Attached

Conference Day
Sat 25 Jan

Displayed 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
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
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
Media Attached File Attached
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
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

Conference Day
Sun 19 Jan

Displayed time zone: Saskatchewan, Central America change

Conference Day
Mon 20 Jan

Displayed time zone: Saskatchewan, Central America change

Conference Day
Tue 21 Jan

Displayed time zone: Saskatchewan, Central America change

Conference Day
Sat 25 Jan

Displayed time zone: Saskatchewan, Central America change

Conference Day
Sat 25 Jan

Displayed time zone: Saskatchewan, Central America change