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)