lnsol/log-e-sappho
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

lol

Browse source
This commit is contained in:
Ellen Arvidsson 2025-06-27 15:08:13 +02:00
parent 429b59b2b3
commit f3618f1648
1 changed files with 7 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

12
docs/about/progress.md
View file

@ -69,17 +69,19 @@ Thoughts
- the meaning of `true` and existence of methods. - the meaning of `true` and existence of methods.
- undefined behaviour and `true`? - undefined behaviour and `true`?
- how does this relate to the denotation stuff from before? - how does this relate to the denotation stuff from before?
* formal rules and the sequent calculus
# formal rules and the sequent calculus
Check formalities.md.
- simple rules - simple rules
- type constructor rules - type constructor rules
- recursion and cyclic proofs - recursion and cyclic proofs
* next steps? * next steps?
- implementation: sequent calculus based subtyping decider
- simple rules, should be fairly simple
- type constructors, straightforward hopefully
- recursion and cyclic proofs... `¯\_(ツ)_/¯`
- formals: - formals:
- formulate theorems - formulate theorems
- if we use semantic subtyping, isn't it enough to - if we use semantic subtyping, isn't it enough to
prove subtyping sound with regards to set denotation? prove subtyping sound with regards to set denotation?
- specify term language? - specify term language?
- implementation: sequent calculus based subtyping decider
- simple rules, should be fairly simple
- type constructors, straightforward hopefully
- recursion and cyclic proofs... `¯\_(ツ)_/¯`