DIKU ITU KVL

Copenhagen Programming Language Seminar

COPLAS Talk

What do we gain by Integrating a Programming Language with a Theorem Prover?

Paul J. Voda
University of Bratislava, Slovakia and Department of Computer Science, University of Copenhagen, Denmark

Thursday, October 24th, 15:15-16:00
DIKU, Universitetsparken 1, room N034

Abstract:

Beside the obvious gains of having a good declarative semantics for the programming language (Why to integrate otherwise?) and of computer-aided proofs of properties of programs (such as their conformance with their specifications) we can design the language with a massively extensible syntax.

We will first illustrate the current state of art with the programming language CL designed and implemented in Bratislava. The formal theory of CL is the simplest of formal theories: Peano Arithmetic (PA). Definitions of functions and predicates are just formulas of PA which conservatively extend PA by definitions. Although a first-order language, CL is not a toy language because it has been used for six years now in the undergraduate teaching at the University of Bratislava. Up to 300 students pass yearly through the four courses based on CL.

CL has a wide set of pattern matching constructs which go far beyond the ones known from the functional programming languages. The advantage of pattern matching over the traditional case (if-then-else) constructs lies in the vastly increased readability of programs. In addition, the programs obtain a mathematical look and feel. We will illustrate this point with a brief demo of CL during the talk. The current implementation of CL has a fixed set of pattern matching constructs (we call them discriminators ).

The main topic of the talk is a proposal of how to make pattern matching extensible. User-defined discriminators must be proved correct in PA before they can be used in definitions of functions and predicates. Since discriminators can be conditional (the ones implemented in the current CL are unconditional), they may be used in definitions only when their conditions are met. This must be again demonstrated by a proof (by so-called proof obligations).

The talk will discuss the consequences of such extensible syntax; one of which is that programs cannot be syntactically analyzed but must be prompted in a top-down fashion.

Scientific host: Andrzej Filinski. Administrative host: Camilla Jørgensen. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, IT-C and KVL.
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