Type theory beginners' study group

[Yusha3 L]

Hello all, I'm working on organizing a study group on type theory that would gradually work its way up to HoTT. The plan is to begin with Aarne Ranta's book Type-theoretical Grammar,

 possibly using Nederpelt & Geuvers, Type Theory and Formal Proof for more details, then David Corfield's Modal Homotopy Type Theory and/or the HoTT book itself.

We're still in the early stage of organizing the group so we haven't set a schedule yet. We're coming to the subject with a background in linguistics and philosophy, so it would be great to get people from math and comp sci to help us out.

If you're interested in participating, reply to this thread.

Thanks!

[fernan...@gmail.com]

Hello all. I am interested! I have a decent math and comp sci background I believe and would love to be part of this group.

[Hendrik Boom]

On Sun, Jun 13, 2021 at 11:04:30AM -0700, Yusha3 L wrote:

Looks interesting. I got into type theory in the 1980's, and spent some
time trying to implement it as a kind of formally verified programming
language.

I didn't get very far at the time because of machine limitations.

My inspiration came from automath (which gave me the idea of
propositions as types) and from Martin-Lof's papers. I'm not sure where
my copies of these documents are now.

I'm not at all sure I want to expend serious money buying books that
likely tell me what I'm already familiar wit,

> Hello all, I'm working on organizing a study group on type theory that
> would gradually work its way up to HoTT. The plan is to begin with Aarne

> Ranta's book *Type-theoretical Grammar*
> <https://books.google.ca/books?hl=sv&lr=&id=A5m13eGOcqYC&oi=fnd&pg=PA1&dq=aarne+ranta&ots=KjH2Put2Wa&sig=J__Gk-RZctvQzSqJBDVXyngpY1Y&redir_esc=y#v>
> ,

> possibly using Nederpelt & Geuvers, Type Theory and Formal Proof

> <https://www.cambridge.org/core/books/type-theory-and-formal-proof/0472640AAD34E045C7F140B46A57A67C> for

This one seems to expound in detail what I already know.

> more details, then David Corfield's *Modal Homotopy Type Theory
> <https://oxford.universitypressscholarship.com/view/10.1093/oso/9780198853404.001.0001/oso-9780198853404>

This one looks interesting, but the web page doesn't make it clear how
to go about getting a copy. It certainly doesn't give me a clue how
much it would cost. I do not have proper access to a research library.

> *and/or the HoTT book itself.

This one I have, and enjoy. I think I'd understand more of it if I knew
more about homotopy theory itself.

> We're still in the early stage of organizing the group so we haven't set a
> schedule yet. We're coming to the subject with a background in linguistics
> and philosophy, so it would be great to get people from math and comp sci
> to help us out.

I'm a mathematician who has spent most his his life doing things with
computers.

> If you're interested in participating, reply to this thread.
> Thanks!
>

-- hendrik

> --
> You received this message because you are subscribed to the Google Groups "HoTT Cafe" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to hott-cafe+...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/hott-cafe/4ea638a5-75af-4f73-a4b7-a4e43b1dc596n%40googlegroups.com.