-
Notifications
You must be signed in to change notification settings - Fork 236
Project topics on F*
http://prosecco.gforge.inria.fr/personal/hritcu/students/topics/2016/fstar.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 CiC.
- 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/ 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
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 Nik 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] [Tiger]: https://www.cs.princeton.edu/~appel/modern/ml/project.html