Talk:Intuitionistic type theory

From Wikipedia, the free encyclopedia

You have new messages (last change).

I have extensively expanded and rewritten this page. I am happy for anybody who helps me by elimenating typos and bad expression and by inserting more references. In the past somebody rewrote parts of what I had written, changing the emphasis considerably, e.g. talking about "an" Intuitionistic Type Theory while people in the wider area usually refer to Intuitionistic Type Theory using capital letters in the same way they refer to Set Theory and not a set theory. Hence, I have changed this back. If anybody is unhappy about this, please let's discuss it here.

Thorsten 21:57, 21 May 2005 (UTC)txa

I took out the reference to Automath, while it is true that there are interactions between Type Theory and Automath it is not true that Automath is based on Type Theory. I am happy to put it back in as soon as either me or sb else comes up with a good way of saying this.

I am not so sure whether the Thompson reference is such a good idea. I know and respect Simon, but I can't say I like this book... --Thorsten 18:39, 22 May 2005 (UTC)

  • I did start a dependent types article, but my point re the Thompson book wasn't so much where it should be cited but rather whether it should be cited.--Thorsten 15:37, 28 May 2005 (UTC)

[edit] Article name

It's right to notice all the synonyms that have been used for this theory, but my impression is that few scholars will use Intuitionistic Type Theory to refer to the calculus, but instead talk of Martin Loef's type theory, because there are many proposed intuitionistic type theories. I'd suggest moving the page, and say that the calculus has been called these other names. --- Charles Stewart 19:03, 23 May 2005 (UTC)

I agree Martin-Loef's Type Theory is more used more often than Intuitionistic Type Theory but the latter is more descriptive and in particular doesn't depend on Per Martin-Loef being happy with it. As I tried to express in the article there are a number of variants of Type Theory, e.g. extensional vs intensional, predicative vs.impredicative. However, we also talk about Set Theory and not set theories even though also there is some variation, we may add the axiom of choice or not, we may have the continuum hypothesis and we may or not add some large cardinals but we still call it Set Theory. I think it woukd be misleading to talk about intuitionistic type theories and I haven't seen anybody using this term. --Thorsten 15:34, 28 May 2005 (UTC)

JA: I did not do an exhaustive search, but as far as I can tell, searches for a generic article on "theory of types" get directed here, in addition to which we have computation-related articles on Type systems and Type theory. If there is some sort of proprietary claim on a capitalist rendition of T2, then let the interested parties go take it up with Arnold Schwarzenegger. In the meantime, we need generic lower shelf articles on type theory and intuitionistic type theory that are comparable to those on graph theory, group theory, etc. Jon Awbrey 14:53, 1 May 2006 (UTC)

There is no claim whatsoever, the capitilasation expresses that one means the Type Theory instead of any.

--Thorsten 20:58, 7 June 2006 (UTC)

[edit] Type Theory is the name of a Programming Language

Spelled with initial capitals, Type Theory refers to a functional programming language based on the same principles.

Who has added this nonsense???? I have removed it. If you want it back, please xplain.

--Thorsten 20:55, 7 June 2006 (UTC)

Retrieved from "http://en.wikipedia.org../../../i/n/t/Talk%7EIntuitionistic_type_theory_f0c0.html"