Embedding Proof-oriented 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
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!)
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 Proof-oriented Parser Generator Layered on Low*
Lecture 4, part 1 and part2 : Thursday, June 17: Embedding a Semantics and Logic for Concurrency