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
This workshop is to 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.
Programme Committee (TBC)
Markus Pfeiffer, University of St Andrews
Gabriel Dos Reis, Microsoft Research
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
Submissions
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.
08月13日
2018
08月17日
2018
初稿截稿日期
摘要截稿日期
初稿录用通知日期
注册截止日期
留言