Sat 22 Jun 2019 11:30 - 12:00 at 106B - Compiler Verification Chair(s): Zhong Shao
For families of related software programs, it can be convenient to
implement libraries of generic algorithms, which can be proved
once; and then specialize those algorithms to parameters and
optimize the new less-general programs.  If the latter process is
also verified, we have an appealing recipe for churning out
verified code quickly.  One use case that the MIT subteam works on
is generating low-level code for cryptographic primitives, which
are often parameterized on large prime numbers.  Our original
approach to partial evaluation (a term of art for compile-time
optimization of function specializations) was to use Coq's
built-in term reduction.  However, we do not want full reduction
to normal forms, since variables standing for runtime inputs
remain in the output; and telling Coq about a customized reduction
strategy is too difficult, when we don't want to wait for hours or
more for a reduction to finish, as we encountered for quite a few
parameter sets.  I will explain the alternative strategy we have
developed, which is essentially a new low-trusted-code-base
approach to fast, customized reduction and rewriting in Coq,
combining the ideas of proof by reflection, parametric
higher-order abstract syntax, normalization by evaluation, and
efficient compilation of pattern matches.

Sat 22 Jun
Times are displayed in time zone: Tijuana, Baja California change

11:00 - 12:30: Compiler VerificationDeepSpec at 106B
Chair(s): Zhong ShaoYale University
11:00 - 11:30
Talk
DeepSpec
Zoe ParaskevopoulouPrinceton University, Andrew AppelPrinceton
11:30 - 12:00
Talk
DeepSpec
Adam ChlipalaMassachusetts Institute of Technology, USA
12:00 - 12:30
Talk
DeepSpec
Yuting WangYale University