Releases: Beluga-lang/McTT
Releases · Beluga-lang/McTT
Base MLTT 1.1
Contributors
pientka and Ailrun
Assets 2
Base MLTT 1.0
This release contains the basic MLTT with natural numbers as the base type, Pi types, and a cumulative universe hierarchy with covariant universe subtyping. The release contains a normalizer, a subtyping decision procedure, a type checking procedure, and a front-end.
What's Changed
- Extract parser to Coq by @jinh0 in #11
- Reorganize Coq modules + AST definition by @jinh0 in #13
- Fix parser by @jinh0 in #21
- [WIP] Well-Scopedness Lemma by @IanGrenville in #12
- Merge fork into
typing-rulesbranch by @jinh0 in #22 - Add typing rules by @jinh0 in #26
- Jason's proof for the well-scopedness lemma by @HuStmpHrrr in #24
- Add lemmas for context conversion proof by @IanGrenville in #28
- Context conversion Lemmas by @IanGrenville in #29
- Proof of syntactic validity(Presup) Lemmas by @IanGrenville in #30
- Update CI build by @IanGrenville in #37
- Update README.md by @HuStmpHrrr in #38
- Update notations by @Ailrun in #39
- Update project structure by @Ailrun in #40
- Update makefile to make extraction cleaner by @Ailrun in #41
- Update Makefile by @Ailrun in #42
- Add natural number recursor by @Ailrun in #43
- Refactor syntatic code style by @Ailrun in #45
- Add domain and related props by @Ailrun in #46
- Fix errors in Semantics by @Ailrun in #48
- Add PER definition by @Ailrun in #47
- Add helper tactic for functional relations by @Ailrun in #50
- Finish PER transitivity by @Ailrun in #49
- fix scripts by @HuStmpHrrr in #53
- attempt to remove unnecessary axioms by @HuStmpHrrr in #52
- Streamline some proofs by @Ailrun in #54
- Streamline some syntactic proofs by @Ailrun in #55
- Rearrange PER parts a bit by @Ailrun in #56
- Finish all PERs by @Ailrun in #57
- Fix per_univ_elem by @Ailrun in #58
- Remove some complexity for PER by @Ailrun in #59
- Finish Realizability for PER by @Ailrun in #60
- Some refactoring by @Ailrun in #62
- Refactor the module structure by @Ailrun in #66
- Prove cumulativity by @Ailrun in #67
- Prove PER for per_ctx_env by @Ailrun in #68
- Refactoring structure by @Ailrun in #69
- Improve proof quality by @Ailrun in #70
- Start to write the base of completeness proof by @Ailrun in #72
- Prove some cases of completeness by @Ailrun in #74
- Update some proofs by @Ailrun in #77
- define type class instances for PERs by @HuStmpHrrr in #79
- Change isomorphism between per_elem by @Ailrun in #81
- Extraction of NbE by @HuStmpHrrr in #80
- make CI parallel by @HuStmpHrrr in #83
- More completeness cases by @Ailrun in #84
- Remove depedence on axioms for PER lemmas by @Ailrun in #89
- More cases for completeness by @Ailrun in #88
- working on the logrel for soundness proof by @HuStmpHrrr in #86
- Finish completeness by @Ailrun in #90
- Add some templates by @Ailrun in #91
- add lemmas for weakenings by @HuStmpHrrr in #92
- improve presup performance by @HuStmpHrrr in #94
- Add build time check to CI by @Ailrun in #96
- Feature/logrel lemmas by @HuStmpHrrr in #93
- Refactoring and optimizing proofs by @Ailrun in #98
- Update ci_build.yml by @Ailrun in #103
- Optimize completeness proofs by @Ailrun in #102
- need a few lemmas to push through this proof by @HuStmpHrrr in #99
- (Probably) Last completeness optimization by @Ailrun in #104
- True last one by @Ailrun in #105
- Try container-based CI by @Ailrun in #106
- Add syntactic judgements for type subsumption by @Ailrun in #101
- Add helper lemmas by @Ailrun in #107
- Add inversion theorems by @Ailrun in #112
- Update inversion theorems by @Ailrun in #114
- Prove some additional lemmas by @Ailrun in #115
- Fix inversion lemmas by @Ailrun in #117
- Prove more lemmas by @Ailrun in #119
- Working on subtyping by @HuStmpHrrr in #122
- remove unnecessary hints by @HuStmpHrrr in #123
- fix tactics by @HuStmpHrrr in #126
- remove contra-variant subtyping by @HuStmpHrrr in #127
- subtyping in the PER model by @HuStmpHrrr in #128
- working on algorithmic subtyping by @HuStmpHrrr in #124
- working on completeness rules for subtyping by @HuStmpHrrr in #130
- finish completeness proof by @HuStmpHrrr in #133
- Some updates on soundness by @Ailrun in #132
- Refactor gen rewritings by @Ailrun in #137
- Prove admitted lemmas by @Ailrun in #138
- Update ci_build.yaml by @HuStmpHrrr in #139
- Provide more soundness lemmas by @Ailrun in #141
- working on realizability by @HuStmpHrrr in #140
- implement monotonicity by @HuStmpHrrr in #149
- add more morphisms by @HuStmpHrrr in #148
- Gluing Cumulativity by @Ailrun in #150
- Prove per escape lemma along gluing by @Ailrun in #151
- Prove subtyping case for soundness by @Ailrun in #153
- Rearrange soundness proofs by @Ailrun in #155
- Provide placeholders for cases by @Ailrun in #156
- Change system rules by @Ailrun in #157
- Prove all easy soundness cases by @Ailrun in #158
- working on subtyping impl by @HuStmpHrrr in #152
- Finish function cases by @Ailrun in #159
- Finish nat cases by @Ailrun in #160
- Add Algorithmic Typing Rules by @Ailrun in #163
- Implement type checker by @Ailrun in #164
- Optimize soundness a bit by @Ailrun in #165
- Reorganize code by @Ailrun in #168
- Use consistent naming by @Ailrun in #169
- Update Coq by @Ailrun in #171
- Add a more "proper" entrypoint with fuller parser by @Ailrun in #170
- update main file by @HuStmpHrrr in #178
- update build process by @HuStmpHrrr in #179
- implement a homepage by @HuStmpHrrr in #183
- Bump actions/checkout from 3 to 4 by @dependabot in #185
- Bump docker/build-push-action from 5 to 6 by @dependabot in #184
- wo...
Contributors
HuStmpHrrr, Ailrun, and 4 other contributors