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 B20418239C for ; Mon, 29 Jan 2018 17:26:55 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=nicolas.ratier@femto-st.fr; spf=Pass smtp.mailfrom=nicolas.ratier@femto-st.fr; spf=None smtp.helo=postmaster@mail.femto-st.fr Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of nicolas.ratier@femto-st.fr) identity=pra; client-ip=194.57.88.66; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="nicolas.ratier@femto-st.fr"; x-sender="nicolas.ratier@femto-st.fr"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of nicolas.ratier@femto-st.fr designates 194.57.88.66 as permitted sender) identity=mailfrom; client-ip=194.57.88.66; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="nicolas.ratier@femto-st.fr"; x-sender="nicolas.ratier@femto-st.fr"; 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@mail.femto-st.fr) identity=helo; client-ip=194.57.88.66; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="nicolas.ratier@femto-st.fr"; x-sender="postmaster@mail.femto-st.fr"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3An4rZ1xB5OeAvv/JdHMoCUyQJP3N1i/DPJgcQr6Af?= =?us-ascii?q?oPdwSPv+r8bcNUDSrc9gkEXOFd2Cra4c0qyO6+jJYi8p2d65qncMcZhBBVcuqP?= =?us-ascii?q?49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6?= =?us-ascii?q?JvjvGo7Vks+7y/2+94fcbglUmTaxe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfO?= =?us-ascii?q?pWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnM?= =?us-ascii?q?VhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykC?= =?us-ascii?q?oJKiA38G/XhMJzgqxUrh2uqB5jzIPPeo6ZKOBzc7nBcd4UR2dMWNtaWSxbAoO7?= =?us-ascii?q?aosCF/IPPedEoIn6o1sBtwC+DhSwCuz11j9Ih2H53bcn2OkmFwHG3RAvH9UKsH?= =?us-ascii?q?vOt9X5Lr0SXvqpzKnJ0zrDdehb2Tnj54jNbhAhpuiAXalsccbLx0kvDRrIg1ON?= =?us-ascii?q?ooLmJzOYzvkBvmyU4uZ6Ve+iiXQrpgJyrzS1x8ohi5HFip8Rx13L7yl13Yc4KN?= =?us-ascii?q?+iREN0YdOoCoVcui6VOoZwX8gsWXtnuDwgxb0DoZO7fDYFyJAgxxPHbvyIaYmI?= =?us-ascii?q?4hb5WOafPzh4gW5leLWmixap7Uis0OP8VtOs3FZLqCpKjMXMu2gQ2xHX5cWLUP?= =?us-ascii?q?tw80W71TuM1A3f8OBJLEEsmareMZEhw7owlpQJsUTEGy/7gEP2jK6KeUUj/uin?= =?us-ascii?q?8f/nbq/8ppCGK490ix/xMr41l8yxH+s4NxQOX2+C9eSnyL3v50P5QK9Sgv0sjq?= =?us-ascii?q?bZqIzaJdgcpqOhHwBayIMj6xKmAzei0dQYhmUHIUleeBOHiojpI0vBLOr5Dfe5?= =?us-ascii?q?mVSskS1ky+rIPr37Ud3xKS3ImbLlOLJ88FIUnAE6yNQa45NPFpkAJujyUwn/ro?= =?us-ascii?q?qLIAU+NlmSwu3gDNxmnrkXRWOCGOfNNqLZtluB/aQ1KvWNaZU9tjv4N/9g/OKo?= =?us-ascii?q?g2VvygxVRrWgwZZCMCPwJf9hOUjMOSO90OdEKn8Du08FdMKvjVSDVTBJYHPrBP?= =?us-ascii?q?Ay6zQnD8e9EcHNXNL02eDT7GKABpRTI1t+JBWUC36xLNeKVvIQb2eJPolviG5c?= =?us-ascii?q?DOXze8oazRir8TTC5f9nI+7To31KsJvi0J576ujPklQp6Xp6FZbF3g=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DYAwCOSm9ah0JYOcJcHQIFDIQscoQIi?= =?us-ascii?q?xinPIIWCoU7AoJSBwQ3EQEBAQEBAQEBAQEBEgEBAQoLCQgoL4I4IoJKBiMEYg8?= =?us-ascii?q?BPQICVwYNCAEBijWmAYFtOiaKLgwBJYRUg2yCEYs+gmUFimqZKoEWgTSXO4gPh?= =?us-ascii?q?3yXNQIECwIZAYE8OQ2BYjMaJ4J5gmSCE497AQEB?= X-IPAS-Result: =?us-ascii?q?A0DYAwCOSm9ah0JYOcJcHQIFDIQscoQIixinPIIWCoU7AoJ?= =?us-ascii?q?SBwQ3EQEBAQEBAQEBAQEBEgEBAQoLCQgoL4I4IoJKBiMEYg8BPQICVwYNCAEBi?= =?us-ascii?q?jWmAYFtOiaKLgwBJYRUg2yCEYs+gmUFimqZKoEWgTSXO4gPh3yXNQIECwIZAYE?= =?us-ascii?q?8OQ2BYjMaJ4J5gmSCE497AQEB?= X-IronPort-AV: E=Sophos;i="5.46,431,1511823600"; d="scan'208,217";a="311148310" Received: from lifc.univ-fcomte.fr (HELO mail.femto-st.fr) ([194.57.88.66]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 29 Jan 2018 17:26:55 +0100 Received: from [172.16.120.211] (nat-tf.ens2m.fr [194.167.45.244] (may be forged)) (authenticated bits=0) by mail.femto-st.fr (8.14.4/8.14.4/Debian-4+deb7u1) with ESMTP id w0TGQrfT002779 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES128-SHA bits=128 verify=NOT) for ; Mon, 29 Jan 2018 17:26:53 +0100 To: caml-list References: <1515782196.604079108@f381.i.mail.ru> <937c674a-bf63-b2be-44eb-9ad331aa622f@ocamlpro.com> <1516012497.2168791.1235601456.5B7510E5@webmail.messagingengine.com> From: Nicolas Ratier Message-ID: <6d6e175f-bbdf-1ea3-a863-a27654caf323@femto-st.fr> Date: Mon, 29 Jan 2018 17:26:00 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.6.0 MIME-Version: 1.0 In-Reply-To: <1516012497.2168791.1235601456.5B7510E5@webmail.messagingengine.com> Content-Type: multipart/alternative; boundary="------------6437C6818F1DFF6BC8F88992" X-Scanned-By: MIMEDefang 2.71 on 194.57.88.66 Subject: [Caml-list] OCaml <-> Computer Algebra This is a multi-part message in MIME format. --------------6437C6818F1DFF6BC8F88992 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit Hello, We develop an OCaml code to automate repetitive calculations and to assemble proofs in the mathematical domain of PDE homogenization (to summarize in one sentence). We now need to embed elementary symbolic calculations. Do you know a library of "Computer Algebra" which interfaces well with OCaml? Does COQ need symbolic calculus? If so, is there a core of CA in COQ? Thank you for your help, Nicolas --------------6437C6818F1DFF6BC8F88992 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: 8bit

Hello,

We develop an OCaml code to automate repetitive calculations and to assemble proofs in the mathematical domain of PDE homogenization (to summarize in one sentence).

We now need to embed elementary symbolic calculations.
 
Do you know a library of "Computer Algebra" which interfaces well with OCaml?
Does COQ need symbolic calculus? If so, is there a core of CA in COQ?

Thank you for your help,
Nicolas

--------------6437C6818F1DFF6BC8F88992--