You must enable JavaScript to use this site
  • Computer Algebra in the Age of Types

    The workshop will take place on Friday the 17th of August 2018.


    Time Title Speaker
    9:00-10:00 Keynote Michael Kohlhase (FAU Erlangen)
    10:30-11:00 Categories, Algorithms, and Programming Sebastian Posur (University of Siegen)
    11:00-12:30 Idris Edwin Brady (University of St Andrews)
    14:00-15:30 MMT Dennis Müller (FAU Erlangen)
    16:00-17:30 Discussion, prototyping and development with Idris, MMT, and other tools All participants


    Computer algebra, being one of the oldest computational disciplines, keeps growing rapidly. Most code is available as open source software: Constructive code tends to be written in very weakly typed systems like Python (notably Sage), GAP, C, or C++. Formal systems naturally carry strong typing and formal proof tools.

    There is still, somewhat surprisingly, very little connection between the two disciplines, though many attempts have been made to bridge the gap by devising new systems that incorporate strong typing, proof assistants, and powerful (bespoke) programming languages.

    This workshop advocates a slightly different approach: For modern computational mathematics to thrive we want to promote the use of types to

    • compose existing constructive and formal systems with a low initial overhead, and a strong incentive towards eventual formal checkability and correctness,
    • enable development of domain specific tools that make computations and algorithms in mathematical domains more natural, concise, and avoid large classes of common errors and cognitive overhead.
    • provide access to machine verified proofs for use in computation and algorithm development
    • provide access to efficient computations for use in proofs
    • enable effective automated testing a-la Haskell's Quickcheck
    This workshop is to provide an incubator for this approach, featuring a tutorial on the programming language Idris ( by its author Edwin Brady, and an introduction to the system MMT (, inviting practising researchers in computer algebra, formal methods, and programming languages to present and discuss approaches and form a common vision for the next generation of computer algebra.

    Topics of Interest

    • Type systems in computer algebra software
    • (Computer) algebra in type systems
    • Interfacing mathematics software using types
    • Mathematical challenges for contemporary computer algebra
    • Tools for using types in algorithm development and implementation
    • Work in progress
    • Real world applications

    Invited speakers

    Keynote Lecture by Professor Michael Kohlhase (FAU Erlangen-Nürnberg)


    Submissions are welcome for papers, software presentations, and posters. Contributors should submit a short abstract (no more than 4 pages) through EasyChair. It is expected that at least one author of each accepted submission is present at the workshop to give a presentation.

    Important dates

    Deadline for submissions: 2. June 201821. June 201
    Notification of acceptance: 1st July 2018

    Programme Committee (TBC)

    • Markus Pfeiffer, University of St Andrews
    • Gabriel Dos Reis, Microsoft Research
  • News

    • CICM is over
    • award winners online
    • detailed program online
    • accepted papers online
    • registration open
    • program overview online
    • deadline extended: April 22 (abstract), April 29 (paper)
    • 6 workshops accepted
    • 3 invited speakers
    • CfP and CfW available
    • PC completed
    • initial website online
Privacy policy and legal information
Last modified: August 06 2018 12:55:25 CEST