Home
Mark Gritter edited this page Nov 30, 2021
·
119 revisions
Welcome to the F* wiki! This wiki contains additional, usually more in-depth, technical documentation on top of the F* tutorial. If you add a new page, please add it to the table of contents below!
This is a best effort thing, so it might be unpolished, inconsistent, or out of date. Please help us improve it! This wiki might one day expand into a full-fledged "reference manual", or something. Use the search feature of GitHub or table of contents on the right to navigate.
- F* tutorial
- Installing F*
- Editor-support-for-F*
- Executing F* code
- What is verified, what is extracted?
- Early stumbling blocks, FAQ
- Different types of equality in F*
- Sliding admit verification style
- rlimits: Machine Independent Resource Limits for Deterministic Execution
- Quantifiers and patterns
- F* symbols reference
- Calculational proofs
- Sugar for manipulating connectives in classical logic
- Dealing-with-F★-dependencies
- F★-Interfaces (simple version)
- F★ interfaces (split-file, more complicated version)
- Generating documentation with fsdoc comments
- Using SMT fuel and the normalizer
- Robust, replayable proofs using unsat cores, (aka, hints, or how to replay verification in milliseconds instead of minutes)
- Running F* from a docker image
- Profiling z3 queries
- Tactics
- The syntax of arrow types and default effects
- Recent backward incompatible changes
- Qualifiers-for-definitions-and-declarations
- Custom attributes
- Migrating-code-to-universes
- Parsing and operator precedence
- Machine integers
- Deriving hasEq predicate for inductive types, and types of equalities in F*
- Modules, namespaces and name resolution
- Local opens
- Explicit universes
- Partial evaluation before extraction
- Tactic meeting minutes
- Unicode Support in F★
- New modifies clauses with buffers, references and regions
- SMT-Equality-and-Extensionality-in-F*
- Working with files with huge verification times
- Error-locations-in-generated-OCaml-code
- Pragmas (#set-options, #reset-options)
- Debugging FStar
- F* Heap Model
- Some-issues-and-workarounds-when-writing-interfaces
- Running F* Programs Interactively with the OCaml Interactive Toplevel
- Some general guidelines about src syntax, the core AST
- Bootstrap-process-of-F★-(the-gory-details)
- Editing F* compiler sources
- Structure of src dir
- The-many-Makefile-targets
- Editing files in the library
- Writing code in the intersection of F★, F# and OCaml
- Profiling F* (Linux/OCaml)
- Creating binary packages for your platform
- F* release process; Release notes for F* 0.9.5
- Moving to menhir
- The unification algorithm
- Contributing to master
- Some day, maybe
- Top-level effects
- Cheap functors
- Indexed effects
- F* Lean Integration
- Style guide
- let mutable
- Large-scale separate verification & compilation
- Roadmap for usable interfaces
- Getting better mileage out of Z3
- Improving the sequence library
- Uniform effects
- Efficient execution of F* tactics (native compilation scheme)
- F* tactics proposal (original design of tactics in relation to Lean)
- Generalizing tactics to customize the behavior of F*
- Elements-of-Low*-v3
- Abstractions-for-Reasoning-about-Memory-in-F*-Low*
- Low*-v3-surface-language-:-Steel
- Steel (outdated)
- Steel-(Outline) (outdated)
- Steel:-surface-language (outdated)
- Steel:wishlist