- About
- Events
- Calendar
- Graduation Information
- Cornell Tech Colloquium
- Student Colloquium
- BOOM
- Spring 2024 Colloquium
- Conway-Walker Lecture Series
- Salton 2023 Lecture Series
- Seminars / Lectures
- Big Red Hacks
- Cornell University - High School Programming Contests 2024
- Game Design Initiative
- CSMore: The Rising Sophomore Summer Program in Computer Science
- Explore CS Research
- ACSU Research Night
- Cornell Junior Theorists' Workshop 2024
- People
- Courses
- Research
- Undergraduate
- M Eng
- MS
- PhD
- Admissions
- Current Students
- Computer Science Graduate Office Hours
- Business Card Policy
- Cornell Tech
- Curricular Practical Training
- Exam Scheduling Guidelines
- Fellowship Opportunities
- Field of Computer Science Ph.D. Student Handbook
- Graduate TA Handbook
- Field A Exam Summary Form
- Graduate School Forms
- Instructor / TA Application
- Ph.D. Requirements
- Ph.D. Student Financial Support
- Special Committee Selection
- Travel Funding Opportunities
- Travel Reimbursement Guide
- The Outside Minor Requirement
- Diversity and Inclusion
- Graduation Information
- CS Graduate Minor
- Outreach Opportunities
- Parental Accommodation Policy
- Special Masters
- Student Spotlights
- Contact PhD Office
Speaker
Thursday, October 19, 2023 - 11:45 to 12:45
G01 Gates Hall and via Zoom https://cornell.zoom.us/j/97728839889?pwd=UEwwS0o1Ym9ROGttWCtJbFBmalVpdz09&from=addon
Host:
Dexter Kozen
Abstract:
Quantum algorithms can solve some problems exponentially faster than classical algorithms and the quantum computers that can run them are rapidly getting better. However, implementing a quantum algorithm on a quantum computer is a difficult task that could use some tool support. Such tools are emerging and more are needed, particularly for optimization and verification of quantum programs. The challenge is to design tools that run in polynomial time, which is in contrast to simulation which takes exponential time, in general. I will present approaches to the optimization and verification of quantum programs that scale to large programs. Our optimizer uses an automatically generated set of local rules and is competitive with the state of the art. Our verifier uses abstract interpretation with an abstract domain of polynomial size and is the first that can verify certain assertions automatically. My presentation is based on papers in PLDI 2021 and PLDI 2022.
Bio:
Jens Palsberg is a Professor and former Department Chair of Computer Science at the University of California, Los Angeles (UCLA). His research interests span the areas of programming languages, software engineering, and quantum computing. He is the director of the UCLA-Amazon Science Hub for Humanity and Artificial Intelligence, an associate editor of ACM Transactions on Quantum Computing, and a member of the ACM Executive Committee. In 2012 he received the ACM SIGPLAN Distinguished Service Award, and in 2023 he received the Eon Instrumentation Excellence in Teaching Award at UCLA for his courses on quantum computing.