Tau Language
In development
Tau Language is a novel temporal logic designed mainly for software specification, describing finite and infinite sequences and trees of sentences in some logics. It allows many more programs to be written by means of logical formal specification compared to other specification languages. This means there is no longer a need to deal with the “how” but only with the “what“.
Programming becomes writing down constraints about the program
Tau Language is purely declarative, but in contrast to other declarative programming languages, the specification doesn’t need to pin down a unique program. Instead, many programs can meet the requirements. Currently available specification languages are not rich enough, in particular, because they have limited forms of inputs and outputs. Tau Language allows infinitary kind of inputs, outputs, and states, making it a breakthrough in logics for software specification that overcomes many of the bottlenecks which have been holding the formal methods back from becoming widely used.
Decidable Temporal Logic
Tau Language has a strong aspect of homoiconicity, where data and specification may take the same form. It therefore makes a decidable temporal logic with infinite datawords that come with a theory and not only equality, as well as being closed under Boolean combinations.
Supports certain second-order features
Tau Language has the ability to quantify over functions between sequences and trees, under what we call “time compatibility” semantics.
Supports Description Logics
These logics can be Tau Language itself, and it also comes with a support for certain Description Logics, while maintaining the ability to add more logics in a backward-compatible manner.
Technical Details
See here to read a low level description of Tau Language.
Licensing and Support
We provide technical support: bug fixes, how-to’s, and efficient answers tailored to your solution.
Contact us for questions on licensing and support:
