Write a Blog >>
ICFP 2016
Sun 18 - Sat 24 September 2016 Nara, Japan
Thu 22 Sep 2016 11:00 - 11:25 at Conference Room 1 - Web Chair(s): Katsuhiro Ueno

F* is a language in the tradition of ML equipped with dependent types, monadic effects, refinement types and a weakest precondition calculus. Together, these features enable the F* programmer to prove functional correctness using a combination of automation via SMT solving and manual program proofs.

In the context of the greater Everest project, we are using F* to prove, build and deploy miTLS, a verified, efficient implementation of the Transport Layer Security (TLS) 1.3 protocol.

This extended abstract presents our work in progress. We are currently focusing our efforts on proving the memory safety and functional correctness of Elliptic Curve Cryptography (ECC) primitives, and on extracting this code to C. ECC primitives are a good candidate: they are modeled after the reference implementations in C. Therefore, they only exercise an imperative, first-order subset of F* that lends itself well to an efficient extraction to C.

Thu 22 Sep
Times are displayed in time zone: Osaka, Sapporo, Tokyo change

10:35 - 11:25: WebML at Conference Room 1
Chair(s): Katsuhiro UenoTohoku University, Japan
10:35 - 11:00
WebAssembly: high speed at low cost for everyone
11:00 - 11:25
Extracting from F* to C: a progress report
Jonathan ProtzenkoMicrosoft Research, Karthikeyan BhargavanINRIA, Jean-Karim ZinzindohouéINRIA, Abhishek Anand, Cédric FournetMicrosoft Research, Bryan Parno, Aseem RastogiMicrosoft Research India, Nikhil SwamyMicrosoft Research