F7 An enhanced typechecker for the F# programming language
Download

F7 Ranking & Summary

F7 Tags

annotation F# typechecker fsi checker generate fsi typechecker

F7 Description

F7 was developed to be an enhanced typechecker for the F# programming language. F7 supports static checking of properties expressed with refinement types. Our motivation is to check various security properties of F# implementation code by typing. The F7 typechecker enables programmers to express and statically check refinement types for programs written in F#. The current implementation of the typechecker supports only a subset of F# and works best when type annotations are provided according to certain idioms. To use the typechecker, the programmer must define F7 interfaces for each F# module in thex program. F7 interfaces have the suffix .fs7 to distinguish them from normal F# interfaces (that have suffix .fsi); they may contain types that are outside the F# type system. F# modules have suffix .fs and contain unmodified F# code. In our current approach, all refinement type annotations must be given in the F7 interface. Given an F# module M.fs with an F7 interface M.fs7, the typechecker can be invoked in two ways. First, it can be invoked with the -genfsi flag to generate an F# interface M.fsi by erasing all refinements: f7.exe -genfsi M.fs7 Second, it can be invoked to typecheck M.fs against the types declared in M.fs7. f7.exe M.fs7 M.fs In general, these command lines would contain a series of F# modules and F7 interfaces, including interfaces for all the library modules. A special library interface, called pervasives.fs7, declares common F# types, such as integers, strings, booleans, and lists, and their common operators, such as arithmetic operations and logical connectives. This library can be extended to include any F# operator that the program needs to use.

F7 Related Software