Qbit (bik_top) wrote in ru_fsharp,
Qbit
bik_top
ru_fsharp

F*

http://research.microsoft.com/en-us/projects/fstar/:
«F* is a new dependently typed language for secure distributed programming. It's designed to be enable the construction and communication of proofs of program properties and of properties of a program's environment in a verifiably secure way. F* compiles to .NET bytecode in type-preserving style, and interoperates smoothly with other .NET languages, including F#, on which it is based.

Self-certification of F*: We have verified the F* type checker using F* itself, using a novel bootstrapping technique called self-certification

http://research.microsoft.com/apps/pubs/?id=141708:
«We present F*, a full-fledged design and implementation of a new dependently typed language for secure distributed programming. Unlike prior languages, F* provides arbitrary recursion while maintaining a logically consistent core; it enables modular reasoning about state and other effects using affine types; and it supports proofs of refinement properties using a mixture of cryptographic evidence and logical proof terms. The key mechanism is a new kind system that tracks several sub-languages within F* and controls their interaction. F* subsumes two previous languages, F7 and Fine. We prove type soundness (with proofs partially mechanized in Coq) and logical consistency for F*.»

Via nponeccop.
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your IP address will be recorded 

  • 0 comments