Embedding Proof-oriented Programming Languages in F*

Oregon Programming Language Summer School (OPLSS 2021)

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.
  1. Lecture 1, Monday, June 14, Overview and Deeply Embedded Languages


  2. Lecture 2: Tuesday, June 15: Shallow Embeddings of Effectful Languages


  3. Lecture 3: Wednesday, June 16: Layering Effectful Languages


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