Crate lsts

source ·
Expand description

Large Scale Type Systems: LSTS implements a categorical view of typed lambda calculus with flexible soundness guarantees.


  • 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.
  • General quality-of-life services in Rust