On Friday 16/12/2011, at 14h, in room Euler Violet.
Speaker: Pierre-Yves Strub.
Title: 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.