[Club2] Talk by Andrei Popescu: Friday, Dec. 6, 15:00, Room: Konrad Zuse (01.11.018)

[Andrei Popescu]

Dear All,  

Tomorrow, Friday, I will talk about nonfree datatypes in Isabelle/HOL. 
This is a rehearsal for my CPP presentation next week in Melbourne. 

http://cpp2013.forge.nicta.com.au/    

Please note the unusual (time and) place.  

Cheers, 
  Andrei  

Nonfree Datatypes in Isabelle/HOL
Andrei Popescu
joint work with Andreas Schropp
======================================================================
Friday, Dec. 6, 15:00, Room: Konrad Zuse (01.11.018)

Datatypes freely generated by their constructors are well supported in
mainstream proof assistants. Algebraic specification languages offer more
expressive datatypes on axiomatic means: nonfree datatypes generated from 
constructors modulo equations.  

We have implemented an Isabelle/HOL package for nonfree datatypes, without 
compromising foundations. The use of the package, and its nonfree iterator in particular,
is illustrated with examples: bags, polynomials and lambda-terms  
modulo $\alpha$-equivalence. The many-sorted metatheory of nonfree datatypes is formalized 
as an ordinary Isabelle theory and is animated by the package into user-specified instances.
HOL lacks a type of types, so we employ an ad hoc construction of a universe embedding the 
relevant parameter types.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20131205/f031609c/attachment.html>