Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss

[Caml-list] Felix 1.1.3 released

9 views
Skip to first unread message

skaller

unread,
May 12, 2007, 1:07:08 AM5/12/07
to caml...@inria.fr
Felix 1.1.3 has been released and can be obtained from

http://felix.sourceforge.net/flx_1.1.3_rc4_src.tgz

(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
threading.

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
typeclass.

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

http://why.lri.fr/

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

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

0 new messages