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.

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 Proof-oriented Assembly Language (A lot of this material here was contributed by Chris Hawblitzel ... thanks Chris!)
    - Background reading: Vale at POPL '19
    - Slides
    - OPLSS2021.Vale.fst Basic semantics of MiniVale, a small assembly langugage with manual proofs
    - OPLSS2021.ValeVC.fst An efficient VC generator for MiniVale

Lecture 2: Tuesday, June 15: Shallow Embeddings of Effectful Languages
- Basic monadic effects
  - Basic state OPLSS2021.BasicState.fst
  - Combining state and nondeterminism OPLSS2021.NDS.fst
- Refined monadic effects
  - Dijsktra monad for state OPLSS2021.DijkstraMonads.fst (Thanks Guido Martinez!)
  - Custom abstractions: Noninterference and Information flow control OPLSS2021.IFC.fst
- 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*
  - Simple demo of Low*: OPLSS2021.MemCpy.fst
  - Background reading:
    - Low* @ ICFP '17
    - A User Manual to Low* and KReMLin, written by Jonathan Protzenko ... thanks Jonathan!
    - Lots of provably correct and secure code built in Low* and deployed in many places, including ValeCrypt, EverCrypt, and HACL*
- EverParse: A Proof-oriented Parser Generator Layered on Low*
  - Slides
  - Demo: TCP Header FormatsTCP.3d
  - Background reading:
    - EverParse @ USENIX '19
    - EverParse manual, by Tahina Ramananandro ... thanks Tahina!
    - EverParse blog

Lecture 4, part 1 and part2 : Thursday, June 17: Embedding a Semantics and Logic for Concurrency
- Simple, total concurrency, with basic action trees: OPLSS2021.ParTot.fst
- Layering total concurrency on top of state and nondeterminism: OPLSS2021.ParNDS.fst
- Refined semantics with a generic separation logicOPLSS2021.ParDiv.fst
- The full semantics of SteelCore (Thanks Aseem!)
- Background reading:
- Steel examples, with a lot of the proof automation due to Aymeric Fromherz ... thanks Aymeric!