Department of Information Technology

General Binding in Nominal Isabelle

Speaker

Christian Urban, TU Munich

Date and Time

Thursday, March 3rd, 2010 at 15:15

Location

Polacksbacken, room 1245

Abstract

Nominal Isabelle is a definitional extension of the Isabelle/HOL theoremprover. It provides a proving infrastructure for reasoning about programming language calculi involving named bound variables (asopposed to de-Bruijn indices). We have extended Nominal Isabelle so that it can deal with terms which bind multiple variables at once. Such general bindings are ubiquitous in programming language research and only very poorly supported with single binders, such as lambda-abstractions. In this talk I will present the new definition of alpha-equivalence behind the extension and show how to establish automatically a reasoning infrastructure for the more general terms.

Back to the seminar page

Updated  2011-02-24 15:59:57 by Frédéric Haziza.