|
|||||
|
I spent a week trying to implement higher-order pattern unification. I looked at couple of PhD dissertations, talked to lots of smart people, and failed because the substitutions were just getting in the way all the time. So today we are going to bite the bullet and implement de Bruijn indices and explicit substitutions. The code is available on Github in the repository andrejbauer/tt (the I am on a roll. In the second post on how to implement dependent type theory we are going to:
I am spending a semester at the Institute for Advanced Study where we have a special year on Univalent foundations. We are doing all sorts of things, among others experimenting with type theories. We have got some real experts here who know type theory and Coq inside out, and much more, and they’re doing crazy things to Coq (I will report on them when they are done). In the meanwhile I have been thinking how one might implement dependent type theories with undecidable type checking. This is a tricky subject and I am certainly not the first one to think about it. Anyhow, if I want to experiment with type theories, I need a small prototype first. Today I will present a very minimal one, and build on it in future posts. Make a guess, how many lines of code does it take to implement a dependent type theory with universes, dependent products, a parser, lexer, pretty-printer, and a toplevel which uses line-editing when available? Matija and I are pleased to announce a new major release of the eff programming language. In the last year or so eff has matured considerably: It now looks and feels like OCaml, so you won’t have to learn yet another syntax. With Matija Pretnar. Abstract: Eff is a programming language based on the algebraic approach to computational effects, in which effects are viewed as algebraic operations and effect handlers as homomorphisms from free algebras. Eff supports first-class effects and handlers through which we may easily define new computational effects, seamlessly combine existing ones, and handle them in novel [...] While making a comment on Stackoverflow I noticed something: suppose we have a term in the $\lambda$-calculus in which no abstracted variable is used more than once. For example, $\lambda a b c . (a b) (\lambda d. d c)$ is such a term, but $\lambda f . f (\lambda x . x x)$ is not because [...] As a preparation for my part of a joint tutorial Programs from proofs at MFPS 27 at the end of this month with Ulrich Berger, Monika Seisenberger, and Paulo Oliva, I’ve developed in Agda some things we’ve been doing together. Using Berardi-Bezem-Coquand functional, or alternatively, for giving a [...] Bob Harper of CMU, has recently started a blog, called Existential Type, about programming languages. He is a leading expert in Programming Languages. I remember being deeply inspired the first time I heard him talk. I was an incoming graduate student at CMU and he presented what the programming languages people at CMU did. His posts [...] [UPDATE 2012-03-08: since this post was written eff has changed considerably. For updated information, please visit the eff page.] Let’s keep the blog rolling! Here are delimited continuations in eff, and a bunch of questions I do not know the answers to. [UPDATE 2012-03-08: since this post was written eff has changed considerably. For updated information, please visit the eff page.] From some of the responses we have been getting it looks like people think that the |
|||||
|
|
|||||
