Twelf is an implementation of the logical framework LF developed by Frank Pfenning and Carsten Schürmann at Carnegie Mellon University.[1] It is used for logic programming and for the formalization of programming language theory.