Yu-Hsi Chiang, Shin-Cheng Mu. Journal of Logical and Algebraic Methods in Programming, 85(5), Part 2, pp 879-905, August 2016.
[Paper(doi:10.1016/j.jlamp.2015.12.003) | Code]
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 …
Proving the Church-Rosser Theorem Using a Locally Nameless Representation Read More »
“I cannot prove that if a function is injective, it has an inverse,” Hideki Hashimoto posed this question to me. Is it possible at all?
I was puzzled by the fact stated in a number of places that axiom of choice, proof irrelevance, and extensional equality together entail the law of excluded middle.
S-C. Mu, H-S. Ko, and P. Jansson. Algebra of programming in Agda: dependent types for relational program derivation. In Journal of Functional Programming, Vol. 19(5), pp. 545-579. Sep. 2009. [PDF]
Anton Setzer argued in his letter to the Agda mailing list that we should go back to a category theoretical view of codata, and Dan Doel soon successfully experimented the ideas.
It would be nice to if we could write the program and prove its termination separately. Adam Megacz published an interesting paper: A Coinductive Monad for Prop-Bounded Recursion. As a practice, I tried to port his code to 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.
S-C. Mu, H-S. Ko, and P. Jansson. Algebra of programming using dependent types. In Mathematics of Program Construction 2008, LNCS 5133, pp 268-283. July 2008.
Superseded by the extended version for Journal of Functional Programming.
[PDF]
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.