Embedding Prooforiented Programming Languages in F*
The material presented here is based on work by a large team of
people working on F*
and Project Everest
... thanks to everyone!
For questions about F* join the Everest Slack.

Lecture 1, Monday, June 14, Overview and Deeply Embedded Languages
 Overview of F*, its applications and deployments
 Basic functional programming with dependent types
Background reading:
Online Tutorial, Sections 1 and 2
 Basic demo: Factorial, lists, vectors OPLSS2021.Basic.fst
 Deeply embedded languages
 Warm up: Syntactic metatheory of the simply typed lambda calculus OPLSS2021.STLC.fst
 Vale: A Prooforiented Assembly Language (A lot of this material here was contributed by Chris Hawblitzel ... thanks Chris!)

Lecture 2: Tuesday, June 15: Shallow Embeddings of Effectful Languages
 Basic monadic effects
 Refined monadic effects
 Background reading
 Layered Indexed Effects: What F* implements today, much of it by Aseem Rastogi ... thanks Aseem!
 Some prior papers and history on Dijkstra monads:

Lecture 3: Wednesday, June 16: Layering Effectful Languages
 Low*: A shallow embedding of a subset of C in F*
 EverParse: A Prooforiented Parser Generator Layered on Low*

Lecture 4, part 1 and part2 : Thursday, June 17: Embedding a Semantics and Logic for Concurrency