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

mlfamilyworkshop-2016-papers
10:35 - 11:25: ML - Web at Conference Room 1
Chair(s): Katsuhiro Ueno
mlfamilyworkshop-2016-papers147453330000010:35 - 11:00
Talk
Pre-print
mlfamilyworkshop-2016-papers147453480000011:00 - 11:25
Talk
Pre-print