rntz

@rntz@recurse.social
632 Followers
288 Following
1.7K Posts

Michael Arntzenius irl. PL design, math, calligraphy, &c.

Postdoc at UC Berkeley working on incremental computation, DB ⋈ FP, etc.

Webhttp://www.rntz.net
Twitterhttps://Twitter.com/arntzenius
cohostrntz
emaildaekharel@gmail.com
rntz4d ago
the right notion of equality on existential types should be something like bisimulation, right? is there a standard reference for this?
rntz6d ago

I've heard the argument made that hashtable lookup is only constant-time if memory access is O(1), but it's actually O(log n).

But isn't it actually O(∛n)? In a given time t, I can reach at most O(t³) space, limited by the speed of light.

Show threadrntzJun 21

I might expect rules like the following:

Γ ⊢_m e : T_n A
-------------------
Γ ⊢_{mn} run e : A

Γ ⊢_{mn} e : A
----------------------
Γ ⊢_m thunk e : T_n A

Γ ⊢_m e1 : A
Γ, x:A ⊢_n e2 : B
------------------------------
Γ ⊢_{mn} let x = e1 in e2 : B

rntzJun 21
Is there a type system using graded monads that puts a grade on the _typing judgment_, not just on the monad type? I swear I saw something like this once, but can't find it. @dorchard ?
rntzJun 21
Martin EscardoJun 20

I am happy to announce that my colleague Paul Blain Levy has won the Alonzo Church Award.

https://siglog.org/winner-of-the-2025-alonzo-church-award/

Winner of the 2025 Alonzo Church Award – ACM Special Interest Group on Logic and Computation

rntzJun 21
Ivan ReeseJun 19
Hey Germans, please come up with a word that means "the fear of typing `return` vs `shift-return` because you don't know which inserts newline and which sends the message"
rntzJun 20
\title{Finite functional programming}
\title{(Finite function)al programming}
\title{Toward finite functional programming}
\title{Finite functional logic programming}
\title{Functional programming with support}
\title{Supporting functional programming} % lol
\title{Graded, grounded functional logic programming}
\title{Functional logic programming graded \& grounded}
\title{Logic programming with finite functions}
\title{Logic is functions with support}
\title{Logic, functions \& support}
rntzJun 20
Show threadRobJun 20

I had them write reflections on the third assignment experience (asking them to write reflections with their brains and not ChatGPT, I estimate about 80% compliance), and based on that reflection and in-class discussion I set a pretty permissive AI policy for the group project.

Some of y'all might find that policy an interesting artifact: https://neu-se.github.io/CS4530-Summer-2025/policies/group-project-ai-policy/

AI in the Group Project | CS4530, Summer 2025

rntzJun 19
redmp (EDITED)Jun 18

Hey! Our paper about the ECS pattern was accepted to OOPSLA/Splash2025! Thank you to my co-authors: @Twisol, @jmct, and @lindsey!

We formalized the ECS pattern, used the formalism to prove when (concurrent) ECS programs are deterministic despite scheduler-nondeterminism, and then showed that prominent existing frameworks disallow lots of ECS programs that *would* be deterministic.

A draft of "Exploring the Theory and Practice of Concurrency in the ECS Pattern" is at https://curious.software/plr/static/2025-03_ecs-conc-theory-practice.pdf

rntzJun 18
Show threadConor Mc BrideJun 18
Proofs are about why a small type isn't empty. Programs are about exercising taste in a big type's shop.