Lectures on the Curry-Howard Isomorphism Chapter 2 (1/3)

Read a third of Chapter 2. It was less dry! For Natural Deduction they define the context as a set, so they did not need to discuss a permutation theorem. They did mention the substitution theorem. They next part of the chapter will talk about algebraic semantics and Heyting algebras, so that should be fun as well. Pretty excited about returning to some of the material from my Universal Algebra course.

Thoughts on WebAssembly

WebAssembly does not feel like an assembly language and there does not seem to be any plans to make it more like one. I feel that functional languages will always have a second class status on the web because we don’t have access to enough low level primitives to add our own garbage collectors.

Reference Counting

There seem to be several ways of thinking about reference counting. One is actual counts. Another way to think about the reference count is as an approximation to some kind of a remembered set.

Compiling without Continuations

Recently read the “Compiling without Continuations” paper for the n^th time. Was still a fun read! I really like the IR in that paper – it’s simple and cute. Personally, I think join points are useful if exposed to the user.

Lectures on the Curry-Howard Isomorphism Chapter 1

Read the first chapter of “Lectures on the Curry-Howard Isomorphism”. It was a very technical introduction to the untyped lambda calculus. Although the theory seems very robust, it was somewhat dry. The book was recommended to me by someone who held it in high regard, so I think the later chapters will be more exciting.

Newer