Skip to content

Formalization of the Lambda Cube #25

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
vmarionneau wants to merge 22 commits into
base: main
Choose a base branch
from
Open

Formalization of the Lambda Cube #25

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
110d097
Updated project config
Oct 22, 2025
c52c466
Basic definitions of terms, substitutions and convesion for the lambd…
Oct 22, 2025
ce14f56
Added notion of contexts for the lambda cube
Oct 23, 2025
f245bb4
Aborted unfinished lemmas in LambdaCube/Term.v
Oct 23, 2025
5485d01
added Makefile.conf to gitignore
bousmahawassel Oct 23, 2025
133f1b3
Minor comments
Oct 23, 2025
a61f4c9
Proved most lemmas needed for subtitutions
Nov 14, 2025
e4ca361
Proved lemma about interaction of substitution and fill
Nov 14, 2025
6b51b26
proved confluence of beta-reduction (after rectifying the definition …
bousmahawassel Nov 16, 2025
31bbba5
added typing
bousmahawassel Nov 16, 2025
9b5d5b1
typing contexts are now parametrized by one integer and not 2
bousmahawassel Nov 17, 2025
57f9c0a
Simplified execution contexts
Nov 18, 2025
75fa299
Added stub of strong normalization proof
Nov 18, 2025
0e7d5bc
proved subject reduction
bousmahawassel Nov 18, 2025
4e9e532
Merge branch 'lambda_cube' of https://github.com/bwerner/FormArith in…
bousmahawassel Nov 18, 2025
12f7e8f
proved subject reduction (last time it was only preservation)
bousmahawassel Nov 18, 2025
f7e3f17
fixed naming conflict that appeared when merging
bousmahawassel Nov 19, 2025
b43ec19
fixed typing! When converting types, we ask the 2 types to be convert…
bousmahawassel Nov 20, 2025
eebf3ab
made a file to talk about weak head normal forms
bousmahawassel Nov 29, 2025
79c358a
wrote type inference for the lambda cube
bousmahawassel Dec 5, 2025
c7cdeec
Failed attempt at proving normalization, unclear if salvageable
Dec 15, 2025
7312b44
Renamed files
Dec 15, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,8 @@ time-of-build-before.log
time-of-build-both.log
time-of-build-pretty.log

# Makefile gitignore
Makefile.conf

# == Dune gitignore

Expand Down
3 changes: 2 additions & 1 deletion FormArith.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,9 @@ authors: "FormArith contributors"
homepage: "https://github.com/bwerner/FormArith"
bug-reports: "https://github.com/bwerner/FormArith/issues"
depends: [
"coq" { (= "8.17.1" ) }
"coq" { (= "8.19.2" ) }
"dune" {>= "3.8"}
"coq-autosubst" {>= "1.9"}
]
build: ["dune" "build" "-p" name "-j" jobs]
install: ["dune" "install" "-p" name]
Loading