Home

LSTS is a proof assistant and maybe a programming language. Proofs in LSTS are built by connecting terms, type definitions, and quantified statements. Terms can be evaluated to obtain Values. Types describe properties of Terms. Statements describe relations between Terms and Types.

• Installation
• Expressions
• Functions
• Data Types
• Control Flow
• Propositional Types
• Memory Model
• Statements

Mascot

Doby was a mule that refused to cross a bridge on the way back from a camping trek. He was left for dead in the rough wilderness with winter approaching. Somehow he survived the whole winter under that bridge and was discovered by the game warden the next year.

Doby is the opposite of the common tech mantra of "move fast and go nowhere". Instead, we want to take our time and make steady progress.