@ionchy I'm sorry, that is a feature that's only available to premium Agda members.

sized types 

WAIT now that Agda has polarity annotations you could do proper subsizing!! omg
You could probably also do subsizing now ignoring parameters with inductives as covariant and coinductives as contravariant, idk why Agda doesn't have that

Show thread

Twitter is no longer enforcing its Covid-19 misinformation policy, per this message on its transparency site transparency.twitter.com/en/re

sized types 

idk why throughout my thesis I was so confident strict positivity checking was completely separate from termination checking. if I had bothered to write out this simple example I would've seen there's obviously something funky going on

Show thread

AI bros: AI is already sentient, outperforms humans in every task!

Amazon: since you bought a dozen books on abstract algebra, here are these study guides for pre-algebra we thought you might like. They all have "algebra" in the title!

LinkedIn automated recruiting: how would you, tenured faculty member in CS, like to apply to this summer internship in software development for junior undergraduates? Your resume lists a degree in computer science!

Various automated recruiting emails: we see you are a professor, here are 10 open faculty positions in fields you know nothing about. They all say "professor" in the ads!

GitHub Copilot: <always suggests repeating the same paragraph I just wrote, but with made-up citation keys instead of the ones I used>

Meta's Galactica model for summarizing research: <makes up random crap when asked for an overview of basically anything>

I realize there are folks working hard on these things and plenty of smart people I admire have built really impressive systems but... the gap between the hype and reality is really absurd, even by tech industry standards.

Aww yeah the Liquid Types folks (few of whom I can find on the fedi yet, sadly) have started hacking Rust also


Want to help redesign one of the most popular and widely-used tools for researchers?

Zotero is hiring a designer: zotero.org/jobs/ui_designer

Would do it if I could. Ideal for someone else who has great UX / product design chops.

I am looking for two PhD students to work with me at KIT (Karlsruhe, Germany) on topics related to accessibility, technology, and self-determination. Fully funded positions for four years (TV-L 13). Knowledge of German is not strictly required but a plus, previous experience with methods of co-design or in running focus groups would be very much appreciated. If you have questions - please ask!

@vollmerm I’ve seen the assetion that lisp having the simplest syntax across languages has resulted in it having the most complex indentation rules


Today's quasi-incoherent ranting about HoTT is brought to you the last chapter of my thesis being blocked by a proof about transport

#MULCIA: Fully funded PhD positions in PL theory and interactive theorem proving at Heriot-Watt University in Edinburgh. bit.ly/3V3pIEh #PhD #CompSci

#TypedRacket has just got way more powerful. The following code gets typechecked as is:

(: eval-with (All (a) (-> (VariableMapping a) Any AnyValues)))
(define (eval-with ht expr)
  (parameterize ([current-namespace (make-base-namespace)])
    (for ([(x val) (in-hash ht)]) (namespace-set-variable-value! x val))
    (eval expr)))

Six months ago I spent a couple days trying to get eval-with to typecheck, only to get the answer on the mailing list that Typed Racket couldn’t do that. Well now not only can it do this, it also has dependent types!

I’m extremely excited 😍

For those who want a good PL read, I can recommend Michael Arntzenius' PhD Thesis (available at rntz.net/files/thesis.pdf ). The level of detail included in the wonderful narrative made it a really easy read (for me).

I don't even care very much about Datalog, but all the techniques deployed, in the manner they were deployed, captivated me.

(Not sure of rntz is on here?)

Come work with us!!

We are thrilled to announce the opening of 17 (!) #phd and #postdoc positions in our national research program Public Values in the Algorithmic Society algosoc @algosoc

DL: January 16, 2023


Show older

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