Add topic "F*" Accepted
Changes: 4
-
Add F* Tutorial
- Title
-
- Unchanged
- F* Tutorial
- Type
-
- Unchanged
- Book
- Created
-
- Unchanged
- no value
- Description
-
- Unchanged
- The first four parts of this book explain the main features of the language using a variety of examples. You should read them sequentially, following along with the associated code samples and exercises. These first four parts are arranged in increasing order of complexity—you can stop after any of them and have a working knowledge of useful fragments of F*. The remaining parts of the book are more loosely connected and either provide a reference guide to the compiler and libraries, or develop case studies that the reader can choose depending on their interest. Of course, some of those case studies come with prerequisites, e.g., you must have read about effects before tackling the case study on parsers and formatters.
- Link
-
- Unchanged
- https://www.fstar-lang.org/tutorial/
- Identifier
-
- Unchanged
- no value
Resource | v1 | current (v1) -
Add F*
- Title
-
- Unchanged
- F*
- Description
-
- Unchanged
- F* (pronounced F star) is a functional programming language inspired by ML and aimed at program verification. Its type system includes dependent types, monadic effects, and refinement types. This allows expressing precise specifications for programs, including functional correctness and security properties. The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving and manual proofs. Programs written in F* can be translated to OCaml, F#, and C for execution. Previous versions of F* could also be translated to JavaScript. The latest version of F* is written entirely in a common subset of F* and F#, and bootstraps in both OCaml and F#. It is open source (under the Apache License 2.0) and is under active development on GitHub.
- Link
-
- Unchanged
- https://en.wikipedia.org/?curid=38420593
Topic | v1 | current (v1) -
Add F* has official F* Tutorial
- Current
- has official
Topic to resource relation | v1 -
Add Programming language e.g. F*
- Current
- e.g.
Topic to topic relation | v1