CAAT2018: Computer Algebra in the Age of Types |
Website | https://cicm-conference.org/2018/cicm.php?event=caat |
Submission link | https://easychair.org/conferences/?conf=caat2018 |
Abstract registration deadline | June 17, 2018 |
Submission deadline | June 17, 2018 |
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 by construction.
- enable development of domain specific tools that make computations and algorithms in mathematical domains more natural, concise, and avoid large classes of common errors caused by unnecessary 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 will provide an incubator for this approach, featuring a tutorial on the programming language Idris (https://www.idris-lang.org/) by its author Edwin Brady, and an introduction to the system MMT (https://uniformal.github.io), 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.
Submission Guidelines
We would like to invite abstracts (for talks, software demonstrations, posters, etc) for the new workshop. Submissions can be work in progress, demonstrations of previously published work, or original work.
List of Topics
- Computer Mathematics
- Dependent Types
- Practical Solutions
Organizing committee
- Markus Pfeiffer
- Gabriel Dos reis
Invited Speakers
- Edwin Brady (University of St Andrews)
- Michael Kohlhase (University of Erlangen)
- Dennis Müller (University of Erlangen)
Venue
The workshop will be held at CICM 2018, August 13-17, 2018 at RISC Linz, Hagenberg, Austria
Contact
All questions about submissions should be emailed to markus.pfeiffer@st-andrews.ac.uk