Formalization of the Lambda Cube#25

Open

vmarionneau wants to merge 22 commits intomainfrom

Commits on Oct 22, 2025

Updated project config
Virgil Marionneau
committed
Basic definitions of terms, substitutions and convesion for the lambda cube
Virgil Marionneau
committed

Commits on Oct 23, 2025

Added notion of contexts for the lambda cube
Virgil Marionneau
committed
Aborted unfinished lemmas in LambdaCube/Term.v
Virgil Marionneau
committed
added Makefile.conf to gitignore
bousmahawassel
committed
Minor comments
Virgil Marionneau
committed

Commits on Nov 14, 2025

Proved most lemmas needed for subtitutions
Virgil Marionneau
committed
Proved lemma about interaction of substitution and fill
Virgil Marionneau
committed

Commits on Nov 16, 2025

Commits on Nov 17, 2025

typing contexts are now parametrized by one integer and not 2
bousmahawassel
committed

Commits on Nov 18, 2025

Commits on Nov 19, 2025

fixed naming conflict that appeared when merging
bousmahawassel
committed

Commits on Nov 20, 2025

fixed typing! When converting types, we ask the 2 types to be convertible
bousmahawassel
committed

Commits on Nov 29, 2025

made a file to talk about weak head normal forms
bousmahawassel
committed

Commits on Dec 5, 2025

wrote type inference for the lambda cube
bousmahawassel
committed

Commits on Dec 15, 2025

Failed attempt at proving normalization, unclear if salvageable
Virgil Marionneau
committed
Renamed files
Virgil Marionneau
committed