Copenhagen Programming Language Seminar
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.
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 email@example.com with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see http://www.coplas.org