## Leaving the Nest: variables with interleaving scopes

A paper [PDF] with this title, co-written with Jamie Gabbay and Daniela Petrişan, will appear in Computer Science Logic (CSL 2015). Actually the full title is Leaving the Nest: Nominal techniques for variables with interleaving scopes. The “nominal techniques” part is in reference … Continue reading

Posted in programming languages | 1 Comment

## Inventing an algebraic knot theory for eight year olds (V)

Towards Equations We finally reconvened our maths club after a mid-term break (children not available) combined with the university exams period (me not available). I correctly assumed nobody remembered anything we talked about before. At least not in detail. Also, … Continue reading

## Types: computation vs. interaction

Type Theory is at the moment the workhorse of programming language theory. It is an elegant, clever and incredibly useful framework for thinking about programming (for full disclosure, I have written several papers with the word “type” in the title). … Continue reading

Posted in programming languages | 1 Comment

## Inventing an algebraic knot theory for eight year olds (IV)

Equations Here is a quote that captures the ethos against which our maths club militates: We take other men’s knowledge and opinions upon trust; which is an idle and superficial learning. We must make them our own. We are just … Continue reading

Posted in teaching | 1 Comment

## Inventing an algebraic knot theory for eight year olds (III)

Unlike previous posts, this one precedes the math club meeting. The reason is that we need to tighten some loose ends in our emerging knot theory notation. The first two meetings (I and II) were all about exploring knots and ways to describe them using … Continue reading

Posted in teaching | 1 Comment

In previous posts I gave arguments against the apparently widely held belief, at least amongst readers of this blog, that all mental states and phenomena, consciousness in particular, are reducible to computational processes in the brain: computationalism. Whether this is … Continue reading

## Inventing a knot theory for eight year olds (II)

So I am running a math club for 8 year olds and we are reinventing (an) algebraic knot theory. We are not trying to reinvent existing knot theory, just to make a journey of intellectual and mathematical discovery. In the … Continue reading

Posted in teaching | 1 Comment

## Inventing a knot theory for eight year olds (I)

Last year I experimented with teaching seven and eight year olds about monoidal categories using a very concrete model of cardboard rectangles and bits of string. The experiment was a success, with children becoming able to represent formally a model … Continue reading

Posted in teaching | 2 Comments

## Two kinds of mathematics

Preliminary reading: “The Origins and Motivations of Univalent Foundations” by V. Voevodsky’s [PDF] “Proofs and refutations” by I. Lakatos [link] “On proofs and progress in mathematics” by W. Thurston [link] I find the recent surge in interest in the use of … Continue reading

Posted in armchair philosophy, proof assistants | 1 Comment

## Two views of programming language design

In computer science, the Boolean or logical data type is a data type, having two values (usually denoted true and false), intended to represent the truth values of logic and Boolean algebra. [Wikipedia] In computer science, a tagged union, also called a variant, variant record, discriminated union, disjoint union, or sum type, is a data structure used to hold a value that could … Continue reading

Posted in programming languages | 3 Comments