COPLAS Talk: Isabelle’s Truly Modular (Co)datatypes and Beyond


Isabelle’s Truly Modular (Co)datatypes and Beyond


Foundational proof assistants, like Isabelle, are built around a small inference kernel with few primitives to which all other specification mechanisms are reduced. The foundational approach provides the highest level of trustworthiness. In Isabelle's higher-order logic (HOL) there are two primitives: a mechanism for defining non-recursive functions and a mechanism for defining non-recursive types as being isomorphic to a subset of an existing type. I describe a line of work, which started in 2011, that developed foundational constructions for more advanced type and function specifications via reduction to the above primitives. The constructions include

  • inductive datatypes,
  • their coinductive counterpart, the codatatypes,
  • non-primitively corecursive function definitions,
  • non-uniform (co)datatypes, in which the type arguments vary recursively, and
  • (co)datatypes with bindings, which identify their elements modulo alpha-equivalence

and come with the corresponding reasoning and definitional principles. 

Dmitriy TraytelSpeaker Dmitriy Traytel

Since August 2020, Dmitriy is an associate professor at UCPH, part of DIKU’s Software, Data, People & Society section. Prior to this position, he worked  as a senior researcher in David Basin's information security group at ETH Zürich. Dmitriy completed his PhD in 2015 in Tobias Nipkow's logic and verification group at TU München. His research interests include logic, automata, runtime verification and monitoring, decision procedures, (co)induction and (co)recursion, and interactive theorem proving.

HostFritz Henglein (DIKU, tel. +45-30589576

All are welcome. No registration required.