--- Day changed Sat Apr 04 2015
jonsterlingxplat: By the way, here is a quick example of a intensional type theory that is open-ended, modular, and has computational content in the same sense as ETT, if I am not mistaken: https://github.com/jonsterling/twelf-itt/blob/master/computational/thy.elf04/04 19:23
jonsterlingThere are a few other techniques that could be used, but this one seemed to work nicely for me. It's very fine-grained, but the judgements are factored to make the definition of a type as similar as possible to how one would do it in ETT.04/04 19:23
jonsterlingI don't have time to discuss it right now (forgot my laptop charging cable in another city), but I'll just put it here as food for thought and if there is interest, we could discuss it another time.04/04 19:23

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!