System Description: Twelf - A Meta-Logical Framework for Deductive Systems

Abstract. 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 constraint logic programming interpreter for implementation [Pfe91], and the meta-logic M2 for reasoning about object languages encoded in LF [SP98]. It is a significant extension and complete reimplementation of the Elf system [Pfe94]. Twelf is written in Standard ML and runs under SML of New Jersey and MLWorks on Unix and Window platforms. The current version

• Type: Conference
• Year: 1999
• Where: CADE
• Authors: Frank Pfenning, Carsten Schürmann
• Keywords: CADE 1999, Constraint Logic Programming, LF Type Theory, Logical Reasoning, Programming Languages