From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,HTML_MESSAGE,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: (qmail 29923 invoked from network); 20 Jan 2022 08:16:41 -0000 Received: from mail-wm1-x340.google.com (2a00:1450:4864:20::340) by inbox.vuxu.org with ESMTPUTF8; 20 Jan 2022 08:16:41 -0000 Received: by mail-wm1-x340.google.com with SMTP id j18-20020a05600c1c1200b0034aeea95dacsf6192732wms.8 for ; Thu, 20 Jan 2022 00:16:41 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1642666600; cv=pass; d=google.com; s=arc-20160816; b=fq5W1b332tT4cN/mV7MZjRCxFsyw4VWEK3DFDKwjgVt61pnk3ED/LpEWEVO+/CqNZb Z8ItNuetXDEMW6FRr+6WBqJyhLx0/awe+wCIZ+adUyitJeYxH1FYebOyo1A5WlhmjSni DU567KEJIrezfw3lUgwGY224wQ6FjRTlanTaI7GXyIlOEh/1dNMB4a18fGVUgvoDr27g Kf6nEsAnGagKmOfZG08u0QR0Ljqqo+Ah0s87KqCUvkCDus5BICPVZr3jdhfRefmg3TgD pkpkPPcIequqidPFHhTvVUCI1eyCWqmdbxIdwgOiP3EvdKn77rct8uU5haU9453xUjQ4 MXlg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:content-language:mime-version :user-agent:date:message-id:subject:from:to:sender:dkim-signature; bh=q3VveHHoQKbJ3Zd0085sLT4fQHNAUquAuuV+vn90ZsM=; b=FrBS+iDvsi47vYzKhu/GDDOSMnBRwtYoUv/+9MBypCyGYDogUXfMwfbRy6lyQO/BjJ 0fVD5FupdtF+4v2D94XTIVVY4U56Eevhvw95bt8zJKgzP0T2yuIlOTXnb1ropejVb7kw +KTJL7L0v/tp9feDIe+pjmpH+498N6ZrjC87QyW25oSpWyAowfYVyV/dGO3zMAm9j3Lq 1rA2vsergxD2tWEOaPnXJWlAHYBgZAODAZ5RotGbdaPoSYVu0Y1ADBRgoq+wbVCzIhAb m0ABI/d2MQldlVSdfpvJby0Bk0eOae5lJxt72iQPR8oZm7KVuJEUbHCCj6JG5WJHQUwl oNIg== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of frederic.blanqui@inria.fr designates 192.134.164.104 as permitted sender) smtp.mailfrom=frederic.blanqui@inria.fr DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20210112; h=sender:to:from:subject:message-id:date:user-agent:mime-version :content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-subscribe:list-unsubscribe; bh=q3VveHHoQKbJ3Zd0085sLT4fQHNAUquAuuV+vn90ZsM=; b=EvCzsRzil3uDjEbrPScit5WBaJbY52cxqCDEwts/ITbwefk+QmYPONXNbGMPlUd/FE PUDUFaLipbe2r93aTZUfFdqfZseIkgpndHxeV1kDHYxo0c0Akwt4yAIg6Sy0Y7NXvtqY PsALP8CPR3hE85IFEOvX8EVtxGaFcSGcj/D8XEiptjqFvN8hw3M2F6yU+Ac/gBRO2wu1 pdmXiTbtpgzZYCkps9S+zh0u+KXS0oPREpGmhfnEsjpTnfRPRiBS/ZXYvnnM3233gWqc mYJjtqxN9L/fHWz5DESImbbMkO9iYPcNRcET4hWd8AfbOQeuYFU0Jm8PHFkWERTHOkQw WXFw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=sender:x-gm-message-state:to:from:subject:message-id:date :user-agent:mime-version:content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-subscribe:list-unsubscribe; bh=q3VveHHoQKbJ3Zd0085sLT4fQHNAUquAuuV+vn90ZsM=; b=oFVgTtgRMNP6wc7/g/YSq+DKGM1aUUVr5baWDigd6k3CIa58j50dv1dcHTyguQjWt7 5oQk5bpdtLlLJS9EdbqdIcLf1VNA1xKL1Tn3sJyv1tDLcQ8mnzcgEJMMS0j87SJ6TvjG Qo0IpwxbiefVFN2acVjeY/XETKK24hN1MRbZDvmPe4bmgUMHzMpyNd6WkBiB1axgD0WR 6ZVO1sm9QXT9SNU9WhHOZXOiHoMCWMDzkWp1rRtFlEu/B7xIPOLQ1zgZJ3+l8RuUbWmn jf9lZnKXr6+wm5Zw6BIjiecu3xKMhXdMWOfrEOUV6V1sA8tu7KHEwBGHEMztOBkxkSjH QM5g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOAM533STaASrkduJvIdhMMOkbcqq2Y0sWJOgJS7jdSSi1nCDWUyy0Eg C+4HowVM+O0KbkCNbawAomk= X-Google-Smtp-Source: ABdhPJx+GVzOO/4JQfIBvoOi4gXcVhzWmNnect8MwLk15hPFWFxiEo6D/FVUJanfCUj95EYZwVsLQA== X-Received: by 2002:a05:600c:4111:: with SMTP id j17mr7579727wmi.7.1642666600291; Thu, 20 Jan 2022 00:16:40 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:600c:4f04:: with SMTP id l4ls1843951wmq.1.canary-gmail; Thu, 20 Jan 2022 00:16:38 -0800 (PST) X-Received: by 2002:a7b:c40c:: with SMTP id k12mr7774476wmi.185.1642666598735; Thu, 20 Jan 2022 00:16:38 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1642666598; cv=none; d=google.com; s=arc-20160816; b=reGmrkYu0HfvhAIkKxo+2ZvulW6wYoi8atswixOYgJWCcy2/RPiX9cCSFXIVWjxKnl 4Qb6YuTI/xzsxZmkrcviyD+vFD0+o8jrJfEmelEJZ5G0/5yW1P3Pl6VJWARGVT5imzCq zpIlyvlRPnL0RWsxMaUXH0gr+8XckrAOZ68tfOSgyWn3fJFbctSSZOqS6D5YMSssweM4 OpStvRIXrBG2ObtN5lZSWsYqIwJJD5kMT0lZz8hf208e2csgZPqmXd9pRxhHqOC0SYuS UdWaZKmHO+JBsg/SIFp5wYMQNqCIfuCPf89CrExsw7aoHkFUABDzKzByLo1sDDFjpKSm l1Lw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:mime-version:user-agent:date:message-id:subject :from:to; bh=U/BRkINogB/hkGVjVfb+uDULrCe2Icz49TJ2vMbp9wQ=; b=mo5HAX0YugtG3LjUzy+4UyotX9tVIf4Hg54zRU+Pcp8SBatSA6MgjCXgDgrMwbDXk5 +x0r/VbA5zQLcb/AJKol/MPPOU9NDzbDPCKIIAh/aGI9CNQPjwgRgQCJB3QyTPiozBcG kSckf2Q23UwxlIiHDxpc/f+mqU9WTGIP6tqPG/UPJPlG6djC/YJzIOzL1h6VlZ7lt7qu 7HDwV/NxxrxMP1biZZpuPKUgmrQHUP2X+B6HYsTyp8R+Uefyt5spCPELcLjx641nxSe7 BEU1wJPwU4ctGlwwZT1VLdllPcBxrNA6fiZIb2L9VGjz7CSyD1HbFBykr79mIqPjdac0 493g== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of frederic.blanqui@inria.fr designates 192.134.164.104 as permitted sender) smtp.mailfrom=frederic.blanqui@inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr. [192.134.164.104]) by gmr-mx.google.com with ESMTPS id m25si81312wmg.1.2022.01.20.00.16.38 for (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Thu, 20 Jan 2022 00:16:38 -0800 (PST) Received-SPF: pass (google.com: domain of frederic.blanqui@inria.fr designates 192.134.164.104 as permitted sender) client-ip=192.134.164.104; X-IronPort-AV: E=Sophos;i="5.88,301,1635199200"; d="scan'208,217";a="3565717" Received: from lfbn-idf2-1-886-98.w86-247.abo.wanadoo.fr (HELO [192.168.1.19]) ([86.247.9.98]) by mail3-relais-sop.national.inria.fr with ESMTP/TLS/ECDHE-RSA-AES256-GCM-SHA384; 20 Jan 2022 09:16:38 +0100 To: "homotopytypetheory@googlegroups.com" From: =?UTF-8?B?RnLDqWTDqXJpYyBCbGFucXVp?= Subject: [HoTT] Release of Lambdapi 2.1.0 Message-ID: <325320a5-6e41-4c42-5d29-a9971b04eca0@inria.fr> Date: Thu, 20 Jan 2022 09:16:37 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.14.0 MIME-Version: 1.0 Content-Type: multipart/alternative; boundary="------------FB521E360269165214D6DAD4" Content-Language: en-US X-Original-Sender: frederic.blanqui@inria.fr X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of frederic.blanqui@inria.fr designates 192.134.164.104 as permitted sender) smtp.mailfrom=frederic.blanqui@inria.fr Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , List-Unsubscribe: , This is a multi-part message in MIME format. --------------FB521E360269165214D6DAD4 Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Transfer-Encoding: quoted-printable Dear all, I am pleased to announce the release 2.1.0 of Lambdapi on opam. See https://github.com/Deducteam/lambdapi for more details and https://lambdapi.readthedocs.io/ for its user manual. Lambdapi is a proof assistant for the =CE=BB=CE=A0-calculus modulo rewritin= g. Lambdapi provides a rich type system with dependent types. In Lambdapi, one can define both type and function symbols by using rewriting rules (oriented equations). The declaration of symbols and rewriting rules is separated so that one can easily define inductive-recursive types for instance. Rewrite rules can be exported to the TRS and XTC formats for checking confluence and termination with external tools. A symbol can be declared associative and commutative. Lambdapi supports unicode symbols and infix operators. Lambdapi does not come with a pre-defined logic. It is a powerful logical framework in which one can easily define its own logic and build and check proofs in this logic. There exist .lp files defining first or higher-order logic and complex type systems like in Coq or Agda. Lambdapi provides a basic module and package system, interactive modes for proving both unification goals and typing goals, and tactics for solving them step by step. In particular, a rewrite tactic like in SSReflect, and a why3 tactic for calling external automated provers through the Why3 platform. Lambdapi is mostly compatible with Dedukti: it can read .dk files and convert .lp files to .dk files. Dedukti is just a type checker and has no features such as implicit arguments, etc. Hence, Lambdapi can be used as a higher-level intermediate language to translate proofs from a given proof system to Dedukti. Best regards, Fr=C3=A9d=C3=A9ric. --=20 You received this message because you are subscribed to the Google Groups "= Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/325320a5-6e41-4c42-5d29-a9971b04eca0%40inria.fr. --------------FB521E360269165214D6DAD4 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

Dear all,

I am pleased to announce the release 2.1.0 of Lambdapi on opam.

See https://github.com/D= educteam/lambdapi for more details
and https://lambdapi.readthed= ocs.io/ for its user manual.

Lambdapi is a proof assistant for the =CE=BB=CE=A0-calculus modulo rewriting.

Lambdapi provides a rich type system with dependent types.
In Lambdapi, one can define both type and function symbols
by using rewriting rules (oriented equations). The declaration
of symbols and rewriting rules is separated so that one can
easily define inductive-recursive types for instance.
Rewrite rules can be exported to the TRS and XTC formats
for checking confluence and termination with external tools.
A symbol can be declared associative and commutative.
Lambdapi supports unicode symbols and infix operators.

Lambdapi does not come with a pre-defined logic. It is a
powerful logical framework in which one can easily define
its own logic and build and check proofs in this logic.
There exist .lp files defining first or higher-order logic
and complex type systems like in Coq or Agda.

Lambdapi provides a basic module and package system,
interactive modes for proving both unification goals
and typing goals, and tactics for solving them step by step.
In particular, a rewrite tactic like in SSReflect, and
a why3 tactic for calling external automated provers through
the Why3 platform.

Lambdapi is mostly compatible with Dedukti: it can read .dk files
and convert .lp files to .dk files. Dedukti is just a type checker
and has no features such as implicit arguments, etc. Hence,
Lambdapi can be used as a higher-level intermediate language
to translate proofs from a given proof system to Dedukti.

Best regards,

Fr=C3=A9d=C3=A9ric.


--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgi= d/HomotopyTypeTheory/325320a5-6e41-4c42-5d29-a9971b04eca0%40inria.fr. --------------FB521E360269165214D6DAD4--