v0.9.4.0 (Universes, DM4F)

@catalin-hritcu catalin-hritcu released this Feb 2, 2017

This is a big release with lots of important changes compared to v0.9.2.0 exactly a year ago:

  • Predicative hierarchy of universes with universe polymorphism
  • Uniform syntax between expressions and types allowing rich type-level computation
  • Dijkstra Monads for Free (https://www.fstar-lang.org/papers/dm4free/)
  • Extraction to C via KreMLin (https://github.com/FStarLang/kremlin)
  • New parser based on Menhir
  • New pretty printer for surface syntax and fstar --indent
  • Changed default effect to Tot
  • Strict positivity check for inductives
  • New synatax for inductive type projectors and discriminators
  • Better semantics for module open and support for local opens
  • Better dependency analysis
  • Better error locations for Z3 failures
  • Replaced Z3 timeouts with machine independent resource limits
  • Cleaned up libraries and examples (a bit)
  • Improvements to interactive mode
  • Docker builds
  • Fixed a ton of bugs (262 closed GitHub issues)