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.
Research Blog
Tail-Recursive, Linear-Time Fibonacci
How can I introduce accumulating parameters to derive the linear-time, tail recursive implementation of
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
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
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