| CS-2023-01 | ||||
|---|---|---|---|---|
| Title | Extensible Metatheory Mechanization via Family Polymorphism: Technical Report | |||
| Authors | Ende Jin, Nada Amin, Yizhou Zhang | |||
| Abstract |
With
the
growing
practice
of
mechanizing
language
metatheories,
it
has
become
ever
more
pressing
that
interactive
theorem
provers
make
it
easy
to
write
reusable,
extensible
code
and
proofs.
This
paper
presents
a
novel
language
design
geared
towards
extensible
metatheory
mechanization
in
a
proof
assistant.
The
new
design
achieves
reuse
and
extensibility
via
a
form
of
family
polymorphism,
an
object-oriented
idea,
that
allows
code
and
proofs
to
be
polymorphic
to
their
enclosing
families.
Our
development
addresses
technical
challenges
that
arise
from
the
underlying
language
of
a
proof
assistant
being
simultaneously
functional,
dependently
typed,
a
logic,
and
an
interactive
tool.
Our
results
include
(1)
a
prototypical
implementation
of
the
language
design
as
a
Coq
plugin,
(2)
a
dependent
type
theory
capturing
the
essence
of
the
language
mechanism
and
its
consistency
and
canonicity
results,
and
(3)
case
studies
showing
how
the
new
expressiveness
naturally
addresses
real
programming
challenges
in
metatheory
mechanization. This technical report is the extended version of a paper published at PLDI 2023 [Jin et al. 2023a] | |||
| Date | April 18, 2023 | |||
| Report | CS-2023-01 (746K PDF) | |||
| CS-2023-02 | ||||
| Title | Order of Approximation and Some Tests of a Functional Variation of a Blending Surface Scheme for Scattered Data Interpolation | |||
| Author | Stephen Mann | |||
| Abstract | This technical report describes an implementation and tests of a blending scheme for scattered data inter- polation, and in particular studies order of approximation for the method. This particular implementation is a special case of an earlier scheme by Fang for fitting a parametric surface to interpolate the vertices of a closed polyhedron with n-sided faces, where a surface patch is constructed for each face of the polyhedron, and neighbouring faces can meet with a user specified order of continuity. The specialization described in this technical report considers functions of the form z = f(x,y). This restriction allows for investigation of order of approximation, as well as easier tests of higher order continuity between patches (with G3 continuity being empirically verified in this report). Further, it is shown that the functional version of Fang’s scheme has polynomial precision. Some details on the implementation are provided to assist others who wish to implement Fang’s method. | |||
| Date | August 3, 2023 | |||
| Report | CS-2023-02 (24 MB PDF) | |||