hms/lambda
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
A translation of Gérard Huet's Lambda Calculus formalization in Coq (https://github.com/coq-contribs/lambda) to WhyML. Part of an internship focusing on adding case analysis on inductive predicates in Why3.
32 commits 1 branch 1 tag 356 KiB
  • OCaml 100%
Find a file
Exact
Henri Saudubray 41673af4ce
 feat: final proof with correct termination check
2024-09-20 13:50:21 +02:00
ml feat: proof with match_inductive (without termination) and a bit of ml 2024-06-04 15:58:18 +02:00
mlw feat: final proof with correct termination check 2024-09-20 13:50:21 +02:00
.gitignore chore: backup 2024-04-01 19:00:43 +02:00
README.md feat: proof with match_inductive (without termination) and a bit of ml 2024-06-04 15:58:18 +02:00

README.md

Lambda

A direct translation of Gérard Huet's Lambda Calculus formalization in Coq to WhyML.

Part of an internship focused on adding case analysis on inductive predicates in Why3.