CICM2018 -- Workshop Computer Algebra in the Age of Types RISC Linz, Hagenberg, Austria, 17th of August 2018

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.

Workshops and Conferences