Expand description
Large Scale Type Systems: LSTS implements a categorical view of typed lambda calculus with flexible soundness guarantees.
Modules
The Constant module provides value constants for dynamic evaluation in dependent types
The Debug module defines error messages and formatting
The DFA module defines Deterministic Finite Automata and operations on them
The Kind module provides abstractions over Kinds.
A Term has at least the kind Term.
A Type has precisely one Kind unless that Type is an And.
A Kind can always be written as K1<K2,K3> for Kinds K1, K2, and K3.
There are three intrinsic Kinds: Nil, Term, and Constant.
The LL module defines an LL(1) hand written parser.
The Scope module defines the shape of a typing and evaluation context.
The Term module defines lambda calculus expressions.
The TLC module provides a context object for parsing, typing, and evaluating expressions.
The Token module defines lexical tokens, spans, and a stream tokenizer
The Typ module provides abstractions over Types.