lightandlight / cbpv

A usable type system for call by push-value

About Me

He/Him

I'm a programmer living in Brisbane, Australia.

I enjoy building things that make people more effective. I'm particularly passionate about developer tooling because it contributes to a cycle of self improvement within software development.

Projects

My 'academic' roots lie in programming language theory and type theory. As a result, all of my biggest personal projects have been programming languages, or programming language related. See my 'pinned' repositories for a selection of my favourite projects.

cbpv's Issues

Question about AlephNull example

The AlephNull example codata AlephNull where { next : AlephNull } by name would seem to have countably many inhabitants. But is it not the Unit type, at least up to bisimilarity?