Lambda the Ultimate

via OCaml

The Calculemus 2005 Symposium on July 18-19, 2005 will explore the mission of the Calculemus project:

The scientific and technological goal...is the design of a new generation of mathematical software systems and computer-aided verification tools based on the integration of the deduction and the computational power of Deduction Systems and Computer Algebra Systems respectively.

Both Deduction Systems and Computer Algebra Systems are receiving growing attention from industry and academia. On the one hand, Mathematical Software Systems have been commercially very successful in recent years....On the other hand, the use of formal methods in hardware and software development has made Deduction Systems indispensable not least because of the complexity and sheer size of the reasoning tasks involved.

In spite of these successes there is still need for improvement as many application domains still fall outside the scope of existing Deduction Systems and Computer Algebra Systems. For instance, the scope of Computer Algebra Systems (CASs) could be significantly enhanced by adding deductive reasoning power. In fact this lack of expressivity together with the unsolved problem of correctness prohibit large classes of applications. Deduction systems (DSs), which - on the other hand - provide such an expressivity, as well as the guarantee of correctness, still lack computational power as they are not suited to directly carry out algebraic or numerical calculations. This severely restricts their scope of application in mathematics and - more importantly - in engineering applications.

Earlier we discussed the Axiom CAS.

Sergey Dmitriev of JetBrains has written a whitepaper on domain specific languages. It is called "Language Oriented Programming: The Next Programming Paradigm" and is available at Language Oriented Programming