This is a fairly simple standalone implementation of the Edinburgh Logical Framework, originally adapted from my Typecoin work (but with the few Typecoin extensions to LF stripped out), but since changed substantially. It could be useful educationally (or maybe even practically if you need to embed LF in your stuff for some reason but don't need to parse it >_>). It is all pretty atrociously documented, though, and not that great of code to begin with. Some notes on the implementation: * All of the different syntactic levels (terms, type families, kinds) are collapsed into one level of "expressions" in the implementation. This is because terms and type families share analagous notions of lambdas, variables, constants, and applications and type families and kinds share analagous pi types. * We use the Canonical LF methodology in which all expressions must be in "Canonical Form": beta-short and eta-long. That is, there are no beta redexes (no lambdas applied to arguments) and everything is maximally eta-extended (every variable and constant of function type is applied to all of its arguments). * The type-checking rules for LF involve substitution and substitution does not preserve canonical forms in general. To handle this we use "hereditary substitution" which automatically reduces any new beta-redexes that would be introduced by a substitution. * Hereditary substitution is defined such that it always terminates, even for ill-typed terms. (Though on ill-typed terms it may return an error.) * The lack of beta redexes is enforced by a syntactic split between "atoms" and "expressions", in which the LHS of an application must be an atom, while lambdas are expressions. An earlier version (from Typecoin), used "spine-form", and is available in [the spine branch](https://github.com/msullivan/sully-lf/tree/spine). I switched away from spine form because it seemed like it would make elaboration easier (at least, if I wanted to reuse the same syntax tree for Vanilla LF, as described below.) * Eta-longness is enforced by the type checker, which allows atoms to appear in expressions only at a base type. * One of the big advantages of Canonical LF is that term/type equality is just structural equality! * To make this extra true, we represent variables using de Bruijn indexes. * Code is also included that can elaborate Vanilla LF into Canonical LF. The approach is taken from "LF in LF: Mechanizing the Metatheories of LF in Twelf" by Martens and Crary. Vanilla LF is encoded using the same syntax tree as Canonical LF, through the presence of a atom constructor that takes an expression and an optional type annotation on lambdas. The Canonical LF rejects terms using the expression atom constructor, and the elaborator requires the lambda type annotation to be present (while the Canonical LF typechecker will validate it if present but does not need it). We need to do type-checking as we perform the elaboration, if we want it to be sound (since type incorrect subterms may disappear while reducing beta-redexes, we can't just do checking on the final Canonical LF term). The elaboration process goes recursively, type-checking as it goes, producing both Canonical LF terms and Canonical LF types. Variables and constants are eta-expanded using their "simple types" (that is, only distinguishing between pi types and base types). When elaborating an application, the left hand side should always elaborate to a lambda, and so we use hereditary substitution to eliminate the lambda. The *canonical* expression is substituted into the pi type on applications, and the canonical types are used for all type equality checks. Thus, we do type checking on the Vanilla LF program using Canonical LF expression equality (which is trivial) instead of Vanilla LF equality (which is complex).