This page provides access to some of the systems and ideas emanating from the work done under the Sparrow project. This project has been concerned broadly with developing mechanisms for formally encoding computational systems that are described via syntax-directed, rule-based, relational specifications and for reasoning about these systems through such encodings. The work under the project has spanned foundational studies aimed at designing suitable logics and related formalisms that can sustain the goals of specification and reasoning, the implementation of these formalisms to support applications and the experimentation with actual applications. A key aspect of the project has been its focus on formalisms and reasoning systems that incorporate a higher-order approach to representing syntactic structure. This kind of representation is especially well-suited to representing and manipulating objects such as types, formulas, programs and proofs whose whose analyses require dealing with binding notions in a fundamental way.
More detailed information about the different strands of the work comprising the project can found with the systems that have resulted from it and the applications that have been explored. Links to these are provided below:
Work on the varied components of this project that are described on this page has been supported by the National Science Foundation under Grant No CCF-0917140 and Grant No. CCF-1617771. Additional sources of support for each specific aspect of the work are indicated on the pages pertaining to them. Any opinions, findings and conclusions or recommendations expressed in the material on this page are those of the project participants and do not necessarily reflect the views of the National Science Foundation.
The views and opinions expressed in this page are strictly those of the page author(s). The contents of this page have not been reviewed or approved by the University of Minnesota.