Tiago Cogumbreiro

@forkjoin.bsky.social

127 Followers 284 Following

Associate professor @ UMass Boston | https://cogumbreiro.github.io/ | Faial is a verifier for #CUDA and #WebGPU written in #OCaml https://gitlab.com/umb-svl/faial #ocaml #rocq

A screenshot of Egg's Getting Started guide ported to an OCaml API.

Screenshot of git history showing 14 commits.

A screenshot of OCaml code showing some JSON deserialization code.

A screenshot of `proof-ls` in action, showing a proof state.

**CRITICAL RULE**: If ANY proof attempt fails to compile, STOP IMMEDIATELY.

`nat_ind (fun x => x + 0 = x) eq_refl (fun n IH => eq_S (n + 0) n IH)`

A screenshot of the game unpacking.

Small excerpt in Rocq showing the 3 tactics in action.

Source: Nielson's "A Hoare-like proof system for analysing the computation time of programs," 1987.

A few inference rules generated from the OCaml code.