From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id DD738BC69 for ; Sat, 12 May 2007 07:06:10 +0200 (CEST) Received: from ipmail01.adl2.internode.on.net (ipmail01.adl2.internode.on.net [203.16.214.140]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l4C568CP013310 for ; Sat, 12 May 2007 07:06:09 +0200 X-IronPort-AV: E=Sophos;i="4.14,525,1170595800"; d="scan'208";a="126503956" Received: from ppp8-148.lns1.syd7.internode.on.net (HELO [192.168.1.201]) ([59.167.8.148]) by ipmail01.adl2.internode.on.net with ESMTP; 12 May 2007 14:36:07 +0930 Subject: Felix 1.1.3 released From: skaller To: caml-list@inria.fr Content-Type: text/plain; charset=UTF-8 Date: Sat, 12 May 2007 15:06:03 +1000 Message-Id: <1178946363.14691.54.camel@rosella.wigram> Mime-Version: 1.0 X-Mailer: Evolution 2.10.1 Content-Transfer-Encoding: 8bit X-Miltered: at concorde with ID 46454B40.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; osx:01 cygwin:01 ocaml:01 ocaml:01 haskell:01 threading:01 haskell:01 variants:01 typeclass:01 axioms:01 rewriting:01 axioms:01 semantics:01 emits:01 lri:01 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 Felix, successor to C++: http://felix.sf.net