Parinati:
A meta-programming approach to implementing logic programming search in LF.

Overview

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).

Examples and Benchmarks

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.

Source Code

Parinati was written in OCaml by Zach Snow. You can download the latest version of Parinati's source code, which includes the translator, (some) documentation, examples, and benchmarks. Parinati is released under the GPL version 3.

Acknowledgements

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.