5 open source projects by tchajed

Tricks you wish the Coq manual told you

Library to create Coq record update functions

Ltac2 tutorial

We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic.

Goose converts a small subset of Go to Coq