Alice ML is a functional programming language that enriches the statically typed, closed functional world of ML with extensive support for type-safe programming of concurrent, distributed, and open systems. It also features cutting-edge constraint programming technology in the tradition of Oz/ Mozart. Alice ML is a mostly conservative extension of Standard ML.
FFTW is a fast C FFT library. It includes complex, real, symmetric, multidimensional, and parallel transforms, and can handle arbitrary array sizes efficiently.It is typically faster than other freely available FFT implementations, and is even competitive with vendor-tuned libraries (benchmarks are available at the homepage). To achieve this performance, it uses novel code generation and runtime self optimization techniques (along with many other tricks).
FaCiLe is a constraint programming library over integer finite domain written in OCaml. It offers all usual facilities to create and manipulate finite domain variables, arithmetic expressions and constraints (possibly non-linear), built-in global constraints, and search goals. It also allows you to build easily user-defined constraints and goals (including recursive ones), making pervasive use of OCaml higher-order functionals to provide a simple and flexible interface for the user.
Higher Order Logic (HOL) is a programming environment in which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems. An Oracle mechanism gives access to external programs such as SAT and BDD engines. HOL 4 is particularly suitable as a platform for implementing combinations of deduction, execution, and property checking.
HOL-TestGen allows one to write test specifications in Higher-order logics (HOL). It can (semi-) automatically partition the input space, resulting in abstract test cases, and automatically select concrete test data. Automatic generation of test harnesses (in SML) is supported, and using a foreign language interface, implementations in arbitrary languages (e.g. C) can be tested.