On 22-Nov-2019 I have delivered the following talk at TUM (Garching bei München):
- Export of formal theory content in Isabelle/Scala
- 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.
- Slides with sources, which include practically relevant links and examples.