From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id C5ED780138 for ; Wed, 17 May 2017 15:58:16 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=helmut.brandl@gmx.net; spf=Pass smtp.mailfrom=helmut.brandl@gmx.net; spf=None smtp.helo=postmaster@mout.gmx.net Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of helmut.brandl@gmx.net) identity=pra; client-ip=212.227.15.15; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="helmut.brandl@gmx.net"; x-sender="helmut.brandl@gmx.net"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of helmut.brandl@gmx.net designates 212.227.15.15 as permitted sender) identity=mailfrom; client-ip=212.227.15.15; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="helmut.brandl@gmx.net"; x-sender="helmut.brandl@gmx.net"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mout.gmx.net) identity=helo; client-ip=212.227.15.15; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="helmut.brandl@gmx.net"; x-sender="postmaster@mout.gmx.net"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3ACTHuyhyHahMHAk3XCy+O+j09IxM/srCxBDY+r6Qd?= =?us-ascii?q?1OwTIJqq85mqBkHD//Il1AaPBtSHraocw8Pt8InYEVQa5piAtH1QOLdtbDQizf?= =?us-ascii?q?ssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1?= =?us-ascii?q?JuPoEYLOksi7ze6/9pncbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeu?= =?us-ascii?q?BWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbO?= =?us-ascii?q?SxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRHolC?= =?us-ascii?q?gIODA3/nzUhMJui6xWuwiuqwB6w4POYIGZKPhzc6XAdt0aX2pBWcNRWjRDDIyi?= =?us-ascii?q?a4sPCvcBPfpFpITgvVsBtx2+ChSoBOjyzTJIhmH53ak/0+Q8DQHKxhcvH8gUv3?= =?us-ascii?q?TSsdr1MLwfUe+wzKjH1znDae1Z2Svk5YXObxsvr/aMXbdqfsrQz0kiDwzFjlSM?= =?us-ascii?q?qYP+ODOV0ecNv3KH4OpnUOKijXMspQJpojW32Msgl5fFipgLxlza9yh12ps5KN?= =?us-ascii?q?2iREJmYdOoCIZcuiKYOodsXM8uXm5ltDwkxrAIupO3ZjUGxZspyhPZdveJaZKH?= =?us-ascii?q?4gj5W+aUOTp4hGxqeLa4hxuq9EigzfD8VtWu3FZFqypEncPAtnYT2BzP8sSHS/?= =?us-ascii?q?198Vm92TuXyQzf9/9ILVoqmabFKZMt2KM8m5oJvUjeHiL6gED2g7WXdkUg9Oio?= =?us-ascii?q?8ePnYrD+q5+cKYB0jgT+MrkymsClGus4KBIBX26G9uS4z7Dj8kj5QbpQgv0wjK?= =?us-ascii?q?bZrIjWJd4Hqa6hHw9VzoEj5g6jADi81dQYmWALLFZEeBKck4jkIErOIfD9Dfen?= =?us-ascii?q?mVugijZrx/bcPr3gGJrBNHbDkK2yNYp6vkVVzQ570MtS/YkcXroIJfa2Xk7qqP?= =?us-ascii?q?TZCAU4Okq62bC0Js9609Y+VGaKH7PRGrnbt1OMrrYvLu2JeZNTsiz0LfQhz/Hr?= =?us-ascii?q?nTk/lENLLvrh5ocedH3tRqcuGE6ee3e52to=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AgCgA3VhxZhw8P49RcHgYMGQYMhAwDh?= =?us-ascii?q?Ha0Ag4egkKJE0MUAQEBAQEBAQEBAQESAQEBCA0JCCgvgjMigm1KBSYBPQJfih0?= =?us-ascii?q?BGgIKnHiEBIwHgiaGaAGEHgsBAQEBHgWGX4IJhWyEPAwxL4IxBZErjGWCEJMPi?= =?us-ascii?q?H8jhkUCkAKERDaBKy8gLGIBglKCIoINiUABAQE?= X-IPAS-Result: =?us-ascii?q?A0AgCgA3VhxZhw8P49RcHgYMGQYMhAwDhHa0Ag4egkKJE0M?= =?us-ascii?q?UAQEBAQEBAQEBAQESAQEBCA0JCCgvgjMigm1KBSYBPQJfih0BGgIKnHiEBIwHg?= =?us-ascii?q?iaGaAGEHgsBAQEBHgWGX4IJhWyEPAwxL4IxBZErjGWCEJMPiH8jhkUCkAKERDa?= =?us-ascii?q?BKy8gLGIBglKCIoINiUABAQE?= X-IronPort-AV: E=Sophos;i="5.38,354,1491256800"; d="scan'208,217";a="273519492" Received: from mout.gmx.net ([212.227.15.15]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES128-GCM-SHA256; 17 May 2017 15:57:54 +0200 Received: from [192.168.1.67] ([187.214.238.143]) by mail.gmx.com (mrgmx003 [212.227.17.190]) with ESMTPSA (Nemesis) id 0Lh7PL-1doSfu1jrr-00oSZD; Wed, 17 May 2017 15:57:53 +0200 From: Helmut Brandl Content-Type: multipart/alternative; boundary="Apple-Mail=_74087290-E96E-4B36-8744-643EB5980E3D" Mime-Version: 1.0 (Mac OS X Mail 10.3 \(3273\)) Date: Wed, 17 May 2017 08:57:49 -0500 Message-Id: <7745EA50-EE24-4E73-B095-4A77117B8DF5@gmx.net> To: caml users X-Mailer: Apple Mail (2.3273) X-Provags-ID: V03:K0:UJaf+42bAQ7n8oS+kQBlVo27v3xEKoecVc7El9WFHfHpLZ+BnvP AbPptW8C9zgd0yTzLa9w3WRQUhLU+Rdo1t1QpRZW1BMPxbSsA+E24My7I2MWssz1JvKmcAI VlVdc1v4HLdqk9w+BRssvGDRdQ2qVXanpg2dgL/ecgqcFdrSsKEiHbhbt+5w49WwpbacZZP 22qyTUyvr+D/dVMCW51xg== X-UI-Out-Filterresults: notjunk:1;V01:K0:a9Tc+DZnIv8=:pRQQ3c0+09TiAkNnRU5aVt woBk7exk429Ec84lujKPfp2pv6WpAvtdIS7r4tsVuqr83pjz0p8Tm3KvFHDAj4tqZL6o1d1g5 lyZozFR3RaTDhXeax+vMsYe6BjMX1nOnIlPO+1rkfszp41vkKyi9b6LcRw7BewDIBj/2iPTfs NHWgA4ogmVcINL8yAbTrgu+Vn2WYqO64J2y8TcspO0ZOQAAaXA4ERJZowcIiekWk2iE5YiJ+N hdF8ssJX8dsa73k2Z6xYHP3LCkzznM+8CjtjyJb7mYxgxOnYNV1nDrEbJHlQyBTtvmoY0NO4v Cr+N/GKUjXvCPkf3srxfRgrmbx5WBXTixW5OmPJyJGvszHpEuoM0LwaMohoTXXa94BOu/HZKw jkbjMCQYZI3Af/+xkB4LSxlb9qYG5pD9hyoeHeNCUJ3HK1A75UvCSL381WCsMUCD3HtCx6zH+ fbooObizhmzmiUOmz5gsMdT+4t7sXnL6zHXvuGzog8fbAU1IjPXiR+8lntoDitGJ+JtBw86JK 4V8VKIWegy4Hkl61ptnh/8Ofr3BqtKZ3Kg6EpLg+tKlCiN5NJCvPqXMcCMx0JD/iVkRSaA7jY oFY3dcBLfDihuyD0OTkmaa74rQCRor/mhX0hgO0TRamvUz7k260Og5dJiq4dVWbAIlKj4h2ll sfuaov0EGRXUsjgr6uw9eMGQC5NRWs6XG+stWY+gIqRApyvDZlnCkDfcf+YaX1Zv1C//lqKwQ X6Kglgtgh+MR3c/D21UgbkoZcaf2y7jb3tYNykSwoGxB/rHf968CJsN93Z7HHwexwcDmuWmTy xxj1iJm Subject: [Caml-list] ANN: New release of the Albatross compiler available via opam --Apple-Mail=_74087290-E96E-4B36-8744-643EB5980E3D Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 It is my pleasure to announce a new version of the compiler for the Albatro= ss programming language. It is available via =E2=80=98opam install alba=E2= =80=99 (it requires ocaml >=3D 4.03.0). Alba is a language which allows static verification. In its current state i= t supports inductive types, recursive functions, pattern matching, inductiv= ely defined sets and relations and abstract data types. It can be used like= coq to define types and functions and prove properties about them. We clai= m that Albatross is easier to use than coq and closer to mainstream languag= es so that there is no steep learning curve. The design of the language is an ongoing activity. Any comments, hints, iss= ue reports etc. are welcome. Its long term goal is to open software verific= ation for the masses. A language description can be found at https://www.gitbook.com/read/book/hb= r/alba-lang-description .= --Apple-Mail=_74087290-E96E-4B36-8744-643EB5980E3D Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8 It is my pleasure = to announce a new version of the compiler for the Albatross programming lan= guage. It is available via =E2=80=98opam install alba=E2=80=99 (it requires= ocaml >=3D 4.03.0).

Alba is a language which allows static verification. In its current state = it supports inductive types, recursive functions, pattern matching, inducti= vely defined sets and relations and abstract data types. It can be used lik= e coq to define types and functions and prove properties about them. We cla= im that Albatross is easier to use than coq and closer to mainstream langua= ges so that there is no steep learning curve.

The design of the language is an ongoing activ= ity. Any comments, hints, issue reports etc. are welcome. Its long term goa= l is to open software verification for the masses.
A language description can be found at&nb= sp;https://www.gitbook.com/read/book/hbr/alba-lang-description.=
= --Apple-Mail=_74087290-E96E-4B36-8744-643EB5980E3D--