Main goals
We want to promote the use of types to compose existing constructive and formal systems, enable formal checkability and correctness, enable development of domain specific tools, provide access to machine verified proofs and efficient computations, enable effective automated testing.
OpenDreamKit implication
The workshop was organised by Markus Pfeiffer (UStan), his travel costs and conference fees were paid by OpenDreamKit. The keynote lecture at the workshop was given by Michael Kohlhase (FAU).
Event summary
Following an excellent keynote lecture given by Michael Kohlhase about the Math-in-the-Middle approach advocated by OpenDreamKit, we saw an excellent usecase of types in Sebastian Posur’s talk about categorical computation. Two tutorials, one on the programming language Idris by its creator Edwin Brady (University of St Andrews), and one by Dennis Müller (FAU) on the formal system MMT showed off what types can do for programming and mathematics today. Some of the workshop participants went to dinner together after the event.
Results and impact
A lively discussion about the vision of using type theory more in day-to-day mathematical programming, and for which purposes took place during the event and also in the breaks and at dinner. Some plans were discussed to use insights from the formal system MMT to drive executable code in Idris.