Skip to content
STELF
Search
Ctrl
K
Cancel
GitHub
Select theme
Dark
Light
Auto
About
The STELF Project
Installation
STELF Site
Style Guide
Additional Resources
Guides
Proving Metatheorems
First Order
Representing Syntax
Simply typed LF
Representing Judgements
Full LF
Totality Proofs
Metatheorems
Summary
Solution: plus is commutative
Solution: defining the odd numbers
Solution: proofs about even and odd numbers
Solution: proofs about adding even and odd numbers
Proving metatheorems with STELF
Advanced
Non-empty contexts
More non-empty contexts
Higher Order
Representing Syntax
Representing the judgements of the STLC
Metatheorems
Summary and exercises
Example Guide
LF Squared
LF Squared
Preliminaries
Basics
Working in LF
Total induction
Data Structures
Higher-order abstract syntax
Total Induction
Functions as Tuple Sets
Total Paradoxes
Reference
Case Studies
Admissibility of cut
Big algebraic solver
Bracket abstraction
C machine and focusing
C machine and focusing (composition in machine state)
C machine and focusing (internalized compositon)
Case studies
Church-Rosser via complete development
Church-Rosser (w/ catch-all case)
Church-Rosser (w/ identity reduction)
Classical S5
Concrete representation
ConstructiveSemantics
Correctness of mergesort
Division over the natural numbers
Double-negation translation
Evaluation contexts
Structural focalization
Hereditary substitution with a zipper
HOAS nat bijection
Indexed HOAS nat bijection
Indexed lists
Iterated inductive definitions and defunctionalization
Iterated Let Bindings
Lax logic
Letrec
Lexicographical orderings with density
Linear logic
Lists
MinMLToMinHaskell
Modal logic
Modally Propositional Logic
Mutable state
Natural numbers with inequality
Pattern matching
Polarized PCF
Reformulating languages to use hypothetical judgements
Sudoku
Tethered modal logic
Typed combinators soundness and completeness
User-defined constraint domain
Verifications and uses
Verifications and uses with zippers
Weak focusing
Zermelo Frankel
Example Reference
Outer Language
Configuring STELF
Error messages
PAL, managing Projects
STELF project file Reference
Reduction Relationships
Alpha reductions
Beta reductions
Canonical forms
Eta reductions
Hereditary substitution
Normal forms
Syntax
Troubleshooting mode checking errors
Decleartions
%define
%determinstic
Expressions
Fixity declaration
Lexical Syntax of STELF
The New Module System
%assert
%block
%clause
%covers
%.
%establish
%freeze
%mode
%name
%prove
%querytabled
%reduces
%solve
%subord
%tabled
%thaw
%theorem
%total
%trustme
%unique
%use
Terminology
Abstract syntax
Ad hoc binding structures
Adaquacy
Catch-all case
Congruence relation
Constraint domains and coverage checking
Converting between implicit and explicit parameters
Coverage checking
Debugging coverage errors
Effectiveness lemma
Equality
Equivalence relation
Exchange lemma
Explicit context
Function
Ground
Higher-order judgements
Hypothetical judgment
Implicit and explicit parameters
Incremental metatheorem development
Intrinsic and extrinsic encodings
Judgment
Logic programming
Meta-logic
Metatheorem
Modes of use
Mutual induction
Negation as failure
Numeric termination metrics
Object Language
Output factoring
Output freeness
Reasoning from false
Relation
Respects lemma
Simplifying dynamic clauses
Simply-typed lambda calculus
Strengthening
Subordination
Syntax (Object logic)
Tabled logic programming
Tactical theorem proving
Theorem prover
Totality assertion
Twelf signature
Type family
Unification
Uniqueness lemma
Unsafe mode
Weakening lemma
Background
Arities in LF
Dependent types
Logical Framework
Lambda cube
LF
Paradoxes of Logic
Examples
GitHub
Select theme
Dark
Light
Auto
Documentation out of date
Learn more
CADE Tutorial/MinML
MinML Syntax and judgments---the code we just wrote
Solutions to exercises
