F7: Refinement Types for F# - Microsoft ResearchF7 is an enhanced typechecker for the F# programming language, a dialect of ML. F7 pioneers the static checking of security properties expressed with refinement types. Although the original motivation was to check security properties, F7 is not security-specific and is applied in other areas, such as database modelling. The theoretical core of F7 is the typed lambda-calculus Refined Concurrent FPC
