HEVEA is a LaTeX to HTML translator. The input language is a fairly
complete subset of LaTeX2e (old LaTeX style is also accepted) and
the output language is HTML.

Coq is a proof assistant which allows to handle calculus assertions, check mechanically proofs of these assertions, helps to find formal proofs and extracts a certified program from the constructive proof of its formal specification.

Flocq (Floats for Coq) is a floating-point formalization for the Coq
system. It provides a comprehensive library of theorems on a
multi-radix multi-precision arithmetic. It also supports efficient
numerical computations inside Coq.

The Metamath language is a language to write theorems and formal proofs for them. The Metamath program can parse files in the Metamath language and verify the proofs.

OpenCL is a royalty-free standard for cross-platform, parallel programming of modern processors found in personal computers, servers and handheld/embedded devices.

This package provides the official C++ headers for OpenCL, which are wrappers around the C headers.

TreeMaker is a program for the design of origami bases. You draw a stick figure of the base on the screen; each stick in the stick figure (the “tree”) will be represented by a flap on the base. You can also place various constraints on the flaps, forcing them to be corner, edge, or middle flaps, and/or setting up various symmetry relationships (forcing pairs of flaps to be symmetric about a line of symmetry of the paper, for example). Once you have defined the tree, TreeMaker computes the full crease pattern for a base which, when folded, will have a projection (roughly speaking, its “shadow”) equivalent to that specified by the defining tree. The crease pattern can be printed out, or copied and pasted into another graphics program for further processing.