Book details

Proof-oriented Programming in F*

Categories F*

This book introduces proof-oriented programming in F*, a dependently typed language that combines functional programming with program verification. It develops techniques for specifying and proving properties of programs, including functional correctness, effects, and verified implementations.