On 22-Nov-2019 I have delivered the following talk at TUM (Garching bei München):

Title:

Export of formal theory content in Isabelle/Scala

Abstract:

This is an overview of the state of affairs of systematic export of formal theory content. The general motivation is to provide semantically enriched views on the Isabelle/AFP library, without requiring a running Isabelle process. A typical application could be search over a database of digested theories, e.g. for an AFP web service.

Materials:

Slides with sources, which include practically relevant links and examples.