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

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
Clement 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
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
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
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
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

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