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/

Outline

No outline is available

Content is not yet available

Nikhil Swamy (nikhil.swamy)

0
Author

No biography is available.

For a complete view of this profile, including education, work experience and developer information, you need to be logged in and have a subscription.

Nikhil's upcoming trainings

No events

Nikhil's past online trainings

Nikhil's blog posts

IntelliFactory Offices Copyright (c) 2011-2012 IntelliFactory. All rights reserved.
Home | Products | Consulting | Trainings | Blogs | Jobs | Contact Us
Built with WebSharper