Template:The Twelf Project/Introduction

From The Twelf Project
Jump to: navigation, search

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.

Visitors without a technical background are encouraged to read the general description of Twelf.