English version
Accueil     À propos     Téléchargement     Ressources     Contactez-nous    

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Browse thread
Felix 1.1.3 released
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2007-05-12 (05:06)
From: skaller <skaller@u...>
Subject: Felix 1.1.3 released
Felix 1.1.3 has been released and can be obtained from


(it's release candidate 4, but that's final in the 1.1.3).
It should build on all Unix systems, OSX, Cygwin, Win32,
and Win64 (using VS2005=VC7 or VS2007=VC8 compilers).
You will need Python, Ocaml, and either g++ or MSVC++ installed.
Please join mailing list for help building on Windows platforms.

Felix is an advanced language in the Algol/ML family,
with technology and ideas stolen from Ocaml and Haskell.
It generates ISO C++ code, and provides facilities for
easy binding to C and C++ using a NFI (Native interface)
generally not requiring any external glue logic.
It also features high performance user space cooperative 

Licence: FFAU (roughly BSD).

Roughly it is designed for C++ programmers who can't afford
to throw out legacy C/C++ libraries or frameworks, 
Ocaml/ML/Haskell programmers with the same problem,
applications requiring very high performance,
or researchers who want to implement production variants
of research ideas in a open code base.

This release was a long time coming because it adds a major
new feature -- Haskell style typeclasses. This facility
is equivalent to C++ template specialisation, but done right.
Second order support is 'just enough' to provide a Monad

In addition, this release supports first order axioms, reductions,
and lemmas. Reductions are user defined term rewriting rules.
Lemmas are propositions which can be proven from axioms.
These assertions can be written in typeclasses to provide
formal specification of some semantics.

Apart from automated checking of axioms by use cases, Felix now
emits Why code representing the axioms, and makes any
lemmas goals. The generated files can be submitted to
a theorem prover via Jean-Christophe Filliâtre Why program


or directly to Ergo. This system is of course work in 
progress, but it does verify at least one simple lemma :)

John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net