Skip to content

wizard7377/stelf

Repository files navigation

STELF (Simple Theorems in the Edinburgh Logical Framework)

STELF is a port of the Twelf project, originally in SML, to OCaml, as well as modernization efforts, such as improving the IDE interface, the build interface, the interlopability, among other efforts.

Note

This is currently a work in progress, and is not yet fully functional

Note that port in this case does mean a literal port, using the Shibboleth converter, we copied over the source litteraly, then fixed out kinks manually and used a port of the SML Basis library. Only after this is working (which has not yet happended) do we intend to make any subsantitive changes to the project itself.

Goals of the Project

Of the goals, there are some more short and longer term ones that are listed here:

Short term goals

  • Get the Twelf/Stelf server as is working correctly
  • Get the testing infrastructure working, also add expected output and expected failure tests
  • Change references of Twelf to Stelf

Medium Term Goals

  • Port the wiki to a easier to use format (likely either mld, typ, tex, or some combination)
  • Port the documentation to odoc style

Long Term Goals

  • Reimplement the lexer and parser to be easier to understand and more efficient
  • Make the frontend OOP based, and make it more modular
  • Split up the concrete syntax and abstract syntax into completely different libraries (ie, one that deals with the internals and another that deals with parsing)
  • Make the server output nicer (add REPL)
  • Make better IDE support (Perhaps using LSP?)
  • Future plans

Credits

While I actually was the one to convert the project, a translator is nothing without a work to translate. As such, credit is in large part due to the original writers of the Twelf project; per the README

Original Twelf Source Code

Copyright (C) 1997-2011, Frank Pfenning and Carsten Schuermann

Authors:

Frank Pfenning
Carsten Schuermann

With contributions by:

Brigitte Pientka
Roberto Virga
Kevin Watkins
Jason Reed

STELF Proper

Copyright (C) 2026, Asher Frost

About

A port of the Twelf implementation of the Logical Framework to OCaml

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

 
 
 

Contributors