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 :)

otini boosted
otini boosted

Peut-on en déduire qu'il faut baisser le salaire des dirigeants pour gagner des parts de marché ? calpaterson.com/mozilla.html

(fr) Loi de programmation pluriannuelle de la recherche 

Elle est passée en première lecture à l'Assemblée. Voici un communiqué des directeurs de laboratoire qui explique pourquoi c'est une mauvaise loi qui approfondit une mauvaise politique : sauvonsluniversite.com/spip.ph

(Le mérite revient à @lesly pour l'avoir déniché)

otini boosted
otini boosted
otini boosted

Aujourd’hui, c’est la Journée Internationale du Logiciel Libre ! On va donc parler de comment Zeste de Savoir participe au logiciel libre, de par sa structure comme de par son contenu. zestedesavoir.com/ #JILL

otini boosted
otini boosted

Give someone a program, you frustrate them for a day; teach them how to program, you frustrate them for a lifetime. -- David Leinweber

otini boosted

Eh folks, any suggestion regarding a modular arithmetic in #Coq? I know CompCert has one, but it is not standalone as far as I am aware, so it’s a bit less easy to use.

Would love to hear your though, thanks!

logic question 

I taught my first class in propositional logic today and one of the students asked a question I couldn't answer.

I had just presented De Morgan's laws and double negation elimination, and call them (rather informally) “calculus rules”.

They asked whether all tautologies could be transformed into the constant formula “TRUE” by applying a sequence of “calculus rules”.

I must say I don't know the answer. I know that every formula can be converted into either CNF or DNF, but I don't whether the CNF or DNF of a tautology is necessarily “TRUE”.

otini boosted

J'ai la preuve qu’SFR a communiqué mon mail à des spammeurs. Leur délégué à la protection des données recevra bientôt un mail de ma part.

Idem pour le numéro de téléphone.

otini boosted
otini boosted

Funkwhale 1.0 is out 🎉

As usual, the full changelog is available at docs.funkwhale.audio/changelog,. New features include:

- A brand new search page
- It's now possible to launch a scan from the UI
- Themes and language are now persisted accross sessions
- A new plugin system, with a scrobbler plugin that works with Last.fm and MusicBrainz

We're thankful to the contributors to this release, as well as all our supporters, backers and members of the community who have been with us for five years!

We wish you a happy upgrade!

otini boosted

#PeerTube 2.4 is out!
Improved moderation tools, better playlist management, an annotations plugin and many more new features!
Check it all out here: joinpeertube.org/en_US/news#re

otini boosted
otini boosted

Tricky language, French. It took me four goes to get this one right.

otini boosted

There used to be apples which fell down and others which flew up into other space.
Those which flew up did not get to reproduce. So apples evolved to fall down.

otini boosted

J'ai pêché dans le flux de Cory Doctorow un petit texte qui risque d'intéresser du monde ici. Ça parle d'un article scientifique qui met à l'épreuve une des hypothèses fondamentales de l'idée de méritocratie, selon laquelle la fortune d'une personne est proportionnelle à son "talent". Ça se passe ici : pluralistic.net/2020/08/23/vis.

Show more
Functional Café

The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!