Amélia Liao 🍊
amy@types.pl
<p>Main author of the 1Lab and spooky cubical ghost haunting your citrus trees. Charitably describable as "hinged"</p>
Posts
-
Post #2992388
how it feels to be responsible for the termination checker
-
Post #2044537
We're announcing Mikan: a proof assistant for cubical type theory, forked from the Agda codebase. Note: you can also read this announcement as a Gist. The Agda developers have recently proposed codifying their official stance on LLM-generated contributions: they are "concerned about the negative effects of large language models (LLMs) on many individuals, our society, and our planet", but refuse to take any concrete action to address their own contribution to these. They have jud...
-
Post #1437802
mlg
-
Post #802319
(Bool → String) ∷ Nat ∷ []
-
Post #674471
boost this cat with nontrivial delay