Twelf logic / Logics via Twelf

Reported by till and assigned to till Migrated from http://trac.informatik.uni-bremen.de:8080/hets/ticket/356

Build a connection to Twelf:

Haskell datatype for Twelf signatures / theories (synchronized with Scala datatypes)
Twelf-Syntax -- Twelf --> OMDoc -- Hets/Omdoc --> XML-Datatype -- translation function --> Twelf datatype
Twelf-datatype -- translation function --> XML-Datatype -- Hets/Omdoc --> OMDoc --> Twelf
Integrate Twelf as a tool for parsing, typchecking and proof checking
Design datastructure for signature morphisms
Parsing and checking of symbol maps via Twelf/OMDoc
Implement translation of terms along signature morphisms
Derived signature morphisms in Hets?
Proof trees are just Twelf terms (via Curry Howard)
Twelf theories lead to new logic instances in Hets, inherting most stuff from the Twelf logic
Twelf theory morphisms lead to new logic comorphisms
Translations from existing Hets logics to their Twelf counterparts
translate SPASS proofs to ND proofs, or better, use MathServe's transformation to ND
pretty printing for ND proofs
FFI between Haskell and Scala/Java?

spechub / Hets