Research projects using Twelf

From The Twelf Project
Jump to: navigation, search

Please add your research using Twelf to the links below. We hope this collection of links will encourage collaboration among Twelf users and record how Twelf is being used in practice.

The links on this page are grouped into two rough categories: larger projects (e.g., a multi-year endeavor) and smaller projects (e.g., some Twelf code that accompanies a research paper). The line between these two is fuzzy, so add your work wherever you think it fits best.

Research using Twelf

Larger projects

  • Logosphere - using Twelf to represent logics in other languages like Resolution, HOL, and PVS. The logic programming engine can then translate proofs between different theories, which has been done for HOL and Nuprl.
  • Proof Carrying Code - scaling up the idea of Proof Carrying Code to real programming languages, using a logic encoded in Twelf's dependent type system.
  • The SeLF Project - encodings of security policies and proofs of security properties for the Grey project.
  • Mechanizing the Metatheory of Standard ML - a formalization of Standard ML and verification of its metatheory in Twelf.
  • Modal Types for Mobile Code - Tom's Ph.D. thesis project
  • LATIN - a project aimed at the creation of a large library of logics and logic translations supported by a web-scalable infrastructure

Smaller projects

Related projects

  • The POPLmark Challenge - A project aimed at increasing the overall use of theorem provers like Twelf in programming language design. A solution to the full challege using Twelf submitted by a team at CMU [1].
  • Delphin - An integration of concepts from Twelf and functional programming languages.
  • Elf - The predecessor to Twelf.