Musing about programming languages and computer science.
During two weeks of September 2024 I experimented with using the Deduce proof assistant in an honors undergraduate data structures course at Indiana University. The rest of the semester is taught using the Java programming language. The primary goal of the experiment was to find out whether it would be feasible to teach our undergraduate students how to use a proof assistant and prove correctness…
This is the seventh blog post in a series about developing correct implementations of basic data structures and algorithms using the Deduce language and proof checker. This post continues on the theme of binary trees, that is, trees in which each node has at most two children. The focus of this post is to implement the Search interface, described next, using binary trees. The Search Interface The…
This is the sixth blog post in a series about developing correct implementations of basic data structures and algorithms using the Deduce language and proof checker. This post continues were we left off from the previous post in which we implemented binary trees and in-order tree iterators. Our goal in this post is to prove that we correctly implemented the iterator operations: ti2tree : < E > fn…
This is the fifth blog post in a series about developing correct implementations of basic data structures and algorithms using the Deduce language and proof checker. In this blog post we study binary trees, that is, trees in which each node has at most two children. We study the in-order tree traversal, as that will become important when we study binary search trees. Furthermore, we implement tree…
Merge Sort with Leftovers This is the fourth blog post in a series about developing correct implementations of basic data structures and algorithms using the Deduce language and proof checker. In this blog post we study a fast sorting algorithm, Merge Sort. This classic algorithm splits the input list in half, recursively sorts each half, and then merges the two results back into a single sorted…
Insertion Sort This is the third blog post in a series about developing correct implementations of basic data structures and algorithms using the Deduce language and proof checker. In this blog post we study a simple but slow sorting algorithm, Insertion Sort. (We will study the faster Merge Sort in the next blog post.) Insertion Sort is, roughly speaking, how many people sort the cards in their…
Sequential Search This is the second blog post in a series about developing correct implementations of basic data structures and algorithms using the Deduce language and proof checker. In this blog post we’ll study a classic and simple algorithm known as Sequential Search (aka. Linear Search). The basic idea of the algorithm is to look for the location of a particular item within a linked list,…
Prelude This is the first in what I hope to be a sequence of blog posts about (1) data structures and algorithms, (2) an approach to constructing correct code, and (3) achieving a deeper understanding of testing, logic, and proof, all of which are needed for constructing correct code. These blog posts take a functional programming approach to data structures and algorithms because, in that…
Recall that closure conversion lowers lexically-scoped functions into a flat-closure representation, which pairs a function pointer with a tuple of values for the function’s free variables. The crux of this pass is a transformation we call “delay” (D) because it postpones the point at which the function is applied to the above-mentioned tuple, from the point of definition of the function to the…
{-# OPTIONS --rewriting #-} module LogRel.BlogGradualGuaranteeLogRel where open import Data.Empty using ( ⊥ ; ⊥-elim ) open import Data.List using ( List ; [] ; _∷_ ; map ; length ) open import Data.Nat open import Data.Nat.Properties open import Data.Product using ( _,_ ; _×_ ; proj₁ ; proj₂ ; Σ-syntax ; ∃-syntax ) open import Data.Sum using ( _⊎_ ; inj₁ ; inj₂ ) open import Data.Unit using ( ⊤ ;…
``` {-# OPTIONS --rewriting #-} module rewriting.examples.BlogTypeSafety10Easy4Med1Hard where open import Data.Bool using ( true ; false ) renaming ( Bool to 𝔹 ) open import Data.Empty using ( ⊥ ; ⊥-elim ) open import Data.Nat open import Data.Nat.Properties using ( ≤-refl ) open import Data.List using ( List ; [] ; _∷_ ) open import Data.Product using ( _,_ ; _×_ ; proj₁ ; proj₂ ; Σ-syntax ;…
FastExp ``` module FastExp where ``` # Imports ``` open import Data.Nat open import Data.Nat.Properties open import Data.Nat.Induction hiding ( rec ) open import Data.Product using ( _×_ ; _,_ ; Σ ; Σ-syntax ; ∃ ; ∃-syntax ; proj₁ ; proj₂ ) open import Data.Sum using ( _⊎_ ; inj₁ ; inj₂ ) open import Induction open import Relation.Binary.PropositionalEquality open import Exponents open import…
Some presentations of Kosaraju’s Algorithm don’t provide a detailed explanation of why the algorithm works. Here’s my attempt to explain it. The story begins with depth-first search (DFS). To review, DFS goes deeper at each step, following an out-edge from the current vertex to a never-before-seen vertex. If there are no out-edges to never-before-seen vertices, then the search backtracks to the…
Type Safety in Two Easy Lemmas Type Safety in Two Easy Lemmas Wow, it's been seven years already since I blogged about Type Safety in Three Easy Lemmas . Time flies! In that blog post I showed how to prove type safety of a simple language whose semantics was specified by a definitional interpreter. I still like that approach, and it has proved useful to other researchers on much larger projects…
Which papers would I recommend for getting started on understanding the research on gradual typing? That's a hard question because there are a lot of papers to choose from and, as research papers, their primary goal was not to give a good introduction, but instead to describe some scientific contribution. I really ought to write a proper introduction, but in the mean time, here's my choice of a…
Intersection Types, Sub-formula Property, and the Functional Character of the Lambda Calculus Last December I proved that my graph model of the lambda calculus, once suitable restricted, is deterministic. That is, I defined a notion of consistency between values, written \(v_1 \sim v_2\) , and showed that any two outputs of the same program are consistent. Theorem (Determinism) If \(v \in…
Continuous functions over the real numbers As a high school student and undergraduate I learned in Calculus that real numbers involve infinity in precision, e.g. some have no finite decimal representation, and a continuous function forms an unbroken line, a necessary condition to be differentiable. For an example, the decimal representation of \(\sqrt 2\) goes on forever: \[1.41421 \ldots\] Later…
Happy holidays! There’s nothing quite like curling up in a comfy chair on a rainy day and proving a theorem in your favorite proof assistant. Lately I’ve been interested in graph models of the \(\lambda\) -calculus, that is, models that represent a \(\lambda\) with relations from inputs to outputs. The use of relations instead of functions is not a problem when reasoning about expressions that…
My submission about declarative semantics to POPL was rejected. It's been a few weeks now, so I'm not so angry about it anymore. I've revised the paper and will be submitting it to ESOP this week. The main reason for rejection according to the reviewers was a lack of technical novelty, but I think the real reasons were that 1) the paper came across as too grandiose and as a result, it accidentally…
On the plane ride back from ICFP last month I had a chance to re-read and better understand Plotkin’s Set-theoretical and other elementary models of the \(\lambda\) -calculus (Technical Report 1972, Theoretical Computer Science 1993) and to read, for the first time, Engeler’s Algebras and combinators (Algebra Universalis 1981). As I wrote in my draft paper Declarative semantics for functional…
Last week I submitted a paper to POPL 2018 about the new kind of denotational semantics that I've been writing about in this blog, which I am now calling declarative semantics . I think this approach to semantics has the potential to replace operational semantics for the purposes of language specification. The declarative semantics has the advantage of being compositional and extensional while,…
Robin Milner proved that well-typed programs cannot go wrong in his 1978 paper A Theory of Type Polymorphism in Programming (Milner 1978) . That is, he defined a type system and denotational semantics for the Exp language (a subset of ML) and then proved that the denotation of a well-typed program in Exp is not the “wrong” value. The “wrong” denotation signifies that a runtime type error occurred,…
This is a two part post. The second part depends on the first. Part 1. Consolidation of the Denotational Semantics As a matter of expediency, I've been working with two different versions of the intersection type system upon which the denotational semantics is based, one version with subsumption and one without . I had used the one with subsumption to prove completeness with respect to the…
In my post about intersection types as denotations , I conjectured that the simple "take 3" denotational semantics is equivalent to an intersection type system. I haven't settled that question per se, but I've done something just as good, which is to show that everything that I've done with the intersection type system can also be done with the "take 3" semantics (with a minor modification).…
The ICFP paper submission deadline kept me busy for much of February, but now I'm back to thinking about the simple denotational semantics of the lambda calculus. In previous posts I showed that this semantics is equivalent to standard operational semantics when considering the behavior of whole programs. However, sometimes it is necessary to reason about the behavior of program fragments and we…