Welcome!

[Joseph Razavi]

Hi,

Everybody's on the list now, so it's time I sent out the information I
promised. Before I do, I should reiterate that our default meeting
time is Monday 5-6pm in Kilburn G23 (the mailing list had some old
information from last year, when we met on a Tuesday in a different
room, hidden deep in the settings!).

The mailing list will accept email from all of us. I think it's good
to email it whenever you have something to ask or tell everyone -- but
please speak up if you think you're getting too much email! To email
the list, send your email to
manchester-type-th...@googlegroups.com .

In the rest of this message, I'll suggest some exercises which I think
would be good to look at on Monday (so you can look at them in advance
if you want to). Then I'll describe how to log into Jonas' computer to
use coqide yourself.

See you soon,

Joe



SUGGESTED EXERCISES

I think the most practical thing to do is suggest exercises which we
will look at together in the session. That way nobody gets left behind
once the workload starts to build up later in the semester. Of course,
these are only suggestions -- I think the course (
http://www.cis.upenn.edu/~bcpierce/sf/ ) would be a bit big to just
link people to and say "have a go at that!".

The first interesting stuff is
http://www.cis.upenn.edu/~bcpierce/sf/Basics.html . This web page is
the same as the file Basics.v, just formatted a little bit more
nicely. I think it would be good to look at the basic ways of
describing types; these are given in the sections Booleans, Function
Types, and Numbers. The section "Days of the Week" gives a homely
example.

Exercises "nandb" and "factorial" would be good to focus on. (Exercise
names are in brackets after their "star rating".)

There is a lot of stuff in the descriptive parts which is aimed at one
specialist audience or another and which isn't very important, so if
you don't know what a paragraph is talking about, try skipping it. If
you can do those exercises, you've read enough of the text.

Computer scientists will know what "Booleans" are; mathematicians may
not. A "boolean domain" ( http://en.wikipedia.org/wiki/Boolean_domain
) is just a two element set. They are interesting because subsets of a
set can be seen as functions from that set into a two element set
(i.e. the function separates elements into two classes, those in the
subset and those not in the subset). They can clearly be equipped with
operations which interpret the two elements as the truth vales from
Propositional Logic.

Let me stress again that you don't need to do any reading or work
outside the sessions -- the information is here in case you'd like to
do so, and to give an impression of what might be done in the session.
See you there!

USING COQ YOURSELF

The easiest way to use Coq is probably to log in to Jonas' computer
and use his installation. Most computers in the School of Maths can be
booted in Linux (i.e. when they are first switched on, they offer the
choice to use Linux instead of Windows), so I'll give Linux and Mac
instructions first:

1) Log in to your own account (in the School of Maths, you might need
to contact someone to find out what your Linux username and password
are)
2) Open a terminal (in the Scool of Maths, click on Applications ->
System Tools -> Terminal)
3) Recall your number n (from 0 to 8)
4) Type

ssh -X gue...@rpc324.cs.man.ac.uk coqide

(So if you are number 6, you would type

ssh -X gue...@rpc324.cs.man.ac.uk coqide

)

5) You might see a warning about authentication; type "yes" and hit enter.
6) you will be asked for a password -- everybody's is

coqreading

7) You should see CoqIDE open.
8) To see the file we were working on, click File -> Open -> sf -> Basics.v

In Windows, you need an ssh client. A popular one is PuTTY, which you
can download from here
http://www.chiark.greenend.org.uk/~sgtatham/putty/download.html .
(Click on the link "putty.exe"). Then:

1) Click on "putty.exe" wherever it downloaded to (and click through
and Windows warnings).
2) Find a textbox in the interface called "Host Name"
3) Enter:

rpc324.cs.man.ac.uk

4) In the "Connection type:" area, make sure "SSH" is selected
5) Click "Open"
6) Click through any authentication warnings
7) It should ask for a login, recall your number n (from 0 to 8) and type

guest0n

(So number 6 types

guest06
)

8) It will ask for a password, type

coqreading

9) Type

coqide

10) You should see CoqIDE open.
11) To see the file we were working on, click File -> Open -> sf -> Basics.v

If you want to try installing Coq on your own machine, you can get it
from here: http://coq.inria.fr/download (But I've never tried doing
this!)

Let us know if you have any problems doing any of this!

[Amara Emerson]

As a former student at the CS department I still keep an eye on this
group. I'd like to ask people that if they find interesting
books/articles or other resources that they send a link it to this
mailing list as well for those of us who can't go to the meetings.

Much appreciated,
Amara

> --
> 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.
>
>

[wan...@cs.man.ac.uk]

hello Amara and all others.

I just found a book titled "Type theory and functional programming" by
Simon Thompson (you can find this book in the lib: 005.114.T1). I am
reading it and found it very well structured for beginners.

and thanks for you "eyes" on this group :) hope you are doing well.

Cheers
Robert

[Giles Reger]

Hi,

I know Simon Thompson - I'm thinking of asking him to be my external
PhD examiner. It's also a good book - let us know how you get on! I
think it's also available online.

Giles