Demo Data from EDBT 2026 / reviewers in the wild / expert
RanDair Porter
dblp:276/0022
· DBLP profile ↗
1ranked-venue papers
0as first author
1since 2021 · last 2021
—ORCID · none
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 1 · 1 since 2021
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Software engineering, system software, and programming languages
1 paper |
Program verification · 50% Programming languages and type systems · 50% |
Topics — the 2 heaviest of 2, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Program verification › proof assistants
proof repair |
0.5 | 1 | 2021 | Proof repair across type equivalences · PLDI 2021 |
Programming languages and type systems › type checking
type equivalence |
0.5 | 1 | 2021 | Proof repair across type equivalences · PLDI 2021 |
Methods — techniques the papers use, named apart from their topics
proof term transformation · 0.5decompilation to tactic scripts · 0.5
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2021 | Proof repair across type equivalencesabstractWe describe a new approach to automatically repairing broken proofs in the Coq proof assistant in response to changes in types. Our approach combines a configurable proof term transformation with a decompiler from proof terms to suggested tactic scripts. The proof term transformation implements transport across equivalences in a way that removes references to the old version of the changed type and does not rely on axioms beyond those Coq assumes. Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, Dan Grossman |
PLDI | 2 |