1) Logic in computer science 
===Formalizing mathematics=== Twelf`s main use today is as a system for formalizing mathematics (especially the metatheory of programming languages). Used this way it is closely related to Coq and Isabelle/HOL/HOL Light. However, unlike those systems, Twelf proofs are typically developed by hand. Despite this, for the problem domains at which it ....