Copenhagen Programming Language Seminar

Topics in the mechanisation of the meta-theory of formal systems.

Alberto Momigliano
University of Edinburgh

Thursday, August 16, 11-12:00
IT University of Copenhagen, Rued Langgaards Vej 7, Auditorium 3


The talk will be divided in two parts. In the first one, joint work with Amy Felty (Ottawa), we describe the new version of Hybrid, a system for reasoning using higher-order syntax in theorem proving systems such as Coq and Isabelle. This is a refinement of Miller et al. "two-level approach", where the representation and the reasoning over deductive systems is split into different levels so as to avoid the usual incompatibility of HOAS and inductive definitions (types). We exemplify the approach with the verification of properties of continuation machines with a ordered linear logic frameworks.

In the second part, joint work with James Cheney (LFCS), we investigate the dual problem of searching for errors in formalized systems, such as programming language calculi, type systems, operational semantics etc. We consider the problem of bounded model-checking for meta-theoretic properties of formal systems specified using logical framework such as nominal logic, although this can be applied to other logical frameworks, like Twelf. In contrast to the current state of the art for metatheory verification, our approach is fully automatic, does not require expertise in theorem proving on the part of the user, and produces counterexamples in the case that a flaw is detected. We present two implementations of this technique, one based on negation-as-failure and one based on negation elimination. These techniques seem fast enough to be used interactively to debug systems as they are developed.

Scientific host: Carsten Schürmann . Administrative host: Annette Enggaard . 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 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