Happy September!

[Joseph Razavi]

Hello!

September is back, and perhaps, like autumn leaves and marrows, some
of you are back too. Naturally, you will want to come to type theory
as soon as possible -- but I should warn you that over the summer
meetings have become very ad hoc (and they have closed our room for
renovation!). If anybody gets back and wants to meet anybody else,
it's probably best to arrange a meeting via the list.

Once term has got going, we'll formalize our meetings (and meet our
formalizations!) once again.

Joe


P.S.
Some types-related stuff I've been reading recently:

"A Gentle [ha!] Introduction to Type-Logical Grammars" [parenthetical
remark mine] --
semanticsarchive.net/Archive/DMzOTFiN/barker.gentle.tlg.pdf
This is about studying natural languages via type theory. You have a
strange logic of grammatical sentences, and proofs in this logic can
be read either as parsings of a sentence (labelling each bit with a
grammatical category) or as computations which output the meaning of
the sentence automatically!

"The Elements of an Inductive Type" --
http://math.andrej.com/2013/08/28/the-elements-of-an-inductive-type/
A cool blog post by Andrej Bauer where he describes some models of
type theory where there are more things in the model of the "natural
number" type (..., Horatio,...) than just zero and its successors!

Both of these require background which I don't expect many of us
(including me) will have -- but it might be worth having a glance to
see if the conceptual ideas interest you enough to want to go into the
details.

[Colin Caine]

On Sun, Sep 01, 2013 at 01:52:37AM +0100, Joseph Razavi wrote:
> September is back, and perhaps, like autumn leaves and marrows, some
> of you are back too. Naturally, you will want to come to type theory
> as soon as possible -- but I should warn you that over the summer
> meetings have become very ad hoc (and they have closed our room for
> renovation!). If anybody gets back and wants to meet anybody else,
> it's probably best to arrange a meeting via the list.

Hey Joe,

I'm back in Manchester for the CDT programme. I would be interested in
some type theory meets but I haven't seen you around. Are meets becoming
less ad-hoc with the new semester?

Colin

[Joseph Razavi]

Hi Colin,

I'm mostly out of town until October, hence my addressing the
intentions-to-meet of a rather abstract "anybody". If you want to see
me in particular, I might have a little time on Thursday.

After I get back I'll restart regular meetings (if they haven't
already started in my absence :) ). I suspect we'll have to deal with
a few hiccups to do with the new IT stuff in the CS department -- my
hope is to be ready to take on new people after reading week, though
like everything that's definitely up for debate!

I'd like to conclude as usual with some suggested technical reading --
but I'm on holiday at the moment, and reading Middlemarch!

So there;

Joe

> --
> You received this message because you are subscribed to the Google Groups "Manchester Type Theory Reading Group" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to manchester-type-theory-r...@googlegroups.com.
> For more options, visit https://groups.google.com/groups/opt_out.