## Computer Science/Mathematical Notations

I was just reading this paper from the home page

http://pauillac.inria.fr/~fpottier/slides/fpottier-2007-05-linear-bestiary.pdf

and realized I can't remember the meaning of many of the symbols after not using them for some time. Is there a reference somewhere that explains these symbols. I'm finding it hard to locate one.

Thank you.

## Comment viewing options

### wikipedia

In picking up this notation for the first time I found wikipedia's Calculus of Constructions very helpful. And if you really want to get back to basics then you can start with Lambda Calculus.

### Somewhat underwhelmed...

I'm somewhat underwhelmed by the section on Terms...

Terms

A term in the calculus of constructions is constructed using the following rules:

* T is a term (also called Type)
* P is a term (also called Prop, the type of all propositions)
* If A and B are terms, then so are
o \mathbf{(} A B )
o (\mathbf{\lambda}x:A . B)
o (\forall x:A . B)

The calculus of constructions has four object types:

1. proofs, which are terms whose types are propositions
2. propositions, which are also known as small types
3. predicates, which are functions that return propositions
4. large types, which are the types of predicates. (P is an example of a large type)
5. T itself, which is the type of large types.


It's a bit like a bullet list of non-sequiturs. Anything with a bit more meat on the bones? Or even better, can anyone edit the Wikipedia entry and add that meat?

### thanks!

Thanks Andrew, CoC is exactly what I'm looking for.