# Research Blog

## Typed λ Calculus Interpreter in Agda

In a recent meeting I talked to my assistants about using dependent type to guarantee that, in an evaluator for λ calculus using de Bruin indices, that variable look-up always succeeds.

## Tail-Recursive, Linear-Time Fibonacci

How can I introduce accumulating parameters to derive the linear-time, tail recursive implementation of fib.

## A Simple Exercise using the Modular Law

Prove the following property in point-free style:

## Well-Foundedness and Reductivity

It seems that reductivity of Doornbos and Backhouse is in fact accessibility, which is often taken by type theorists to be an alternative definition of well-foundedness.

## Well-Founded Recursion and Accessibility

Given a relation < that has been shown to be well-founded, we know that a recursively defined function is terminating if its arguments becomes “smaller” with respect to < at each recursive call. We can encode such well-founded recursion in Agda’s style of structural recusion.

## Terminating Unfolds (2)

After seeing our code, Nils Anders Danielsson suggested two improvements. Firstly, to wrap the bound in the seed. Secondly, to define `unfoldT↓` using well-founded recursion.

## Terminating Unfolds (1)

I hope to come up with a variation of unfoldr which, given a proof of well-foundedness, somehow passes the termination check.

## Constructing List Homomorphism from Left and Right Folds

Back in 2003, my colleagues there were discussing about the third homomorphism theorem — if a function f can be expressed both as a foldr and a foldl, there exists some associative binary operator such that f can be computed from the middle. The aim was to automatically construct .

## S Combinator is Injective, with Proofs

By chance, I came upon a blog entry by Masahiro Sakai (酒井政裕) in which he, after reading my short comment “Do you know that the `S` combinator is injective?”, tried to construct the inverse of `S` and showed that `S⁻¹ ○ S = id` in, guess what, Agda!

## Deriving a Virtual Machine

Given an interpreter of a small language, derive a virtual machine and a corresponding compiler