Progressive F# Tutorials NYC / F*: Verifying ML programs with dependent types

Please RSVP for instructions on how to join the event.

Description

The functional-first style encouraged by F# rules out many simple bugs, but we’ve all struggled with deeper algorithmic bugs lurking in our programs. F* is a new research language from Microsoft Research that allows you to formally prove the full functional correctness of code written in a strict, higher-order, stateful programming language, e.g., programs in idiomatic F#, Caml and related languages. This tutorial will give you an overview of F*, including an introduction to the theory of dependent types that's at the heart of F* and the automated theorem-proving technology that underlies its implementation. You will write and formally prove the correctness of several small algorithms, data structures, and web programs. Get started with F* already! An interactive tutorial:http://rise4fun.com/FStar/tutorial/guide Links to several research papers and a compiler download: http://research.microsoft.com/en-us/projects/fstar/
IntelliFactory Offices Copyright (c) 2011-2012 IntelliFactory. All rights reserved.
Home | Products | Consulting | Trainings | Blogs | Jobs | Contact Us | Terms of Use | Privacy Policy | Cookie Policy
Built with WebSharper

Logging in...