The American Mathematical Society wrote a memorial notice on Vladimir Voevodsky where, among others, his contributions to type theory are considered.

# Category Archives: ephemera

## Gentle Introduction to Homotopy Type Theory

### Status

If you’re a programmer and you want to understand what is homotopy type theory about, Dan Licata has a talk on the topic.

## Interactive Theorem Proving

### Status

Interactive theorem proving such as one provided by Agda is so empowering. The help provided by the compiler while interactively developing a proof is invaluable. Types guide you to a solution at every single step.

## Web Page is Back

### Status

After an interruption today, my web page is back online.

## Comparison of Type Theory and Set Theory

### Status

If you ever wondered how are types different from sets or more generally what is the difference between type theory and set theory, I recommend watching a talk by Thorsten Altenkirch at Foundations of Mathematics: Univalent Foundations and Set Theory 2016.

## Competing Against Wadler

### Status

I applied to give a theorem proving seminar at a university. They chose Philip Wadler as a lecturer over me. That must have been close! Still, so disappointed…

## Google and its own Software

### Status

Isn’t it ironic – Google’s own proprietary Meet service isn’t supported in Chromium, a web browser by Google, but it is supported in Firefox, a web browser by Google’s competitor.

## Giving Talk on Productive and Terminating Functions

### Status

Today I’ll be giving a talk on terminating and productive functions as part of the Lambda Zagreb Meetup group. This talk will be very familiar to my upcoming Lambda Days 2019 talk.

## Structurelessness

### Status

Jo Freeman has an interesting essay on the tyranny of structurelessness. The lack of structure implies the lack of power to act.

## Speaking at Lambda Days 2019!

### Status

I’m happy to announce that I’ll be speaking at the Lambda Days 2019 conference! I’ll be giving a talk on function totality.