Steve Zdancewic

QWIRE Practice: Formal Verification of Quantum Circuits in Coq

2018 · Electronic Proceedings in Theoretical Computer Science

We describe an embedding of the QWIRE quantum circuit language in the Coq proof assistant. This allows programmers to write quantum circuits using high-level abstractions and to prove properties of those circuits using Coq's theorem …

An equational theory for weak bisimulation via generalized parameterized coinduction

2020

Coinductive reasoning about infinitary structures such as streams is widely applicable. However, practical frameworks for developing coinductive proofs and finding reasoning principles that help structure such proofs remain a challenge, especially in the context of …

Modular, compositional, and executable formal semantics for LLVM IR

2021 · Proceedings of the ACM on Programming Languages

This paper presents a novel formal semantics, mechanized in Coq, for a large, sequential subset of the LLVM IR. In contrast to previous approaches, which use relationally-specified operational semantics, this new semantics is based on …

Counterfactual Explanations for Natural Language Interfaces

2022 · arXiv (Cornell University)

A key challenge facing natural language interfaces is enabling users to understand the capabilities of the underlying system. We propose a novel approach for generating explanations of a natural language interface based on semantic parsing. …