Copenhagen Programming Language Seminar


A Natural Framework for Writing and Checking Proofs

Masahiko Sato,
Kyoto University, Japan

Monday (!), August 29, 15:15-16:00
DIKU, Universitetsparken 1, room N010


From the beginning of the twentieth century, mathematicians thought about formalizing their activity. First, they formalized some logics, mainly arithmetics. Later, they wanted to define clearly what is a proof. Then came the formalization of meta-properties of a logical system: consistency, completeness. Computer science entered that field with the development of logical frameworks. A logical framework is a formal system in which one can define logics, write and check some proofs in these logics. Hopefully, logical frameworks will also soon be able to handle meta-properties. Natural Framework (NF for short) is a logical framework. It is intended to be as simple as possible, understandable without the heavy classical logic background, e.g. dependent types which are needed for the judgments-as-types approach used in LF.

Scientific host: Robert Glück. Administrative host: Camilla Jensen. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and KVL. COPLAS is sponsored by FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org