Vous pouvez vous abonner à nos annonces de séminaires
                     http://gallium.inria.fr/seminaires/

                             S E M I N A I R E
       __                                  
      / _`  _   /  /  o                       /| /|   __  __  __ __    _  _
     /   ) __) /  /  / /  / /\/|    -----    / |/ |  /  )(_  /  /  ) ) ) __)
    (___/ (_/ (_ (_ / (__/ /   |            /     | (__/ __)(_ (__/ (_/ (_/
                                                
                          I N R I A - Rocquencourt
                        Amphi Turing du bâtiment 1

                          Lundi 10 octobre, 10h30

                             -----------------
                             Pierre-Yves Strub
                             -----------------

                                   INRIA

    ===================================================================
                           An introduction to F*,
    a new dependently typed language for secure distributed programming
    ===================================================================

Distributed applications are difficult to program reliably and
securely. Dependently typed functional languages promise to prevent
broad classes of errors and vulnerabilities, and to enable program
verification to proceed side-by-side with development. However, as
recursion, effects, and rich libraries are added, using types to
reason about programs, specifications, and proofs becomes challenging.

I will present F*, a full-fledged design and implementation of 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* 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.

F* compiles to .NET bytecode in type-preserving style, and
interoperates smoothly with other .NET languages, including F#, on
which it is based.