Tiago Cogumbreiro
@forkjoin.bsky.social
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
Haha I need to try that out. I've seen so many cool examples of DSLs in Lean
November 18, 2025 at 7:48 PM
Haha I need to try that out. I've seen so many cool examples of DSLs in Lean
The tool is all implemented in OCaml. The monadic-design pattern of parsing JSON comes from what I learned in Faial <https://gitlab.com/umb-svl/faial/> and I think it looks neat.
October 25, 2025 at 6:28 PM
The tool is all implemented in OCaml. The monadic-design pattern of parsing JSON comes from what I learned in Faial <https://gitlab.com/umb-svl/faial/> and I think it looks neat.
The output is Markdown-formatted and the tool can figure out your Rocq project. I've been using this to help Claude Code help me, with some success. I have some scratch files in the project, including playing around with Fleche, but I haven't figured that code base yet.
October 25, 2025 at 6:24 PM
The output is Markdown-formatted and the tool can figure out your Rocq project. I've been using this to help Claude Code help me, with some success. I have some scratch files in the project, including playing around with Fleche, but I haven't figured that code base yet.
Reposted by Tiago Cogumbreiro
decoders library is quite elegant, esp if your format is absolutely disgusting
(source used it to parse the activitypub spec, the most underspecified and broken format known to humankind)
github.com/kiranandcode...
(source used it to parse the activitypub spec, the most underspecified and broken format known to humankind)
github.com/kiranandcode...
ocamlot/lib/activitypub/decode.ml at d677ae6b208074660811dc9120e6b90353e7f338 · kiranandcode/ocamlot
An Activitypub server in OCaml! Contribute to kiranandcode/ocamlot development by creating an account on GitHub.
github.com
July 17, 2025 at 6:31 PM
decoders library is quite elegant, esp if your format is absolutely disgusting
(source used it to parse the activitypub spec, the most underspecified and broken format known to humankind)
github.com/kiranandcode...
(source used it to parse the activitypub spec, the most underspecified and broken format known to humankind)
github.com/kiranandcode...
Progress here: github.com/ocaml/dune/i...
Dune Developer Preview (Sept-28-2024) fails to build z3 · Issue #10970 · ocaml/dune
Expected Behavior I would like to migrate my project to Dune developer preview. Actual Behavior dune build is unable to compile the package z3. See point 4 below for output. Reproduction 1. Create ...
github.com
July 14, 2025 at 8:28 PM
Progress here: github.com/ocaml/dune/i...
Turns out, I forgot to run `dune pkg lock` and z3 doesn't work with Dune Preview 😭
I managed to advance a bit further by changing Z3's lock file, but since I have no idea of what I'm doing, z3 then failed in the linking stage.
I managed to advance a bit further by changing Z3's lock file, but since I have no idea of what I'm doing, z3 then failed in the linking stage.
July 14, 2025 at 8:28 PM
Turns out, I forgot to run `dune pkg lock` and z3 doesn't work with Dune Preview 😭
I managed to advance a bit further by changing Z3's lock file, but since I have no idea of what I'm doing, z3 then failed in the linking stage.
I managed to advance a bit further by changing Z3's lock file, but since I have no idea of what I'm doing, z3 then failed in the linking stage.
Having Claude keep tabs of what was done and then generate the migration notes was invaluable. I would've forgotten all the steps otherwise. Humans and tools can use the guide and I already used it to have Claude migrate another project without further input.
June 29, 2025 at 3:19 PM
Having Claude keep tabs of what was done and then generate the migration notes was invaluable. I would've forgotten all the steps otherwise. Humans and tools can use the guide and I already used it to have Claude migrate another project without further input.
If I may ask, what tolling are you using?
May 29, 2025 at 1:46 PM
If I may ask, what tolling are you using?
Reposted by Tiago Cogumbreiro
Oh, defo you should! I am sad that I don't currently have any research actively working on lean at the moment because programming in it is honestly like working in the language of my dreams; I can truly extend it as much and as often as I want to fix any pain points
github.com/kiranandcode...
github.com/kiranandcode...
GitHub - kiranandcode/LeanTeX: Write LaTeX presentations directly from Lean4~
Write LaTeX presentations directly from Lean4~. Contribute to kiranandcode/LeanTeX development by creating an account on GitHub.
github.com
May 21, 2025 at 4:37 AM
Oh, defo you should! I am sad that I don't currently have any research actively working on lean at the moment because programming in it is honestly like working in the language of my dreams; I can truly extend it as much and as often as I want to fix any pain points
github.com/kiranandcode...
github.com/kiranandcode...
So cool! You're making me want to play with Lean 👀
May 20, 2025 at 8:56 PM
So cool! You're making me want to play with Lean 👀
Yes, we use ocaml's binding of z3 directly. We have used the stdin+smtlib in the past, but for our use case using the API works quite well and it is simpler to package.
For libclang we have use the stdin approach, which is not ideal. I haven't tried the llvm opam package, but it appears outdated.
For libclang we have use the stdin approach, which is not ideal. I haven't tried the llvm opam package, but it appears outdated.
May 15, 2025 at 12:35 PM
Yes, we use ocaml's binding of z3 directly. We have used the stdin+smtlib in the past, but for our use case using the API works quite well and it is simpler to package.
For libclang we have use the stdin approach, which is not ideal. I haven't tried the llvm opam package, but it appears outdated.
For libclang we have use the stdin approach, which is not ideal. I haven't tried the llvm opam package, but it appears outdated.
Yes, we have a few papers on the subject of the verification (data-race analysis). Our latest is this one at OOPSLA: dx.doi.org/10.1145/3689...
Ah, thanks for the heads up, I will try to submit something.
Ah, thanks for the heads up, I will try to submit something.
Sound and Partially-Complete Static Analysis of Data-Races in GPU Programs | Proceedings of the ACM on Programming Languages
GPUs are progressively being integrated into modern society, playing a pivotal role
in Artificial Intelligence and High-Performance Computing. Programmers need a deep
understanding of the GPU programm...
dx.doi.org
May 15, 2025 at 12:28 PM
Yes, we have a few papers on the subject of the verification (data-race analysis). Our latest is this one at OOPSLA: dx.doi.org/10.1145/3689...
Ah, thanks for the heads up, I will try to submit something.
Ah, thanks for the heads up, I will try to submit something.