Copenhagen Programming Language Seminar
Mizar is a proof checker suitable for formal verification of mathematical proofs, where proofs are based on Jaskowski natural deduction. Mizar is also a language in which these texts are written. The language is intended to be understandable both by computers and humans. The huge part of the system is the Mizar Mathematical Library, a collection of Mizar articles containing proofs of mathematical facts.
The first hour is the COPLAS talk proper. Afterwards, there will be an opportunity for interested attendees to try out the system themselves.
All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU, KVL and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to email@example.com with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see http://www.coplas.org