(a.) The simply typed lambda calculus (STLC) corresponds via the celebrated Curry-Howard isomorphism (see Wikipedia) to intuitionistic propositional logic (again, for now, see Wikipedia).
(b.) Adding dependent types to the STLC corresponds to adding predicates to the language, i.e. to intuitionistic predicate logic.
(c.) Adding abortive continuations (call/cc) to the STLC corresponds to classical propositional logic.
(d.) (b) and (c) above have never been included in a single type system. Wouldn't it be great to have a nice type system for a lambda calculus that corresponds to CLASSICAL PREDICATE logic? It is also very nice for programming. That is the meaning of this project. More info will be up later.

Glossary:

Being your computer's slave master and telling it what to do, step after step.
problems:

The computer hasn't a clue what it's being asked to do, so:
1. the programmer must write lots of things explicitly.
2. it can't check that the programmer is actually doing what he wanted to do.

benefits:

1. Readability: Commands are executed roughly in the order that they were given, unless the computer is told to do otherwise.
2. Current imperative programming languages are the only ones that are suitable for serious large-scale development.

languages:

Machine language, Assembly language, BASIC, Pascal, Cobol, Fortran, ...

Making the computer do things by defining functions, applying functions, and making inquiries about expressions made of functions.
Note:

Functions here actually refer to things that take arguments and give results based only upon these arguments, and not anything else, like what the user types on the keyboard, the time of day, the contents of a file on the hard drive, or global variables containing information about the programmer's friends' phone numbers. (In fact, global variables do not exist in stripped-down functional programming languages, though they can be added in more complicated versions. There are tricks (see "monads" in Haskell) for making these functions blend in well with the basic functional paradigm.)

problems:

1. Not yet feasible for huge projects -- I suspect more things will have to be abstracted out before functional programming becomes feasible for large collaborative projects. 2. As far as I know: Very little good literature exists that teaches this style of programming. Also, very few programmers today know functional programming!

benefits:

1. Expressions, evaluation, and type systems are mathematically easy to define.
2. Mathematically beautiful.
3. Programs to concepts in mathematical logic (Curry-Howard isomorphism -- types are propositions and expressions are proofs).
4. Supports Program verification -- It is possible to prove, with certainty, that a program does what it is supposed to do, and that it always will (assuming no hardware or operating system or compiler issues)! This is the ultimate way to test a program!

languages:

Scheme, Haskell, Ocaml, lambda calculus, ...

Telling the computer what you want and helping it out by giving hints when it gets stuck or feel like it's taking too long.
problems:

The computer gets stuck or takes too long in lots of cases.

benefits:

1. You can take rests and rely on the computer to write some hard pieces of code for you (even ones that you have no idea how to).
2. Useful for assistance in proving mathematical theorems.

languages:

Prolog, Coq, HOL Light, ...

One of the simplest functional programming languages ever.

Basically, all you can do are make functions (called "abstracting") and apply functions.
Expressions consist of variables, abstractions and applications.
For example:
1.     "(replace x in z) y", conventionally written "(lambda x . z) y", evaluates to z, because when you replace x by y in the expression z, you get, well, z.
2.     "(replace x in x) y", conventionally written "(lambda x . x) y", evaluates to y, because when you replace x by y in the expression x, it turns into y.
3.     If we allow numbers and arithmetic, then "(replace x in x+3) 5", conventionally written "(lambda x . x+3) 5", evaluates to 8, because when you replace x by 5 in the expression x+3, we get 5+3, which is 8.
4.     Again, if we allow numbers and arithmetic, then "(replace x in x+3) ((replace y in y*7) 2)" evaluates to

An assignment of "[data]types" to expressions. The type of an expression should always be possible to determine in finite time (i.e. without running on forever), and it is useful to have the type of an expression tell you how that expression can be used: For example, "lambda x . x+3" is a function that takes numbers and gives you numbers, so its type is "numbers to numbers". If you try to feed it strings, it will vomit, i.e. say something like "This does not make any sense; I will now fail." Wouldn't it be nice to avoid that? Just check the type! If the first part of the type of a function says that it takes numbers, then you should only feed it things that have the type "number" (like, say, "3" or "5+7*91"). Wouldn't it be nice if pets were labeled like that?

A type system in which functions are permitted to take expressions as arguments and produce types as results! For example, "if you give me 1, then I will give you the type 'number', but if you give me any other number, then I will give you the type 'string'" is an expression with type "number -> TYPE". But we can get more complicated, because we can make other functions, whose output types depend on what you feed the first one. This is an explicit way to treat "polymorphism," which is handled more implicitly and less controllably in languages like Java or C++.

A way of asking about your fate, and then taking it into your hands. (A more complete explanation is forthcoming.)