Page Index - FStarLang/FStar GitHub Wiki

291 page(s) in this GitHub Wiki:

• Home
• Beginners guide
• Structuring your project; modularity
• More advanced topics
• Language design
• Tips and tricks when using F★
• Hacking on F★ itself!
• Proposals
• Tactics proposals
• Low* proposals
• List of project topics on F*
• Ongoing work on Steel
• Notes
• [Work in Progress] Enriching Steel's memory model
• Please reload this page
• A Strategy for Inserting returns in Verification Conditions
• Please reload this page
• Abstractions for Reasoning about Memory in F* Low*
• Please reload this page
• Array Structs in Steel
• Please reload this page
• Bootstrap process of F★ (the gory details)
• Please reload this page
• Building F* with dune? (and esy?)
• Please reload this page
• Caching verified modules
• Please reload this page
• Calculational proofs
• Please reload this page
• Cheap functors
• Please reload this page
• CI wishlist
• Please reload this page
• Classifying the F* test suite
• Please reload this page
• Code pattern for hiding definitions from Z3 and selectively revealing them
• Please reload this page
• Collecting .smt2 files from F*'s regression suite
• Please reload this page
• Compiler hacking: Calling an OCaml or F# library from the F* sources
• Please reload this page
• Compiling tactics
• Please reload this page
• Compiling the tutorial using madoko
• Please reload this page
• Contributing to master
• Please reload this page
• Creating binary packages for your platform
• Please reload this page
• Cross module Inlining
• Please reload this page
• Custom attributes
• Please reload this page
• Dealing with F★ dependencies
• Please reload this page
• Debugging flags
• Please reload this page
• Debugging FStar
• Please reload this page
• Deriving hasEq predicate for inductive types, and types of equalities in F*
• Please reload this page
• Design note: Revising the unifier
• Please reload this page
• Different types of equality in F*
• Please reload this page
• Dijkstra Monads for Free
• Please reload this page
• Documenting the library
• Please reload this page
• Early stumbling blocks, FAQ
• Please reload this page
• Editing F* compiler sources
• Please reload this page
• Editing files in the library
• Please reload this page
• Editor support for F*
• Please reload this page
• Efficient execution of F* tactics
• Please reload this page
• Elements of Low* v3
• Please reload this page
• Error locations in generated OCaml code
• Please reload this page
• Executing F* code
• Please reload this page
• Explicit universes
• Please reload this page
• F* Heap Model
• Please reload this page
• F* Lean Integration
• Please reload this page
• F* release process
• Please reload this page
• F* symbols reference
• Please reload this page
• F* tactics proposal
• Please reload this page
• Failure attributes
• Please reload this page
• Friend modules
• Please reload this page
• F★ Interfaces (simple version)
• Please reload this page
• F★ interfaces (split file, more complicated version)
• Please reload this page
• Generalizing tactics to customize the behavior of F*
• Please reload this page
• Generating documentation with fsdoc comments
• Please reload this page
• Getting better mileage out of Z3
• Please reload this page
• Improvements to F*: Brainstorm 2019
• Please reload this page
• Improving channel types in Steel
• Please reload this page
• Improving the sequence library
• Please reload this page
• Indexed effects
• Please reload this page
• Lambda Literals in SMT Proof
• Please reload this page
• Large scale separate verification & compilation
• Please reload this page
• Layered DSLs for Stateful Programming
• Please reload this page
• let mutable
• Please reload this page
• Local opens
• Please reload this page
• Machine integers
• Please reload this page
• Making extraction to Krml extensible; towards a separate repo for Steel?
• Please reload this page
• Mechanized Metatheory in F*
• Please reload this page
• Memoizing typechecking
• Please reload this page
• Meta F* entry points
• Please reload this page
• Meta F*, (anti) quotations, term views and inspect versus inspect_ln
• Please reload this page
• Migrating code to universes
• Please reload this page
• Modules, namespaces and name resolution
• Please reload this page
• Moving away from abstract
• Please reload this page
• Moving to menhir
• Please reload this page
• Mutable structures in Low*
• Please reload this page
• New modifies clauses with buffers, references and regions
• Please reload this page
• Notes on hooks into the tactic engine
• Please reload this page
• Notes on optimizations for type inference and memoization
• Please reload this page
• Optimizing the Generation of Verification Conditions
• Please reload this page
• Parsing and operator precedence
• Please reload this page
• Partial evaluation before extraction
• Please reload this page
• Pragmas (#set options, #reset options)
• Please reload this page
• Profiling F* (Linux OCaml)
• Please reload this page
• Profiling F* with Linux perf
• Please reload this page
• Profiling F* with OCaml Landmarks
• Please reload this page
• Profiling F* with Spacetime
• Please reload this page
• Profiling F* with the OCaml statistical memory profiler
• Please reload this page
• Profiling Z3 queries
• Please reload this page
• Project ideas (Summer 2019)
• Please reload this page
• Project topics on F*
• Please reload this page
• Proposal: A verified region based memory manager for Low*
• Please reload this page
• Proposal: Indexed effects
• Please reload this page
• Qualifiers for definitions and declarations
• Please reload this page
• Quantifiers and patterns
• Please reload this page
• Recent backward incompatible changes
• Please reload this page
• Relational F* for State Separating Cryptographic Proofs
• Please reload this page
• Release notes for F* 0.9.5
• Please reload this page
• Revised checking of a module's interface
• Please reload this page
• rlimits: Machine Independent Resource Limits for Deterministic Execution
• Please reload this page
• Roadmap for usable interfaces
• Please reload this page
• Robust, replayable proofs using unsat cores, (aka, hints, or how to replay verification in milliseconds instead of minutes)
• Please reload this page
• Running F* from a docker image
• Please reload this page
• Running F* Programs Interactively with the OCaml Interactive Toplevel
• Please reload this page
• Running tactics natively (and plugins)
• Please reload this page
• Sign up to show and tell
• Please reload this page
• Sliding admit verification style
• Please reload this page
• SMT Equality and Extensionality in F*
• Please reload this page
• Some day, maybe
• Please reload this page
• Some general guidelines about src syntax, the core AST
• Please reload this page
• Some issues and workarounds when writing interfaces
• Please reload this page
• Squashed vs constructive proofs
• Please reload this page
• Steel
• Please reload this page
• Steel (Outline)
• Please reload this page
• Steel: Framing
• Please reload this page
• Steel: Selectors
• Please reload this page
• Steel: surface language
• Please reload this page
• Steel:wishlist
• Please reload this page
• Structure of the F* sources (very outdated)
• Please reload this page
• Style guide
• Please reload this page
• Sugar for manipulating connectives in classical logic
• Please reload this page
• Tactic meeting minutes
• Please reload this page
• Tactics
• Please reload this page
• The future of fstar mode
• Please reload this page
• The many Makefile targets
• Please reload this page
• The syntax of arrow types and default effects
• Please reload this page
• The unification algorithm
• Please reload this page
• Timing your changes
• Please reload this page
• Tips for extraction with polymorphism and erasure
• Please reload this page
• Top level effects
• Please reload this page
• Towards a Finer grained Incremental Typechecker for F*
• Please reload this page
• Towards a Tactics v2
• Please reload this page
• Tracking and reporting source locations in SMT errors
• Please reload this page
• Trying a new page for the RSS feed
• Please reload this page
• Typeclasses (via meta arguments)
• Please reload this page
• Unicode Support in F★
• Please reload this page
• Uniform effects
• Please reload this page
• Using SMT fuel and the normalizer
• Please reload this page
• What is verified, what is extracted?
• Please reload this page
• Working with files with huge verification times
• Please reload this page
• Wrapping OCAML
• Please reload this page
• Wrapping OCaml Main.fst
• Please reload this page
• Wrapping OCaml WrapOCaml.fsti
• Please reload this page
• Wrapping OCaml WrapOCaml.ml
• Please reload this page
• Wrapping OCaml WrapOCaml.mli
• Please reload this page
• Writing code in the intersection of F★, F# and OCaml
• Please reload this page