System description: twelf-a meta-logical framework for deductive systems

摘要

Twelf is a meta-logical framework for the specification, implementation, and meta-theory of deductive systems from the theory of programming languages and logics. It relies on the LF type theory and the judgments-as-types methodology for specification [HHP93], a con-straint logic programming interpreter for implementation [Pfe91], and the meta-logic M_2 for reasoning about object languages encoded in LF [SP98]. It is a significant extension and complete reimplementation of the Elf system [Pfe94].