Write a Blog >>
POPL 2020
Sun 19 - Sat 25 January 2020
New Orleans, Louisiana, United States
Toggle navigation
Attending
Venue: JW Marriott New Orleans
Restaurant: Palace Cafe
Registration
Online Participation
Travel to the USA
Mentoring Events
Information for Students
Code of Conduct
Supporting POPL
Accessibility
SIGPLAN CARES
Program
POPL Program
Your Program
Filter by Day
Sun 19 Jan
Mon 20 Jan
Tue 21 Jan
Wed 22 Jan
Thu 23 Jan
Fri 24 Jan
Sat 25 Jan
Tracks
POPL 2020
Research Papers
Artifact Evaluation
Student Research Competition
Workshops and Co-located Events
TutorialFest
POPLmark 15 Year Retrospective Panel
Ally Skills Session
LGBTQ Lunch
Mentoring Breakfasts
W@POPL Dinner
Student Volunteers
Co-hosted Conferences
CPP
VMCAI
Workshops
ADSL
CoqPL
HASE
LAFI
(né PPS)
PEPM
PLMW
PLanQC
PriSC
PriSC
Principles of Secure Compilation
- Lucet: A Compiler and Runtime for High-Concurrency Low-Latency Sandboxing
WGT
Co-hosted Symposia
PADL
Organization
POPL 2020 Committees
Organizing Committee
Steering Committee
Track Committees
Research Papers
Artifact Evaluation
Student Research Competition
TutorialFest
POPLmark 15 Year Retrospective Panel
Panel
Organizing Committee
Ally Skills Session
LGBTQ Lunch
Mentoring Breakfasts
W@POPL Dinner
Student Volunteers
Contributors
People Index
Co-hosted Conferences
CPP
Program Committee
VMCAI
Invited Speakers
Organizing Committee
Program Committee
Artifact-Evaluation Committee
Steering Committee
Workshops
ADSL
Organizing Committee
Program Committee
CoqPL
Invited speakers
Organizing Committee
Program Committee
HASE
Organizing Committee
Program Committee
LAFI
Program Committee
Steering Committee
PEPM
PC Chairs
Program Committee
PLMW
Organizing Committee
Invited speakers
Panelists
PLanQC
Organizing Committee
Program Committee
PriSC
Program Committee
Steering Committee
WGT
Organizing Committee
Program Committee
Co-hosted Symposia
PADL
Program Chairs
Program Committee
Publicity Chair
Search
Series
Series
POPL 2025
POPL 2024
POPL 2023
POPL 2022
POPL 2021
POPL 2020
POPL 2019
POPL 2018
POPL 2017
POPL 2016
Sign in
Sign up
POPL 2020
(
series
) /
JW Marriott New Orleans
/
Room information: Maurepas
Venue
JW Marriott New Orleans
Room name
Maurepas
Floor
3
Room Information
No extra information available
Program
Detailed Table
Session Timeline
Detailed Timeline
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT-06:00) Saskatchewan, Central America
.
Use conference time zone: (GMT-06:00) Saskatchewan, Central America
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-10:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-09:00) Alaska
(GMT-08:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-08:00) Pacific Time (US & Canada)
(GMT-07:00) Mountain Time (US & Canada)
(GMT-07:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-05:00) Easter Island
(GMT-06:00) Central Time (US & Canada)
(GMT-05:00) Eastern Time (US & Canada)
(GMT-05:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-03:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-04:00) Atlantic Time (Goose Bay)
(GMT-04:00) Atlantic Time (Canada)
(GMT-03:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-03:00) Miquelon, St. Pierre
(GMT-03:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-03:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT-01:00) Azores
(UTC) Coordinated Universal Time
(GMT) Belfast
(GMT) Dublin
(GMT) Lisbon
(GMT) London
(GMT) Monrovia, Reykjavik
(GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+01:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+01:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+02:00) Athens
(GMT+02:00) Beirut
(GMT+02:00) Cairo
(GMT+02:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+02:00) Jerusalem
(GMT+03:00) Minsk
(GMT+02:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+03:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+10:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+11:00) Hobart
(GMT+10:00) Vladivostok
(GMT+11:00) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+12:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+13:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+13:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
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 program
Specify 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 Talks
PLanQC
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 Categories
PLanQC
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 Methods
PLanQC
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
NISQ
PLanQC
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 Communication
PLanQC
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 talk
CPP
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 verification
CPP
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 solving
CPP
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 interaction
CPP
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 complexity
CPP
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' report
CPP
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 talk
CPP
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 metatheory
CPP
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 cryptography
CPP
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 linearity
CPP
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 1
CPP
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 2
CPP
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 Talk
CoqPL
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 Talks
CoqPL
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 Talk
CoqPL
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 Developers
CoqPL
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
x
Mon 9 Dec 05:55