Pinned toot

Hi everyone! I'm new here so, time for an ?

I'm an M2 student living near Paris, interested in :
• Type systems (Curry-Howard ❤ )


Today I program a lot in , because French research teams use it a lot, but I also use and I like dependently-typed languages like .

For some work I have done on the OCaml compiler you can check out otini.chnik.fr/.

Glad to be here :)

work-related negativity 

otini boosted
otini boosted
otini boosted

More cuuuuurves 

otini boosted

Lecture by Magnus Myreen: a fast and verified interactive theorem prover

Very cool!

otini boosted
otini boosted

Haskell question, C bindings and c2hs 

Just arrived at the Marktoberdorf Summer School in Germany. :)

I'm going to a summer school and there will probably be stuff to install, and I'm afraid already

otini boosted

There isn't even a entry for the newer `nix` command in the Nix documentation, seriously this documentation problem is way worse than I thought

This is one of these days where I regret having installed NixOS on my work laptop.

question: trying to install Wolfram Engine from the script/archive downloadable from their website, this is not going well. Is there any way to have '/bin/bash', but also '/bin/rm', etc. to exist and be usable by the script? Yes, I know they shouldn't be using these hardcoded paths.

otini boosted
otini boosted

@merricat @otini ditto. In the same manner Haskell uses ⊥ (UP TACK) to denote bottom†.

† wiki.haskell.org/Bottom

Reading a journal paper, my supervisor is cited in it. It's normal but it feels weird ^^

Wondering why many people denote \( σ_{\dashv} \) the last element of the sequence σ. Is it because \( \dashv \) looks a bit like −1? 😄

Thunderbird segfaulting, probably yet another Nix-related environment issue that I have no idea how to fix, yayyyyy

otini boosted
Show more
Functional Café

functional.cafe is an instance for people interested in functional programming and languages.