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.
How can I introduce accumulating parameters to derive the linear-time, tail recursive implementation of
Prove the following property in point-free style:
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.
Given a relation
I hope to come up with a variation of unfoldr which, given a proof of well-foundedness, somehow passes the termination check.
Back in 2003, my colleagues there were discussing about the third homomorphism theorem — if a function
Given an interpreter of a small language, derive a virtual machine and a corresponding compiler