the arc of software bends towards understanding

## Equality, roughly speaking

In Software Foundations, equality is defined in this way: Even Coq's equality relation is not built in. It has (roughly) the following inductive definition. Inductive eq0 {X:Type} : X -> X -> Prop := refl_equal0 : forall x, eq0 x x. Why the roughly? Well, as it turns out, Coq defines equality a little differently […]

• January 30, 2014

## HoTT exercises in Coq (in progress)

I spent some of my plane ride yesterday working on Coq versions of the exercises in The HoTT book. I got as far as 1.6 (yeah, not very far, perhaps I should make a GitHub repo if other folks are interested in contributing skeletons. Don't know what to do about the solutions though). All of […]

• July 1, 2013

## (Homotopy) Type Theory: Chapter One

In what is old news by now, the folks at the Institute for Advanced Study have released Homotopy Type Theory: Univalent Foundations of Mathematics. There has been some (meta)commentary (Dan Piponi, Bob Harper, Andrej Bauer, François G. Dorais, Steve Awodey, Carlo Angiuli, Mike Shulman, John Baez) on the Internet, though, of course, it takes time […]

• June 24, 2013

## The Difference between Recursion & Induction

Recursion and induction are closely related. When you were first taught recursion in an introductory computer science class, you were probably told to use induction to prove that your recursive algorithm was correct. (For the purposes of this post, let us exclude hairy recursive functions like the one in the Collatz conjecture which do not […]

• April 27, 2013

## A Zerocoin puzzle

I very rarely post linkspam, but given that I’ve written on the subject of anonymizing Bitcoins in the past, this link seems relevant: Zerocoin: making Bitcoin anonymous. Their essential innovation is to have a continuously operating mixing pool built into the block chain itself; they pull this off using zero-knowledge proofs. Nifty! Here is a […]

• April 11, 2013

## A classical logic fairy tale

(Selinger) Here is a fairy tale: The evil king calls the poor shepherd and gives him these orders. “You must bring me the philosophers stone, or you have to find a way to turn the philosopher’s stone to gold. If you don’t, your head will be taken off tomorrow!” What can the poor shepherd do […]

• April 7, 2013

## An Interactive Tutorial of the Sequent Calculus

You can view it here: An Interactive Tutorial of the Sequent Calculus. This is the "system in three languages" that I was referring to in this blog post. You can also use the system in a more open ended fashion from this page. Here's the blurb: This interactive tutorial will teach you how to use […]

• May 22, 2012

## Chain Rule + Dynamic Programming = Neural Networks

(Guess what Edward has in a week: Exams! The theming of these posts might have something to do with that...) At this point in my life, I’ve taken a course on introductory artificial intelligence twice. (Not my fault: I happened to have taken MIT’s version before going to Cambridge, which also administers this material as […]

• May 30, 2011

## The return of Hellenistic reasoning

I recently attended a talk which discussed extending proof assistants with diagrammatic reasoning support , helping to break the hegemony of symbolic systems that is predominant in this field. While the work is certainly novel in some respects, I can't also but help think that we've come back full circle to the Ancient Greeks, who […]

• March 21, 2011

## Many-valued logics and bottom

I was flipping through An Introduction to Non-Classical Logic by Graham Priest and the section on many-valued logics caught my eye. Many-valued logics are logics with more than the usual two truth values true and false. The (strong) Kleene 3-valued logic, sets up the following truth table with 0, 1 and x (which is thought […]

• March 11, 2011