Tiago Cogumbreiro

Pleased to announce that the third edition of my PL book, PLAI, is finally available on paper! Same price as it's been for 20 years (-:. Also made it available on Kindle EPUB, and a few other options. (Always free options, of course.) Enjoy!
www.plai.org

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...

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 ...

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.

PSA! Please share around! Due to a limited number of submissions, we're extending the OCaml Workshop deadline by a week to July 10th AoE!

Functional programmers! Heed my call! We need your submissions!!

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.

I migrated from a Coq 8.19 + coq_makefile to dune + Rocq 9.0, assisted with Claude Code. It was a great experience, as there are so many little (tedious) details, from opam, Git, dune, etc.

gitlab.com/cogumbreiro/...

If you are a functional programmer in Asia, then it is your obligation, nay your existential imperative to submit to the OCaml workshop this year

SPLASH/ICFP is in Asia this year and we have fewer submissions from the western folks because of the distance

Submit!!! Plsplsplsplsplz

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

I'm learning to use Claude code for my Rocq proof development. First rule of fight club: If ANY proof attempt fails to compile, STOP IMMEDIATELY.

Otherwise, Claude just exhausts my tokens.

If I may ask, what tolling are you using?

Original post: types.pl/@liamoc/1145...

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.

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...

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.

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...

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.

umb-svl / faial · GitLab GitLab.com

For some definition of cool, Faial is a static verifier of CUDA kernels written in OCaml. Self plug disclaimer.

gitlab.com/umb-svl/faial

Forgot to add that the accompanying gist includes a brief and step-by-step tutorial. The screenshot shows the conclusion, not the story.

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

Here's a short demo I gave to my students on proving a simple result without ltac (functional style). #Rocq

gist.github.com/cogumbreiro/...

Paper reviewing, 5 out of 10 done, 2 weeks to go. 🥵

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 ...

Z3 builds in Dune Developer Preview! <3

Love it. I can't wait to have time to make our project build with the new dune!

#ocaml

github.com/ocaml/dune/i...

@ NEPLS

OCaml cross-compilation: an experiment OCaml has no official solution to cross-compilation, with many disparate options developed for different use cases. In this article I describe my own experiments with cross-compilation and attempts to...

Cross-compiling OCaml

www.chrisarmstrong.dev/posts/ocaml-...

This is exciting progress! I'm crossing my fingers to see Z3 in that list soon.

Your research statement is engaging. It was a really compelling front page.

Agreed!

I really enjoy reviewing papers. I am reviewing this paper for OOPSLA. I understood the intro. The overview section started by making me giggle and the problem statement was clear as day. I'm pumped to discover what comes next. Hopefully, a strong accept.

ECS in #OCaml featuring extensible variant types and GADTs edwardwibowo.com/blog/ocaml-g...

new book on session types just dropped!

www.cambridge.org/us/universit...

GitHub - Octachron/roguetype: The first ever roguelike written in the OCaml type system The first ever roguelike written in the OCaml type system - Octachron/roguetype

Finally, a roguelike powered by OCaml's type system!

github.com/Octachron/ro...

Unite! Visiting Professorship Programme at TU Darmstadt (2nd Call) is open for applications until 31 March.

🔗 More information: tinyurl.com/3ppnw75f

#TécnicoLisboa #ULisboa