Proof-Oriented Programming in F*

Contents:

  • Structure of this book
  • Introduction
  • Programming and Proving with Total Functions
  • Representing Data, Proofs, and Computations with Inductive Types
  • Modularity With Interfaces and Typeclasses
  • Computational Effects
  • Tactics and Metaprogramming with Meta-F*
  • Pulse: Proof-oriented Programming in Concurrent Separation Logic
  • Under the hood
Proof-Oriented Programming in F*
  • Search

© Copyright 2020, Microsoft Research.

Built with Sphinx using a theme provided by Read the Docs.