Andy Melnikov (nponeccop) wrote,
Andy Melnikov

F* на F#

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 mechanized in Coq)
and logical consistency for F*. We have implemented a compiler that translates F* to .NET
bytecode, based on a prototype for Fine. F* provides access to
libraries for concurrency, networking, cryptography, and interoperability with C#, F#, and the other .NET languages. We have formalized the metatheory of F*, and mechanized a significant part of the metatheory in Coq. We have developed a prototype compiler for F* (35,000 lines of F#), and used F* to program and verify more than 20,000 lines of code. We believe F* is the first language of its kind with such a scale of implementation and evaluation.
Tags: fp, language design, programming

  • Post a new comment


    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.