# Research projects using Twelf

From The Twelf Project

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

- Dependent Types for ML - A paper by Dan Licata and Bob Harper about enriching an ML-like type system with a form of dependent types. Much of the metatheory of the language is mechanized in Twelf.
- Substructural Languages - Twelf code from some of Matthew Fluet's papers on substructural languages.
- Self-Adjusting Computation - Jake Donham's formalization of a consistency proof of non-deterministic semantics.
- Elaborating Intersection and Union Types — Joshua Dunfield's proofs about an elaboration semantics.
- Coffres forts pour fusils - Sécurité des armes de chasse
- Coffres forts ignifugés pour classeurs - Sécurité des documents contre le risque d'incendie.

## 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.