Parinati is a tool that realizes logic programming search for the Logical Framework (LF) via translation of LF specifications to the higher order logic programming language λProlog. Parinati translates Twelf specifications to compilable λProlog modules, against which queries for discovering inhabitants for particular LF types may be run using the Teyjus implementation of λProlog. Learn more aboute Parinati in A Meta-Programming Approach to Realizing Dependently Typed Logic Programming, by Snow, Baelde, and Nadathur (submitted paper).
Parinati includes several example specifications, along with benchmarks for comparing the efficiency of logic programming search in LF via translation to λProlog with existing implementations like that of Twelf.
Partial funding for this work was provided by the National Science Foundation through the grants CCR-0429572 and CCF-0917140. Opinions, findings, and conclusions or recommendations expressed in this work are those of the authors and do not necessarily reflect the views of the National Science Foundation or the other funding sources.