Tools on Rewriting
-
Maude is a high-performance reflective language and system supporting both equational and rewriting logic specification and programming for a wide range of applications. Maude has been influenced in important ways by the OBJ3 language, which can be regarded as an equational logic sublanguage. Besides supporting equational specification and programming, Maude also supports rewriting logic computation.
* Maude download and installation ... * This page was last modified on 20 March 2024, at 13:32. * This page has been accessed 858,853 times....
-
ACL2 is a very large, multipurpose system. You can use it as a programming language, a specification language, a modeling language, a formal mathematical logic, or a semi-automatic theorem prover, just to name its most common uses.
ACL2 Version 8.3 ... paper note icon Differences from Version 8.2 tiny warning icon filing ... April 14, 2020 ... * ACL2+Books Manual (Version 8.3) ... * ACL2 User's Manual (Version 8.3)...
-
Agda is a dependently typed functional programming language. It has inductive families, i.e., data types which depend on values, such as the type of vectors of a given length. It also has parametrised modules, mixfix operators, Unicode characters, and an interactive Emacs interface which can assist the programmer in writing the program. Agda is a proof assistant. It is an interactive system for writing and checking proofs. Agda is based on intuitionistic type theory.
* (2018-10-29) Agda 2.5.4.2 is now available. ... Page last modified on October 29, 2018, at 05:08 PM...
-
SML# is a new programming language in the Standard ML family being developed at RIEC (Research Institute of Electrical Communication), Tohoku University jointly with Sanpu Koubou Inc. Its design goal is to provide a moderate but practically important extensions (see features of SML#) while maintaining the compatibility of the Definition of Standard ML.
Powered by Ruby 2.0.0-p648 (2015-12-16)....
-
Objective Caml is the most popular variant of the Caml language. From a language standpoint, it extends the core Caml language with a fully-fledged object-oriented layer, as well as a powerful module system, all connected by a sound, polymorphic type system featuring type inference. The Objective Caml system is an industrial-strength implementation of this language, featuring a high-performance native-code compiler (ocamlopt) for 9 processor architectures (IA32, PowerPC, AMD64, Alpha, Sparc, Mips, IA64, HPPA, StrongArm), as well as a bytecode compiler (ocamlc) and an interactive read-eval-print loop (ocaml) for quick development and portability.
The most recent version of OCaml is 4.07.0. It was released on 2018-07-10. ... Some of the highlights in release 4.07 are: * The way the standard library modules are organized internally has ...
-
Q is an interpreted, dynamically typed functional programming language based on term rewriting which allows you to define functions using symbolic equations. It works on Linux, OS X, Unix and Windows, and comes with a bunch of useful libraries which turn it into a practical programming tool. The Q programming system is free software distributed under the GPL.
Q - Equational Programming Language ... News About Examples Documentation Lists Core Add-Ons Download Links [SourceForge] ... Please note that Q has been superseded by the Pure progr...
-
CafeOBJ is a new generation algebraic specification and programming language. As a direct successor of OBJ, it inherits all its features (flexible mix-fix syntax, powerful typing system with sub-types, and sophisticated module composition system featuring various kinds of imports, parameterised modules, views for instantiating the parameters, module expressions, etc.) but it also implements new paradigms such as rewriting logic and hidden algebra, as well as their combination.
-
GURU is a pure functional programming language, which is similar in some ways to Caml and Haskell. But GURU also contains a language for writing formal proofs demonstrating the properties of programs. So there are really two languages: the language of programs, and the language of proofs. When the compiler checks a program, it computes a type for it, just as compilers for other languages like JAVA do. But in GURU, such types can be significantly richer than in mainstream or even most research programming languages. These types are called dependent types, and they can express non-trivial semantic properties of data and functions. Analogously, when the compiler checks a proof, it computes a formula for it, namely the formula the proof proves. So we really have four kinds of expressions in GURU: programs (which we also call terms) and their types; proofs and their formulas.
READ-ONLY: This project has been archived. For more information see this post....
-
GHC is a state-of-the-art, open source, compiler and interactive environment for the functional language Haskell. Highlights: * GHC supports the entire Haskell 2010 language plus a wide variety of extensions. * GHC has particularly good support for concurrency and parallelism, including support for Software Transactional Memory (STM). * GHC generates fast code, particularly for concurrent programs. Take a look at GHC's performance on The Computer Language Benchmarks Game. * GHC works on several platforms including Windows, Mac, Linux, most varieties of Unix, and several different processor architectures. There are detailed instructions for porting GHC to a new platform. * GHC has extensive optimisation capabilities, including inter-module optimisation. * GHC compiles Haskell code either directly to native code or using LLVM as a back-end. GHC can also generate C code as an intermediate target for porting to new platforms. The interactive environment compiles Haskell to bytecode, and supports execution of mixed bytecode/compiled programs. * Profiling is supported, both by time/allocation and various kinds of heap profiling. * GHC comes with several libraries, and thousands more are available on Hackage.
11 July 2014 GHC 7.8.3 Released! [download]...