Recent master’s graduate Ende Jin, his advisor Professor Yizhou Zhang, and their Harvard colleague Professor Nada Amin have received a Distinguished Paper Award at PLDI 2023, the 44th ACM SIGPLAN Conference on Programming Language Design and Implementation. Their paper, “Extensible Metatheory Mechanization via Family Polymorphism,” was presented at the premier forum for programming languages and programming systems research, held this year from June 17 to 21 in Orlando, Florida.
Only about one in ten accepted submissions at PLDI are designated as distinguished papers, an award conferred to highlight research that the PLDI review committee believes should be read by a broad audience because of its relevance, originality, significance, and clarity.
“Congratulations to Ende, Yizhou, and their colleague Nada Amin on receiving a Distinguished Paper Award,” said Raouf Boutaba, Professor and Director of the Cheriton School of Computer Science. “This research was the basis of Ende’s master’s thesis work in which he showed how family polymorphism — an object-oriented idea — leads to a new programming language for engineering extensible, reusable mathematical proofs.”
L
to
R:
Ende
Jin
and
Cheriton
School
of
Computer
Science
Professor
Yizhou
Zhang.
Nada
Amin,
a
professor
at
Harvard’s
School
of
Engineering
and
Applied
Sciences,
is
shown
inset.
Ende
Jin
graduated
in
June
2023
from
the
Cheriton
School
of
Computer
Science
with
a
master’s
degree
during
which
he
developed
a
novel
programming
language
for
engineering
extensible,
reusable
machine-checked
proofs.
Professor
Zhang
is
a
member
of
the
programming
languages
research
group.
His
research
is
on
the
design
and
implementation
of
programming
languages.
More about this award-winning research
Computer scientists often want to prove that programming languages and computer systems enjoy certain nice properties, and they have increasingly been doing so using proof assistants — software tools that help programmers develop machine-checkable proofs with mathematical certainty. This practice, however, is also difficult and costly. In particular, it highlights a long-standing challenge known as the expression problem, a programming challenge that embodies the difficulty of writing type-safe, extensible code. To define an expression language that can be reused for future extensions, programmers face a fundamental tension between adding new constructors to a data type and adding new functions over the data type.
The expression problem is well studied for ordinary object-oriented and functional programming languages. Modern languages, such as Scala, have many linguistic features that offer expressive power to solve the expression problem. Proof assistants, in contrast, have few linguistic solutions to the expression problem, even though the challenge of writing extensible, type-safe code is as real for proof assistants as it is for any other language. Metatheory mechanization is a perfect example of the difficulty encountered. Programmers face a tension between adding new constructors to an inductive type and adding new functions and theorems over the inductive type.
In the Coq proof assistant, for instance, inductive types, as well as functions and theorems over inductive types, are closed to extension. To reuse mechanized metatheories, a common practice is to copy code and proofs, then modify both in each extension. But having to maintain multiple copies is antithetical to good software engineering. A programmer could turn to design patterns for structuring developments and to tool support to reduce boilerplate, but these solutions tend to require heavy lifting from the programmer to make code extensible and often lead to non-idiomatic programming styles.
Ende Jin, and Professors Yizhou Zhang and Nada Amin set out to answer whether an extensible metatheory mechanization can be made easier by having a proof assistant support new linguistic features that address the expression problem. To this end, they contributed a new programming language that integrates family polymorphism into a proof assistant. Because code and proofs are polymorphic to a family they are nested within, and they can be inherited and reused by a derived family. Family polymorphism, therefore, allows for extensible metatheory mechanization.
Integrating family polymorphism into a dependent type theory for logical reasoning, however, poses significant technical challenges. Pillars of dependent type theories — including inductive types, definitional equality, and logical consistency — are all inimical to the kind of extensibility enabled by existing object-oriented designs for family polymorphism. Their contributions, therefore, include novel design recipes and implementation techniques to deal with these challenges as well as foundational guarantees on the underlying logic and programming language.
Specifically, they make the following contributions.
- They present a language design that enables extensible metatheory mechanization in a higher- order, dependent type theory with inductive types. The language design reconciles the expressiveness enabled by family polymorphism with the rigour of a proof assistant, while largely retaining an idiomatic programming style.
- They contribute a prototypical implementation of their language mechanism as a Coq plugin. The plugin works by compiling surface-language definitions into Coq modules parameterized by explicit extensibility hooks.
- They capture the essence of the new language mechanism formally by extending Martin-Löf type theory with facilities to express family polymorphism. They prove foundational metatheoretical results including consistency and canonicity.
- They present case studies of using their Coq plugin to mechanize language metatheories. They show how their language design naturally solves the expression problem and enables a good amount of reuse and extensibility for mechanizing proofs.