DIKU ITU KVL

Copenhagen Programming Language Seminar

COPLAS Talk

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

Abstract:

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