Proving the Church-Rosser Theorem Using a Locally Nameless Representation
November 21, 2011
Around 2 years ago, for an earlier project of mine (which has not seen its light yet!) in which I had to build a language with variables and prove its properties, I surveyed a number of ways to handle binders. For some background, people have noticed that, when proving properties about a language with bound... [1 comment...].
Around 2 years ago, for an earlier project of mine (which has not seen its light yet!) in which I had to build a language with variables and prove its properties, I surveyed a number of ways to handle binders. For some background, people have noticed that, when proving properties about a language with bound... [1 comment...].
Calculating Programs from Galois Connections
December 10, 2010
One is often amazed that, once two functions are identified as a Galois connection, a long list of nice and often useful properties follow from one concise, elegant defining equation. But how does one construct a program from a specification given as a Galois connection? ... [14 comments...].
One is often amazed that, once two functions are identified as a Galois connection, a long list of nice and often useful properties follow from one concise, elegant defining equation. But how does one construct a program from a specification given as a Galois connection? ... [14 comments...].
Evaluating Simple Polynomials
July 12, 2010
I had a chance to show the students, in 25 minutes, what functional program calculation is about. The student have just been exposed to functional programming a week ago in a three-hour course, and I have talked to them about maximum segment sum way too many times. ... [11 comments...].
I had a chance to show the students, in 25 minutes, what functional program calculation is about. The student have just been exposed to functional programming a week ago in a three-hour course, and I have talked to them about maximum segment sum way too many times. ... [11 comments...].
Sum of Squares of Differences
July 11, 2010
Given an array of integers having at least two elements, compute the sum of squares of the difference between all pairs of elements. It is not hard to quickly write up a O(N²) program using nested loops, which, I have to confess, is what I would do before reading Kaldewaij’s book and realised that it... [2 comments...].
Given an array of integers having at least two elements, compute the sum of squares of the difference between all pairs of elements. It is not hard to quickly write up a O(N²) program using nested loops, which, I have to confess, is what I would do before reading Kaldewaij’s book and realised that it... [2 comments...].
An Exercise Utilising Galois Connections
May 6, 2010
In the recent work of Sharon and me on maximally dense segments we needed quite a number of functions to be monotonic, idempotent, etc. It only occurred to me after submitting the paper: could they be defined as Galois connections? ... [no comments...].
In the recent work of Sharon and me on maximally dense segments we needed quite a number of functions to be monotonic, idempotent, etc. It only occurred to me after submitting the paper: could they be defined as Galois connections? ... [no comments...].
