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
For instance, I noticed that the results I ask my students to prove are much simpler at the end of the course than at the beginning, so teaching in reverse would simplify what needs to be taught in terms of proof theory.
November 25, 2025 at 8:17 PM
For instance, I noticed that the results I ask my students to prove are much simpler at the end of the course than at the beginning, so teaching in reverse would simplify what needs to be taught in terms of proof theory.
I love that. It's something I've been meaning to do in a while, but b/c I followed Sipser I started from the usual way, and I haven't had the energy to do rethink the presentation. But good to know all of these great resources. Thanks for sharing these links!
November 25, 2025 at 8:13 PM
I love that. It's something I've been meaning to do in a while, but b/c I followed Sipser I started from the usual way, and I haven't had the energy to do rethink the presentation. But good to know all of these great resources. Thanks for sharing these links!
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...