Every proof assistant: Arend
source link: http://math.andrej.com/2020/04/28/every-theorem-prover/
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
Every proof assistant: Arend
For a while now I have been contemplating a series of seminars titled "Every proof assistant" that would be devoted to all the different proof assistants out there. Apart from the established ones (Isabelle/HOL, Coq, Agda, Lean), there are other interesting experimental proof assistants, and some that are still under development, or just proofs of concept. I would like to know more about them, and I suspect I am not the only one.
Getting the authors of proof assistants to travel to Ljubljana and giving talks at our Foundations of mathematics and theoretical computer science seminar has largely become impossible. But luckily research seminars world-wide are rapidly moving online, and so is our Foundations seminar. I am therefore delighted to announce the first "Every proof assistant" seminar:
Arend proof assistant
Time: Thursday, April 30, 2020 from 18:00 to 19:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 965 4439 5816
Speaker: Valery Isaev (JetBrains research) Proof assistant: Arend proof assistantAbstract: I will discuss Arend, a proof assistant developed at JetBrains Research. The aim of Arend is to provide a powerful system for formalization results in homotopy type theory and in ordinary mathematics. To achieve the latter goal, we prove a flexible class system with subtyping, universe polymorphism with a powerful level inference mechanism, quotient sets with a convenient pattern matching principles for them. We also recently implemented a tactic framework which can be used to automate routine proofs and implement various EDSLs. Homotopic features of Arend include built-in universes of finite homotopy level, higher inductive types, univalence, and path types in the style of cubical type theories. I will talk about these features and also about our plans to implement language extensions that can be used to simplify reasoning about various higher structures.
Video recording of the talk is available.
I have a couple more in the pipeline, so follow this blog, the Foundations seminar announcements or my Twitter account @andrejbauer.
Comments
Will PVS and ACL2 be covered. Both are in the Boyer-Moore family. ACL2 has a significant user based in hardware verification. PVS is used in the CPS community.
I am not sure what we will cover. We will start with proof assistants that are closer to the type-theoretic community, just because I know the scenery there better.
PVS and ACL2 definitely belong to the "established" group, together with Coq, Agda, Lean, Isabelle etc. We will get to those eventually.
LaTTe is similar to Coq, and written in Clojure (https://github.com/latte-central/LaTTe)
Z3 can also be used to prove theorems.
How about https://cedille.github.io/?
Dear Andrej,
Will these talked be recorded and put out somewhere? They look extremely interesting and it would be a same to miss them.
This is a great idea. Will there be a recording of the talk?
Will these seminars be recorded? I sadly have a test at the listed time!
My proof editor (DC Proof) is a very simple system based on my own versions of natural deduction and set theory which you may find interesting in themselves. DC Proof was designed to introduce math undergrads to the basic methods of proof.
I am an amateur software developer. I am not associated with any academic institution and have no postgraduate degrees.
I messed up the time zones and missed the first talk. Any chance a recording will be available? Looking forward to the series!
The seminars will be recorded and the videos will be published online. See the link above for the first video. I will also provide links to the proof assistants.
If you would like to suggest a proof assistant, please contact me by e-mail. I took note of the suggestions in the comments.
Post a comment:
$⋯$ for inline and $$⋯$$ for display LaTeX formulas,
and <pre>⋯</pre> for display code. Your E-mail address is only used to compute
your Gravatar and is not stored anywhere.
Comments are moderated through pull requests.
Name
Website
Comment
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK