Pinned toot


I am a computer scientist interested in , concurrency theory applied to parallel systems.

My main research project deals with verifying safety and performance properties of kernels.

I write code for research mainly in and .

I am passionate about teaching. I am currently using Racket to teach functional programming and Coq to teach Intro to Theory of Computation.

I use this to share my own research findings, papers I like, and software that I find fun.

PS: I just migrated from and I think I lost my posts.

Two updates about the 16th Interaction and Concurrency Experience (ICE 2023) workshop:
1. We are thrilled to announce that Adrian Francalanza ( has accepted to be our first guest speaker, and
2. The deadlines have been extended by ~2 weeks.

Check out !

Show thread

#CallForContributions #ThEdu23 (Theorem proving components for Educational software) "brings together experts in automated deduction with experts in education in order to further clarify the shape of a new software generation and to discuss existing systems" #ATP #CSEd #CSEducation

Really pleased to have pushed out of beta. 130+ videos about #ocaml dating back to 2010 (and would like to get more historical ones) all available via PeerTube/ActivityPub.

Teaching my first module in this semester: thunks and promises, with a hint of polymorphism.

So far, I really enjoyed the language. I love that using TypedRacket code in Racket is so seamless. Types being contracts just feels so good.

My biggest surprise right now is pattern matching with "match"

To appear in FMSD'23: *Memory Access Protocols:
Certified Data-Race Freedom
for Kernels*. Key new points vs our CAV21 publication: full discussion of Coq proofs, cleaned up definitions, gentler introduction of the defs+examples.

Note to self, the expression x <= y is written in Prolog as x =< y, even though x >= y is written as x >= y. Something something parsing?

Note to self: with 2FA, my phone should not be the only way to authenticate. I bought a new phone and almost locked myself out of my school's authentication castle.

If you're using Holbert in the classroom, please tell us! So far, I'm aware of two classes in which it is/will be actively used and two more where instructors tell me they plan to use it at some point but haven't developed the materials yet.

New #Futhark mugs. We hand out these to students who get a top grade in our parallel programming courses.

Happy to release the first version of smlfmt, a formatter for Standard ML.

This has been a hobby project for a while now -- I remember starting work on the parser while visiting my sister for Thanksgiving in 2020. Back then, I was just curious about parsing and wanted to give it a shot. But then a few folks from CMU got interested in the project and suggested that we could turn it into a code formatter. Big thanks to all the Project Savannah folks for your contributions, suggestions, and support!

I had a great time working on this over winter break. Now it's time to get back to research!

Holbert 0.5.1 has been released! Many minor things have been improved, but highlights are:
- Footnote/reference popups
- Links and image embedding (not added to help yet)
- A basic presentation mode that shows a document as a slideshow
- Auto-renames variables in goals to avoid confusing shadows
- Very basic infix input syntax support using "Notation", but does not yet support associativity or precedence settings.

After a slight delay due to winter holidays, the December release of Functional Programming in Lean is out, featuring a new chapter on applicative functors:

Follow up: the winning logic parameters in terms of more answers given and also in terms of faster answers as an aggregate were AUFLIRA and AUFNIRA. This is surprising to me, since the formula we generate do not have arrays.

- AUFLIRA: "Closed linear formulas with free sort and function symbols over one- and two-dimentional arrays of integer index and real value. "
- AUFNIRA: "Closed formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value. "

Show thread

I love learning more about the subtleties of SAT solving. In one of our analysis, we are maximizing a numeric expression and we wanted add support for bit-vectors. The solver (Z3) started giving weird answers only when using bit-vector numerals. The problem is that maximization has no notion of bit-vector signedness.

StackOverflow was invaluable as usual:

Varying the logic parameter to see what works best in our DRF analysis.

Show older

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.