Research projects using Twelf

Please add your research using STELF to the links below. We hope this collection of links will encourage collaboration among STELF users and record how STELF 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 STELF 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 STELF

Larger projects

• Proof Carrying Code - scaling up the idea of Proof Carrying Code to real programming languages, using a logic encoded in STELF’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 STELF.
• 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 STELF.
• Substructural Languages - STELF 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 — Jana Dunfield’s proofs about an elaboration semantics.

Related projects

• The POPLmark Challenge - A project aimed at increasing the overall use of theorem provers like STELF in programming language design. A solution to the full challenge using STELF submitted by a team at CMU [http://fling-l.seas.upenn.edu/~plclub/cgi-bin/poplmark/index.php?title=Submission_from_Carnegie_Mellon].
• Delphin - An integration of concepts from STELF and functional programming languages.
• Elf - The predecessor to STELF.