From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, FROM_EXCESS_BASE64,HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-oi1-x23a.google.com (mail-oi1-x23a.google.com [IPv6:2607:f8b0:4864:20::23a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 910cf3f0 for ; Tue, 6 Aug 2019 22:16:17 +0000 (UTC) Received: by mail-oi1-x23a.google.com with SMTP id t198sf36240393oih.20 for ; Tue, 06 Aug 2019 15:16:16 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=DxaWVvfZVJ4VbWY5PQK2AsbxvnwfvdGQHALfQnZfScE=; b=F0X3L7tDNAkDQI8w79OJcETJ6LCsPMiBQMaicGGkYyMsZVhLu2bhmuyqRVIPoxysZg xVdw0c/eLDSnUnbn/tivH75kKjpKmWef4AKr0folq88Oc/fpgfVseJdQQjpIc+twH69M Dijtg/qB/QnQHU9TuInTwEJb834NocK7KVJ3IzJp5f52I5TPxzHAMoaIGrRIZd6djyht iCIgWmT0MxZq6zyg+xIZtkBHKAaiUz4rq8TdSeCA7D+a9jet+iM1clXHtnNVcgl1KX/o bkEGhrFETG7B8gdsV9cZZCnKbnrgytoj0vACqENZdLNScseYbH3uWyN76vyMeaTCJPf9 ayHQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:subject:mime-version:x-original-sender :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=DxaWVvfZVJ4VbWY5PQK2AsbxvnwfvdGQHALfQnZfScE=; b=jVhYg2cbe9Yu2va2pDadTfiE8FwtTnUDeS/EvILP9IOsWFg4jY5ch5fSYADwxPiSX1 HVU2nvJPBhFkSAVeXFij+KHqIwxmDHmtMF+wxzPcB0b1nCup5yPBUXYDlcrjfQs/eRo3 /teRshvdWUEw3EDtHtiPDDzHpnQoxN3c4J05NQ+3JlTc07H6DXpBr6Ak1Dlq+8At+lrG oobmSrUtZ7dB1h2CkCexh7tJzfSaYYzPvDVMEbdx92ENSlubRrLPN6/v4fVudbsb1Usa D2kOfVwuzgTxNR9hDd+MrO0lYQRtztIpY7BF7PY/w/QhN9GS8J6172bsvVm5riEVEXJL wOQg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=DxaWVvfZVJ4VbWY5PQK2AsbxvnwfvdGQHALfQnZfScE=; b=eA7XiAKs1DhlVp4aNEItcn0K02zg42cr9L/Z9Cyth+KgpJyNMuw9yDsLWR7KNMe0RI AR+nJn2gdYPlNKB/QbP2WILiwfQI6/Wbv6+5y2LvqdHYU5AAiPRQTkFhSAEe3E5Yk9hG FW3AoI03/1tGD+46Zcu+IqWWjXzAExCa5FZRo+dDjY/63HjQh4qb9AXs96j/iSvCdQ5N dk8q9/eZDFdfRr78Y8fqSmEe/SwR9w2sBFatgD8dy0XQeMC8WloIpvj6KEruSP7xlwlc Zxoa+U2oOIQv2PfxSu9YPOox64Ab3gYrfuvRDXptCKww0KHSZm6rSOBN6rpUQDL/Mx/7 O+7g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWWiNTP1a2uBkKV5w1j4sIgWuZhDeT3ml4z/TfmNG+mVjlaWp1t EEM/vy3RQXGanhjX3R71v74= X-Google-Smtp-Source: APXvYqzJ+bkvdldp82cqqbgMLf11RyBlaI78h5Csq6Tevcy4u+BybyyrFaeJz/XgjPnNHMmYEF2uyg== X-Received: by 2002:a9d:6385:: with SMTP id w5mr1989726otk.227.1565129774101; Tue, 06 Aug 2019 15:16:14 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:2489:: with SMTP id z9ls1415594ota.9.gmail; Tue, 06 Aug 2019 15:16:13 -0700 (PDT) X-Received: by 2002:a05:6830:1294:: with SMTP id z20mr5554660otp.0.1565129773487; Tue, 06 Aug 2019 15:16:13 -0700 (PDT) Date: Tue, 6 Aug 2019 15:16:12 -0700 (PDT) From: =?UTF-8?B?0JLQsNC70LXRgNC40Lkg0JjRgdCw0LXQsg==?= To: Homotopy Type Theory Message-Id: <9d23061c-4b7a-4d69-9c22-f28261ad3b33@googlegroups.com> Subject: [HoTT] New theorem prover Arend is released MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2479_1682895400.1565129772906" X-Original-Sender: valery.isaev@gmail.com 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: , ------=_Part_2479_1682895400.1565129772906 Content-Type: multipart/alternative; boundary="----=_Part_2480_1959666824.1565129772907" ------=_Part_2480_1959666824.1565129772907 Content-Type: text/plain; charset="UTF-8" Arend is a new theorem prover that have been developed at JetBrains for quite some time. We are proud to announce that the first version of the language was released! To learn more about Arend, visit our site . Arend is based on a version of homotopy type theory that includes some of the cubical features. In particular, it has native higher inductive types, including higher inductive-inductive types. It also has other features which are necessary for a theorem prover such as universe polymorphism and class system. We believe that a theorem prover should be convenient to use. That is why we also developed a plugin for IntelliJ IDEA that turns it into a full-fledged IDE for the Arend language. It implements many standard features such as syntax highlighting, completion, auto import, and auto formatting. It also has some language-specific features such as incremental typechecking and various refactoring tools. To learn more about Arend, you can check out the documentation . You can also learn a lot from studying the standard library . It implements some basic algebra, including localization of rings, and homotopy theory, including joins, modalities, and localization of types. Frequently asked questions (that nobody asked): - Why do we need another theorem prover? We believe that a theorem prover should be convenient to use. This means that it should have an IDE comparable to that of mainstream programming languages. That is why we implemented IntelliJ Arend . This also means that the underlying theory should be powerful and expressive. That is why Arend is based on homotopy type theory and has features such as an impredicative type of propositions and a powerful class system. - Does Arend have tactics? Not yet, but we are working on it. - Does Arend have the canonicity property, i.e. does it evaluate closed expressions to their canonical forms? No, but it computes more terms than ordinary homotopy type theory, which makes it more convenient in many aspects. If you want to know about language updates, you can follow us on twitter . Questions, suggestions, and comments are welcome at google groups . -- 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 email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/9d23061c-4b7a-4d69-9c22-f28261ad3b33%40googlegroups.com. ------=_Part_2480_1959666824.1565129772907 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Arend is a new theorem prover that have been developed at= =C2=A0JetBrains=C2=A0for quite s= ome time. We are proud to announce that the first version of the language w= as released! To learn more about Arend, visit our=C2=A0site.

Arend is based on a vers= ion of homotopy type theory that includes some of the cubical features. In = particular, it has native higher inductive types, including higher inductiv= e-inductive types. It also has other features which are necessary for a the= orem prover such as universe polymorphism and class system. We believe that= a theorem prover should be convenient to use. That is why we also develope= d a plugin for=C2=A0IntelliJ ID= EA=C2=A0that turns it into a full-fledged IDE for the Arend language. I= t implements many standard features such as syntax highlighting, completion= , auto import, and auto formatting. It also has some language-specific feat= ures such as incremental typechecking and various refactoring tools.
<= div>
To learn more about Arend, you can check out the=C2=A0documentation. You= can also learn a lot from studying the=C2=A0standard library. It implements some basic algebra= , including localization of rings, and homotopy theory, including joins, mo= dalities, and localization of types.

Frequently as= ked questions (that nobody asked):
  • Why do we need another= theorem prover? We believe that a theorem prover should be convenient to u= se. This means that it should have an IDE comparable to that of mainstream = programming languages. That is why we implemented=C2=A0IntelliJ Arend. This also = means that the underlying theory should be powerful and expressive. That is= why Arend is based on homotopy type theory and has features such as an imp= redicative type of propositions and a powerful class system.
  • Does A= rend have tactics? Not yet, but we are working on it.
  • Does Arend ha= ve the canonicity property, i.e. does it evaluate closed expressions to the= ir canonical forms? No, but it computes more terms than ordinary homotopy t= ype theory, which makes it more convenient in many aspects.
I= f you want to know about language updates, you can follow us on=C2=A0twitter. Questions, suggestions, an= d comments are welcome at=C2=A0google groups.

--
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.co= m/d/msgid/HomotopyTypeTheory/9d23061c-4b7a-4d69-9c22-f28261ad3b33%40googleg= roups.com.
------=_Part_2480_1959666824.1565129772907-- ------=_Part_2479_1682895400.1565129772906--