F*: A Proof-Oriented Programming Language

<!doctype html> <html lang="en"> <head> <meta charset="utf-8"> <link type="image/x-icon" rel="icon" href="favicon.ico"> <link type="image/x-icon" rel="shortcut icon" href="favicon.ico"> <link rel="stylesheet" href="style2.css"> <script src="https://ajax.googleapis.com/ajax/libs/webfont/1.5.6/webfont.js"></script> <script>WebFont.load({ google: { families: ['Source Sans Pro'] } });</script> <title>F*: A Proof-Oriented Programming Language</title> </head> <body> <div id="nav"> <img id="logo" src="i/fstar-new.png" alt="F* Logo"> <div id="hdr"> <ul> <li><a href="index.html#intro">Introduction</a></li> <li><a href="index.html#download">Download</a></li> <li><a href="index.html#learn">Learn</a></li> <li><a href="index.html#community">Community</a></li> <li><a href="index.html#uses">Uses</a></li> <li><a href="index.html#research">Research</a></li> <li><a href="people.html">People</a></li> </ul> </div> </div>  <div class="content" id="intro"> <h1>Introduction</h1> <hr /> <p align="justify"> F* (pronounced <it>F star</it>) is a general-purpose proof-oriented programming language, supporting both purely functional and effectful programming. It combines the expressive power of dependent types with proof automation based on SMT solving and tactic-based interactive theorem proving. <p> F* programs compile, by default, to OCaml. Various fragments of F* can also be extracted to F#, to C or Wasm by a tool called <a href="https://github.com/FStarLang/karamel">KaRaMeL</a>, or to assembly using the <a href="https://github.com/project-everest/vale">Vale</a> toolchain. F* is implemented in F* and bootstrapped using OCaml. <p> F* is open source on <a href="http://github.com/FStarLang/FStar">GitHub</a> and is under active development by <a href="http://research.microsoft.com">Microsoft Research</a>, <a href="http://prosecco.gforge.inria.fr/">Inria</a>, and by the community. </div>  <div class="content" id="download"> <h1>Download</h1> <hr /><p> F* is distributed under the <a href="https://raw.githubusercontent.com/FStarLang/FStar/master/LICENSE" target="_blank">Apache 2.0 license</a>. Binaries for Windows, Linux, and Mac OS X are posted regularly on the <a href="https://github.com/fstarlang/fstar/releases">releases page on GitHub</a>. You can also install F* from OPAM, Docker, Nix, or build it from sources, by following the instructions in <a href="https://github.com/FStarLang/FStar/blob/master/INSTALL.md">INSTALL.md</a>. </p> </div> </div>  <div class="content" id="learn"> <h1>Learn F*</h1><hr /> <p>An online book <a href="tutorial/proof-oriented-programming-in-fstar.pdf">Proof-oriented Programming In F*</a> is being written and regular updates are posted online. You probably want to read it while trying out examples and exercises in your browser by clicking the image below. <p align="center"> <a href="/tutorial" target="_blank"><img src="i/tutorial-snapshot.JPG" alt="F* Tutorial" height=400 style="border:2px solid #333;" /></a> </p> <h2>Low*</h2> <p>We also have a <a href="https://fstarlang.github.io/lowstar/html/"> tutorial that covers Low*</a>, a low-level subset of F*, which can be compiled to C by KaRaMeL. </p> <h2>Course Material</h2> <p>F* courses are often taught at various seasonal schools. Lectures and course materials for some of them are also a useful resource. <ul style="padding-left:2em"> <li style="margin-bottom: 1ex;"> Embedding Proof-oriented Programming Languages in F*) <ul style="padding-left:2em"> <li>Online lectures at the <a href="https://www.cs.uoregon.edu/research/summerschool/summer21/">Oregon Programming Language Summer School (2021)</a>: <a href="oplss2021/index.html">Lecture notes, slides, code</a> </li> </ul> </li> <li style="margin-bottom: 1ex;"> Formal Verification with F* and Meta-F* <ul style="padding-left:2em"> <li>Lectures and tutorial at <a href="https://eci2019.dc.uba.ar/">ECI 2019</a>: <a href="eci2019/index.html">Lecture notes, slides, code</a> </li> </ul> </li> <li style="margin-bottom: 1ex;"> Verifying Low-Level Code for Correctness and Security <ul style="padding-left:2em"> <li>Lectures at the <a href="https://www.cs.uoregon.edu/research/summerschool/summer19/">Oregon Programming Language Summer School (2019)</a>: <a href="oplss2019/index.html">Lecture notes, slides, code</a> </li> </ul> </li> <li style="margin-bottom: 1ex;"> Program Verification with F* <ul style="padding-left:2em"> <li> Course at <a href="https://sites.google.com/view/2018eutypesschool/home">2018 EUTypes Summer School</a>, 8-12 August, 2018, Ohrid, Macedonia <a href="https://sites.google.com/view/2018eutypesschool/ahman">Course material</a> </li> </ul> </li> </ul> </div>  <div class="content" id="community"> <h1>Community</h1><hr/> <p> Please use <a href="https://github.com/FStarLang/FStar/discussions">GitHub Discussions</a> to ask questions about F*, learn about announcements, etc. <p> Although we previously used a Slack instance, we aim to consolidate our online community on this public <a href="https://fstar.zulipchat.com">forum on Zulip</a>. <p> We also have a mailing list, which has very low traffic. You can subscribe <a href="https://groups.google.com/g/fstar-mailing-list">at fstar-mailing-list</a>. <p> The <a href="popup/seminar.html">F* PoP Up Seminar</a>, a users and developers meeting is open to all. We aim to schedule it once a month, though the schedule is irregular---we hope to see you there! <p> You can also contact the maintainers of F* at fstar-maintainers@googlegroups.com. </div>  <div class="content" id="uses"> <h1>Uses</h1><hr /> <p> F* is used in several projects in both industrial and academic settings. We list a few of them here. If you are using F* in your project, please let us know by writing to the <a href="https://groups.google.com/g/fstar-mailing-list">fstar-mailing-list</a>. </p> <h2>Project Everest</h2> <p> <a href="https://project-everest.github.io">Project Everest</a> is an umbrella project that develops high-assurance secure communication software in F*. A big part of the development of F* has been motivated by the scenarios that Project Everest targets. Several offshoots from Project Everest continue as their own projects, including some of those listed below. <h2>HACL*, ValeCrypt, and EverCrypt</h2> <p> <a href="https://hacl-star.github.io/">HACL*</a> is a library of high-assurance cryptographic primitives, written in F* and extracted to C. <a href="https://github.com/hacl-star/hacl-star/tree/main/vale">ValeCrypt</a> provides formally proven implementations of cryptographic primitives in Vale, a framework for verified assembly language programming embedded in F*. <a href="https://hacl-star.github.io/EverCryptDoc.html">EverCrypt</a> combines them into a single cryptographic provider. Code from these projects is now used in production in several projects, including <a href="https://blog.mozilla.org/security/2017/09/13/verified-cryptography-firefox-57/">Mozilla Firefox</a>, the <a href="https://github.com/torvalds/linux/blob/0f2a4af27b649c13ba76431552fe49c60120d0f6/lib/crypto/curve25519-hacl64.c#L1">Linux kernel</a>, <a href="https://github.com/python/cpython/issues/99108">Python</a>, <a href="https://github.com/Mbed-TLS/mbedtls/blob/development/3rdparty/everest/">mbedTLS</a>, the <a href="https://www.reddit.com/r/tezos/comments/8hrsz2/tezos_switches_cryptographic_libraries_from/">Tezos blockchain</a>, the <a href="https://www.electionguard.vote/">ElectionGuard</a> electronic voting SDK, and the <a href="https://www.wireguard.com">Wireguard</a> VPN. <h2>EverParse</h2> <p> <a href="https://project-everest.github.io/everparse/">EverParse</a> is a parser generator for binary formats that produces C code extracted from formally proven F*. Parsers from EverParse are used in production in several projects, including in <a href="https://www.microsoft.com/en-us/research/blog/everparse-hardening-critical-attack-surfaces-with-formally-proven-message-parsers/">Windows Hyper-V</a>, where every network packet passing through the Azure cloud platform is parsed and validated first by code generated by EverParse. EverParse is also used in other production settings, including <a href="https://github.com/microsoft/ebpf-for-windows">ebpf-for-windows</a>. </div>  <div class="content" id="research"> <h1>Research</h1><hr /> <p> F* is an active topic of research, both in the programming languages and formal methods community, as well as from an application perspective in the security and systems communities. We list a few of them below, with <a href="fstar_bib.php">full citations to these papers available in this bibliography</a>. If you would like your paper included in this list, please contact fstar-maintainers@googlegroups.com. <h2>The Design of F* and its DSLs</h2> <ul style="padding-left:2em"> <li><a href="https://fstar-lang.org/papers/mumon/">Dependent Types and Multi-monadic Effects in F*</a> (POPL 2016) This is the canonical reference describing the F* system. The language has evolved in significant ways since 2016, however, its core design and implementation is based on this paper. </li> <li><a href="https://arxiv.org/abs/1703.00053">Verified Low-level Programming Embedded in F*</a> (ICFP 2017) which describes the Low* fragment of F* which is a low-level subset of F* that can be compiled to C by KaRaMeL. </li> <li><a href="https://dl.acm.org/doi/10.1145/3290376">A Verified, Efficient Embedding of a Verifiable Assembly Language</a> (POPL 2019) which describes the Vale language, a verified assembly language embedded in F*. </li> <li><a href="http://fstar-lang.org/papers/metafstar/">Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms</a> (ESOP 2019) which describes MetaF*, a metaprogramming system within F* used to implement various aspects of F*, ranging from its tactic engine to its support for typeclasses. </li> <li><a href="https://fstar-lang.org/papers/indexedeffects/">Programming and Proving with Indexed Effects</a> (TR 2021) which describes the design of F*'s support for user-defined effects and provides a calculus that describes the logical core of F*. </li> <li><a href="https://fstar-lang.org/papers/steel/">Steel: Proof-oriented Programming in a Dependently Typed Concurrent Separation Logic</a> (ICFP 2021), which describes the Steel language and its use of the SteelCore concurrent separation logic for proofs of imperative programs with various forms of concurrency. </li> </ul> <h2>Semantics and Effects</h2> <ul style="padding-left:2em"> <li><a href="https://dl.acm.org/doi/10.1145/2499370.2491978">Verifying Higher-order Programs with the Dijkstra Monad</a> (PLDI 2013), which introduces the concept of the Dijkstra monad, a core feature of F*'s system of effects.</li> <li><a href="https://fstar-lang.org/papers/dm4free/">Dijkstra Monads for Free</a> (POPL 2017), which shows how to automatically derive Dijkstra monads for a class of computational monads using a continuation-passing transformation </li> <li><a href="https://arxiv.org/abs/1703.00055">A Monadic Framework for Relational Verification: Applied to Information Security, Program Equivalence, and Optimizations</a> (CPP 2018), which builds on the Dijkstra Monads for Free work to construct a framework for proving properties that relate multiple programs or program executions. </li> <li><a href="https://arxiv.org/abs/1903.01237">Dijkstra Monads for All</a> (ICFP 2019), which generalizes the notion of a Dijkstra monad and shows how to systematically relate computational and specificational monads via monad morphisms. </li> <li><a href="https://arxiv.org/abs/1707.02466">Recalling a Witness: Foundations and Applications of Monotonic State</a> (POPL 2018), which describes the design of a program logic for reasoning about programs whose state evolves monotonically, e.g., where the state is an append-only log. This logic underpins both Low* and Steel. </li> <li><a href="https://fstar-lang.org/papers/steelcore/">SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs</a> (ICFP 2020), which describes the SteelCore concurrent separation logic, the basis of the Steel DSL. </li> <li><a href="https://fstar-lang.org/papers/pulsecore.pdf">PulseCore: A Dependently Typed Stratified Separation Logic</a>, a foundational, axiom-free concurrent separation logic shallowly embedded in F*, supporting dynamic invariants and higher-order ghost state in a predicative setting---PulseCore is the basis of the Pulse DSL. </li> </ul> <h2>Applications in Security and Cryptography</h2> <p>Many papers applying F* in security and cryptography can be found in the <a href="https://project-everest.github.io/papers/">Project Everest bibliography</a>. We mention a few prominent ones here as well as other applications not related to Project Everest. <ul style="padding-left:2em"> <li><a href="https://arxiv.org/abs/1711.06467">WYS*: A DSL for Verified Secure Multi-party Computations</a> (POST 2017), which describes the WYS* language, a domain-specific language for writing verified mixed-mode secure multi-party computations. </li> <li><a href="https://eprint.iacr.org/2016/1178">Implementing and Proving the TLS 1.3 Record Layer</a>(S&P 2017), which describes a verified implementaion of the TLS-1.3 record layer in Low*.</li> <li><a href="https://eprint.iacr.org/2017/536">HACL*: A Verified Modern Cryptographic Library</a> (CCS 2017), which describes HACL*, a verified cryptographic library implemented in Low*.</li> <li><a href="https://ieeexplore.ieee.org/document/8835291">Formally Verified Cryptographic Web Applications in WebAssembly</a> (S&P 2019), which develops LibSignal*, an implementation of the Signal protocol in F* using HACL*, compiled to Wasm by KaRaMeL.</li> <li><a href="https://project-everest.github.io/assets/evercrypt.pdf">EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider</a> (S&P 2020), a crypto provider combining C and assembly code from HACL* and Vale, as well as some applications built on top of it, including a verified high-performance Merkle tree that was used in an initial version of Microsoft Azure CCF.</li> <li><a href="https://project-everest.github.io/assets/haclxn.pdf">HACL脳N: Verified Generic SIMD Crypto (for all your favorite platforms)</a> (CCS 2020), which metaprograms vectorized versions of cryptographic primitives, enabling a "write-once, get vectorized versions for free" style.</li> <li><a href="https://project-everest.github.io/assets/everquic.pdf">A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer</a> (S&P 2021), a verified implementation of the QUIC record layer in Low* combined with the protocol logic implemented in Dafny.</li> <li><a href="https://www.microsoft.com/en-us/research/publication/dice-a-formally-verified-implementation-of-dice-measured-boot/">DICE*: A Formally Verified Implementation of DICE Measured Boot</a> (USENIX Security 2021), which proves the correctness & security of the DICE measured boot protocol for micro-controllers, implemented in Low*, using EverCrypt and EverParse.</li> <li><a href="https://ieeexplore.ieee.org/document/9581188">DY*: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code</a> (Euro S&P 2021), a framework for type-based symbolic security analysis of cryptographic protocol implementations developed in F*.</li> <li><a href="https://link.springer.com/chapter/10.1007/978-3-030-91631-2_4">A Tutorial-Style Introduction to DY*</a> (LNCS 2021), which is, yes, a tutorial-style introduction to DY*.</li> <li><a href="https://dl.acm.org/doi/10.1145/3460120.3484588">An In-Depth Symbolic Security Analysis of the ACME Standard</a> (CCS 2021), which proves the security of a model of the ACME certificate issuance and management protocol using DY*.</li> <li><a href="https://ieeexplore.ieee.org/document/9833621">Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations</a> (S&P 2022), which metaprograms provably secure implementations for a family of secure channel protocols.</li> <li><a href="https://www.usenix.org/system/files/sec23fall-prepub-372-wallez.pdf">TreeSync: Authenticated Group Management for Messaging Layer Security</a> (USENIX Security 2023), a reference implementation of MLS in F*, proven secure using the DY* framework.</li> <li><a href="https://dl.acm.org/doi/10.1145/3607844">Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification</a> (ICFP 2023), which describes proof-engineering techniques used in HACL* for generic implementations of cryptographic constructions that can be specialized repeatedly to many concrete implementations in C. The techniques used here led to the adoption of verified cryptographic code into the libraries of the Python programming language.</li> <li><a href="https://kirby.linvill.net/pdfs/indistinguishability_paper.pdf">Verifying Indistinguishability of Privacy-Preserving Protocols</a> (OOPSLA 2023), which provides a library called Waldo in F* that enables proofs of indistinguishability over traces of communication in networking protocols. </li> <li><a href="https://eprint.iacr.org/2023/1390">Comparse: Provably Secure Formats for Cryptographic Protocols</a> (CCS 2023), which provides a parsing library for data formats that are appropriate for use with symbolic protocol analyzers. Comparse provides bit-level precise accounting of formats allowing the DY* protocol analysis framework to reason about concrete messages and identify protocol flaws that it previously would have missed.</li> </ul> <h2>Applications in Systems</h2> <ul style="padding-left:2em"> <li><a href="https://www.jaybosamiya.com/publications/2022/usenix/provably-safe-sandboxing-wasm.pdf">Provably-Safe Multilingual Software Sandboxing using WebAssembly</a> (USENIX 2022), which describes a verified implementation of a sandbox for WebAssembly modules in Low* and Rust.</li> <li><a href="https://dl.acm.org/doi/10.1145/3448016.3457312">FastVer: Making Data Integrity a Commodity</a> (SIGMOD 2021), which formalizes a protocol for data integrity monitoring in F*.</li> <li><a href="https://fstar-lang.org/papers/fastver2.pdf">FastVer2: A Provably Correct Monitor for Concurrent, Key-Value Stores</a> (CPP 2022), which proves the correctness of a low-level, concurrent implementation of the FastVer protocol in Steel.</li> <li><a href="https://amosr.amospheric.com/papers/robinson2024pipitfull.pdf">Pipit on the Post: Proving Pre- and Post-Conditions of Reactive Systems</a> (ECOOP 2024), which embeds a reactive language in F* and uses it to verify some control systems that execute in real time.</li> <li><a href="https://arxiv.org/abs/2403.09435v1">StarMalloc: Verifying a Modern, Hardened Memory Allocator</a> (SPLASH 2024), a security-oriented, concurrent memory allocator that can be used as a drop-in replacement in real-world projects, verified in Steel.</li> </ul> <h2>Applications in Parsing</h2> <ul style="padding-left:2em"> <li><a href="ttps://www.usenix.org/conference/usenixsecurity19/presentation/delignat-lavaud">EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats</a> (USENIX Security 2019), which describes the EverParse parser generator for parsing binary formats, producing C code. </li> <li><a href="https://fstar-lang.org/papers/EverParse3D.pdf">Hardening Attack Surfaces with Formally Proven Binary Format Parsers</a> (PLDI 2022), which uses EverParse to harden network packet parsers in Windows Network Virtualization and Hyper-V. </li> <li><a href="https://fstar-lang.org/papers/asn1star.pdf">ASN1*: Provably Correct Non-Malleable Parsing for ASN.1 DER </a> (CPP 2022), which formalizes the ASN.1 DER format in F* and proves the correctness of a parser for it in EverParse.</li> </ul> <h2>Applications in Programming, Program Proof, and Program Analysis</h2> <ul style="padding-left:2em"> <li><a href="https://arxiv.org/pdf/1603.01635.pdf">Verified Compilation of Space-Efficient Reversible Circuits</a> (CAV 2018), which presents ReVerC, a compiler for reversible circuits proven correct in F*. <li><a href="https://www.jaybosamiya.com/publications/2020/vstte/transformers.pdf"> Verified Transformations and Hoare Logic: Beautiful Proofs for Ugly Assembly Language </a> (VSTTE 2020), which develops verified transformations for assembly programs in the Vale framework.</li> <li><a href="https://dl.acm.org/doi/10.1145/3428216">Statically verified refinements for multiparty protocols</a> (OOPSLA 2020), which presents Session*, a session-typed programming language for multiparty protocols, formalized in F*.</li> <li><a href="https://arxiv.org/abs/2107.09472">Verified Functional Programming of an Abstract Interpreter</a> (SAS 2021), which develops an abstract interpretation framework for an imperative language with a very compact proof of soundness developed in F*.</li> <li><a href="https://dl.acm.org/doi/abs/10.1145/3473582">Catala: a programming language for the law</a> (ICFP 2021), where core parts of the compiler are formalized and proven correct in F*.</li> <li><a href="https://arxiv.org/abs/2106.04826">Verification of a Merkle Patricia Tree Library Using F*</a>, which ports a Merkle tree library from OCaml to F*, finds and fixes a bug, and eventually proves it correct.</li> <li><a href="https://dl.acm.org/doi/10.1145/3519939.3523735">Certified mergeable replicated data types</a> (PLDI 2022), which presents PEEPUL, a framework in which to build replicated data types for use in distributed programming, formalized in F*.</li> <li><a href="https://dl.acm.org/doi/10.1145/3547647">Aeneas: Rust verification by functional translation</a> (ICFP 2022), which translates Rust into pure F* enabling functional correctness proofs.</li> <li><a href="https://icfp22.sigplan.org/details/planqc-2022/8/Q-Implementing-Quantum-Separation-Logic-in-F-">Q*: Implementing Quantum Separation Logic in F*</a> (PlanQC 2022), which adapts the SteelCore separation logic for use with a quantum programming language.</li> <li><a href="http://amosr.amospheric.com/papers/robinson2023pipit.pdf">Pipit: Reactive Systems in F* (Extended Abstract)</a> (TyDe 2023), which describes a embedded DSL for verifying reactive systems.</li> <li><a href="https://dl.acm.org/doi/10.1145/3632916">Securing Verified IO Programs Against Unverified Code in F*</a> (POPL 2024), which presents SCIO*, a formally secure compilation framework for statically verified programs performing input-output (IO).</li> </ul> <h2>AI-assisted Programming</h2> <ul style="padding-left:2em"> <li><a href="https://arxiv.org/abs/2405.01787">Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming</a> (ICSE 2025), which curates a dataset of 940KLOC of F* code and proof and develops AI models to automate program and proof synthesis</li> <li><a href="https://arxiv.org/abs/2404.10362">3DGen: AI-Assisted Generation of Provably Correct Binary Format Parsers</a>, which developsAI agents to transform mixed informal input, including natural language documents (i.e., RFCs) and example inputs into format specifications into 3D, a data format specification language used with EverParse.</li> </ul> <h2>Miscellaneous</h2> <ul style="padding-left:2em"> <li><a href="https://ieeexplore.ieee.org/abstract/document/10172578">A Theorem Proving Approach to Programming Language Semantics</a> (ICSE-SEET 2023), which reports on experiences teaching operational, denotational, and axiomatic semantics to students using F*.</li> </ul> <h2>Papers about an older version of F*</h2> <p> The first paper to introduce a system called F* was in 2011. Although the current version of F* was redesigned and implemented in 2015, we include some of these older papers here for completeness. <ul style="padding-left:2em"> <li><a href="https://dl.acm.org/doi/10.1145/2034773.2034811">Secure Distributed Programming with Value-dependent Types</a> (ICFP 2011), a longer version of which also appeared in <a href="https://www.cambridge.org/core/journals/journal-of-functional-programming/article/secure-distributed-programming-with-valuedependent-types/14288BBFE9B373738DC8F60C3E89E3E3">JFP</a>.</li> <li><a href="https://inria.hal.science/inria-00628775/document/">Self-certification: bootstrapping certified typecheckers in F* with Coq</a> (POPL 2012), which certifies the correctness of the F* typechecker by programming it in F* itself and bootstrapping the process by checking about 7GB of proof using Coq in about 24 machine-days of compute time.</li> <li><a href="https://dl.acm.org/doi/10.1145/2429069.2429114">Fully abstract compilation to JavaScript</a> (POPL 2013), which models a subset of JavaScript in F* and develops a secure compiler from an ML-like language to JavaScript.</li> <li><a href="https://doi.org/10.1145/2535838.2535889">Gradual typing embedded securely in JavaScript</a> (POPL 2014), which develops a source-to-source compiler for JavaScript with defensive checks to ensure the soundness of gradual typing in adversarial contexts, proven corrent in F*.</li> <li><a href="https://dl.acm.org/doi/10.1145/2535838.2535847">Probabilistic relational verification for cryptographic implementations</a> (POPL 2014), which develops RF*, a relational dialect of the language useful for proving security properties like noninterference and for game-based cryptographic proofs.</li> </ul> <br><br> </div>  <div class="foot-wrap"> <div id="footer"> <div class="foot-1"> <a href="http://research.microsoft.com" target="_blank"><img src="i/msr.png" alt="Microsoft Research" /></a> </div> <div class="foot-1"> <a href="https://www.microsoft.com/en-us/research/collaboration/inria-joint-centre/" target="_blank"><img height="100" src="i/msr-inria.png" alt="MSR Inria Joint Centre" /></a> </div> <div class="foot-1"> <a href="http://www.inria.fr" target="_blank"><img src="i/inria.png" alt="Inria" /></a> </div> </div> </div> </div>

CINXE.COM

F*: A Proof-Oriented Programming Language