Datatypes and codatatypes are useful for specifying and reasoning about (possibly infinite) computational processes. The Isabelle/HOL proof as- sistant has recently been extended with a definitional package that supports both. We describe a complete procedure for deriving nonemptiness witnesses in the general mutually recursive, nested case—nonemptiness being a proviso for intro- ducing types in higher-order logic.
Wed 15 Apr Times are displayed in time zone: (GMT) Azores change
|10:30 - 11:00|
|11:00 - 11:30|
|11:30 - 12:00|
|12:00 - 12:30|