-
Notifications
You must be signed in to change notification settings - Fork 9
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
cfa7900
commit e99c00c
Showing
1 changed file
with
6 additions
and
3 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,16 +1,19 @@ | ||
# Possible future topics | ||
- Have a file showcasing advanced Coq tactics. | ||
- Add example with "Landin's knot" (recursion through the store). | ||
- Add example with "Landin's knot" (recursion through the store) to showcase use of invariants for sequential programs. | ||
- Add some exercises from Persistently chapter in ILN to Persistently chapter. | ||
- Introduce Generic CMRAs | ||
- Introduce Higher Order CMRAs | ||
- Internal equivalence and validity (Plainly, SIProp) | ||
- Inner workings of BI and using Iris proofmode on other logics. | ||
- Incompatibility of excluded middle. | ||
- How to define a new language in Iris. | ||
- Defining new modalities | ||
- Run through the relevant typeclasses | ||
- On inductive, co-inductive, and guarded-recursive predicates (based on chapter in ILN). | ||
- How to define a new language in Iris. | ||
- How to define a new program in Iris. | ||
- How to define logical relations models of type systems in Iris. | ||
|
||
# Features | ||
- Make tutorial accessible as an interactive webpage (jscoq) | ||
- See e.g. https://jscoq.github.io/ext/sf/ | ||
- See e.g. https://jscoq.github.io/ext/sf/ |