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*

Index

Index

© Copyright 2020, Microsoft Research.

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