Markus Pfeiffer
2018-04-27 08:52:28 UTC
Dear all!
We would like to invite abstracts (for talks, software demonstrations,
posters, etc) for the new workshop
1st WORKSHOP ON COMPUTER ALGEBRA IN THE AGE OF TYPES (CAAT2018)
at CICM 2018:
https://cicm-conference.org/2018/cicm.php?event=caat
August 13-17, 2018
Hagenberg, Austria
THEME
-----
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 is through EasyChair
https://easychair.org/conferences/?conf=caat2018. If you have any
further questions, please do not hesitate to contact me by email.
Cheers,
Markus
We would like to invite abstracts (for talks, software demonstrations,
posters, etc) for the new workshop
1st WORKSHOP ON COMPUTER ALGEBRA IN THE AGE OF TYPES (CAAT2018)
at CICM 2018:
https://cicm-conference.org/2018/cicm.php?event=caat
August 13-17, 2018
Hagenberg, Austria
THEME
-----
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 is through EasyChair
https://easychair.org/conferences/?conf=caat2018. If you have any
further questions, please do not hesitate to contact me by email.
Cheers,
Markus