{{language|Twelf |site=http://twelf.plparty.org/wiki/Main_Page }} Twelf is a language used to specify, implement, and prove properties of deductive systems such as programming languages and logics. Large research projects using Twelf include the TALT typed assembly language, a foundational proof-carrying-code system, and a type safety proof for Standard ML. {{stub}}