-
Notifications
You must be signed in to change notification settings - Fork 232
Project topics on F*
https://catalin-hritcu.github.io/students/topics/2019/fstar-topics.pdf
We've done [quite a bit of this already] (https://github.com/FStarLang/FStar/tree/master/examples/metatheory), so this would be a rather safe direction. One interesting topic would be to do the POPLMark challenge cleanly in F*. We have already done System F-omega (not very clean though) and STLC with subtyping (it's in a different repo, but I can send the files around if they are not in the repo by then) in F*, so the gap to fill wouldn't be so large. For POPLMark one would of course expect a solution that's as clean as possible, and we've been quite successful so far with a proof style borrowed from Autosubst that uses parallel substitution and deBruijn indices; the largest clean thing we have in this style is a proof of lambda-omega. Other than System-F-sub, other calculi one could try to formalize could include dependently typed languages for instance: starting with LF and CC, and maybe even try to get to CC-omega and CiC. Also a generic formalization of pure type systems would be great
New page on this: Mechanized-Metatheory-in-F*
- sorting (we have proved correctness for some sorting algorithms but not stability)
- AVL or red-black trees (we have insertion but operations like deletion can be really interesting: http://matt.might.net/articles/red-black-delete/)
- these are all low risk topics
- binary search in sorted arrays (Chantal has functional version)
- union-find, hash-tables, imperative sorting (I think we now have only quick sort)
- again, all low risk
- http://www.verifythis.org -- simple
- http://vscomp.org/wp-content/uploads/2013/04/newproblems1.pdf -- complex
- https://vacid.codeplex.com/
- there is a project at Inria on comparing different verifiers (don't remember the name, but Arthur Charguéraud and Francois Pottier are involved) For these it might even be interesting to compare with solutions in other systems, if available.
- Section 9 here: https://www.ps.uni-saarland.de/courses/cl-ss14/script/icl.pdf
- Gert Smolka says it was nasty formalizing this in Coq because of syntactic termination
- Update Nik has now a version of this in: https://github.com/FStarLang/FStar/blob/master/examples/algorithms/Unification.fst
http://sci-hub.bz/10.1007/BF00289068 https://www.cs.cornell.edu/courses/cs312/2007fa/lectures/lec21-schorr-waite.pdf
"The Schorr-Waite algorithm is the first mountain that any formalism for pointer aliasing should climb" (Bornat).
- QuickStar = QuickChick for F*
- would be interesting only to the extent we can get better automation using the SMT solver
- Zoe and Nick had some progress on this in a private repo, but that was still when defining new effects in F* was a big pain. Should try again once we have DM4F working.
- It would be nice to formalize parts of simple toy compiers, like Tiger