Skip to content
STELF
Search
Ctrl
K
Cancel
GitHub
Select theme
Dark
Light
Auto
About
The STELF Project
Installation
Guides
Proving metatheorems
Natural numbers
Representing Syntax
Simply typed LF
Representing Judgements
Full LF
Totality Proofs
Metatheorems
Summary
Simply Typed Lambda Calculus
Representing Syntax
Representing the judgements of the STLC
Metatheorems
Summary and exercises
Non-empty contexts
More non-empty contexts
Totality as induction
Total induction
Data-Structures
Higher-order abstract syntax
TotalInduction
Functions as Tuple Sets
Total Paradoxes
Reference
Inner Syntax and Logic
STELF's grammar
Incomplete
Syntax Comparison
Outer Syntax and Projects
Configuring STELF
The New Module System
PAL, managing Projects
Twelf Archive
Hereditary substitution for the STLC
Logical Framework
Glossary
GitHub
Select theme
Dark
Light
Auto
Eta reductions
