Person. Nathaniel Yazdani

Papers

Proof repair across type equivalences ringer-2021-proof

PDF · DOI · pldb

Ornaments for Proof Reuse in Coq ringer-2019-ornaments

Ornaments express relations between inductive types with the same inductive structure. We implement fully automatic proof reuse for a particular class of ornaments in a Coq plugin, and show how such a tool can give programmers the rewards of using indexed inductive types while automating away many of the costs. The plugin works directly on Coq code; it is the first ornamentation tool for a non-embedded dependently typed language. It is also the first tool to automatically identify ornaments: To lift a function or proof, the user must provide only the source type, the destination type, and the source function or proof. In taking advantage of the mathematical properties of ornaments, our approach produces faster functions and smaller terms than a more general approach to proof reuse in Coq.
DOI

Adapting proof automation to adapt proofs ringer-2018-adapting

PDF · DOI · pldb
nathanielyazdani person entries/rolodex/nathanielyazdani.hel