Talia Ringer @TaliaRinger@types.pl

Cubes cubes cubes and more cubes

https://github.com/uwplse/pumpkin-pi/blob/evil-professor/plugin/coq/playground/equivalence_int_abs.agda#L479

After two weeks of letting myself try, fail, ask silly questions, and repeat, I finally feel very comfortable using Cubical Agda. Like actually. Wow

ELI5: Kan extensions

My students are stuck on a theorem in Cubical Agda and I'm not sure how to help them. It's here: https://proofassistants.stackexchange.com/questions/2017/paths-between-quotient-types-in-cubical-agda

And I tried to prove it, too, but in the a = [ pos zero ], b = [ neg zero ] case I could not find a proof that also satisfied the necessary definitional equalities (I found a congP application that in theory had the right type, but Cubical Agda yelled at me about some definitional equalities that were not satisfied). Since it's Cubical I have no idea how to find help with this, and so I am curious if type theory mastodon has ideas.

Anyone up to exchange ITP drafts for feedback?

Anyone down to give feedback on a paper draft sometime over the weekend? Fresh eyes would be good. Target audience is proof assistant researchers, especially those interested in certified compilation and in embedded program logics.

Question for a student: What venues are interested in work on reverse engineering neural network behavior? And what are the standards for that work at those venues?

For example, say we reverse engineer behavior for an interesting class of functions with strong motivation that reveal useful insights about the behaviors of a commonly used neural architecture, but we don't yet actually improve the architecture. Is this publishable anywhere?

Or must we also take it a step further and use our insights to improve performance? We plan to do this at some point, but it's a bit downstream.

You may have heard that Google laid off 12000 employees yesterday. I have created a Google Doc to crowdsource job openings and useful contacts for those 12000 employees. Please add anything you know of: https://docs.google.com/document/d/1g5kfdnOPNInmFPlwFS-7DBp7CsrlldzMIPMNk9nnaOQ/edit?usp=drivesdk

Are folks aware of any good resources that cover the basics of compiling recursive functions, both inefficiently and with the basic optimizations like tail call optimization? Just looking for an overview at a late undergrad or early grad level.

While I'm here, also, any resources on implementing recursive functions on a Turing Machine?

Can we build something that goes in the other direction? Like, we add a link to our Twitter on Mastodon, the it crawls various Mastodon instances and looks for people we follow on Twitter? The Muskito can't control this platform

Also, this is how my weekend is going so far. First time with COVID

ICYMI, Twitter just banned the posting of Mastodon usernames and links, including in profiles. Debirdify is dead, basically.