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.
Abstract:
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.
