From: Andrej Bauer <andrej.bauer@andrej.com>
To: "HomotopyTypeTheory@googlegroups.com"
<homotopytypetheory@googlegroups.com>
Subject: [HoTT] Every proof assistant seminar series: Cubical Agda (September 17, 2022)
Date: Fri, 11 Sep 2020 08:32:48 +0200 [thread overview]
Message-ID: <CAB0nkh1qFFEtkb90aj7RBy+f407nJRwjLdWcu8BvMC1N6Z3c7A@mail.gmail.com> (raw)
It is my pleasure to announce the next talk in the Every proof
assistant on-line seminar series. We are starting the Fall season with
Anders Mörtberg who will talk about Cubical Agda.
With kind regards,
Andrej
CUBICAL AGDA: A DEPENDENTLY TYPED PROGRAMMING LANGUAGE WITH UNIVALENCE
AND HIGHER INDUCTIVE TYPES
Anders Mörtberg
Stockholm University
Thursday, September 17, 2020
15:00 to 16:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985, https://zoom.us/j/98904788985
Proof assistant: Cubical Agda, https://github.com/agda/cubical
Abstract: The dependently typed programming language Agda has recently
been extended with a cubical mode which provides extensionality
principles for reasoning about equality, such as function and
propositional extensionality. These principles are typically added
axiomatically to proof assistants based on dependent type theory which
disrupts the constructive properties of these systems. Cubical type
theory provides a solution by giving computational meaning to Homotopy
Type Theory and Univalent Foundations, in particular to the univalence
axiom and higher inductive types. In the talk I will discuss how Agda
was extended to a full-blown proof assistant with native support for
univalence and a general schema of higher inductive types. I will also
show a variety of examples of how to use Cubical Agda in practice to
reason about mathematics and computer science.
--
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/CAB0nkh1qFFEtkb90aj7RBy%2Bf407nJRwjLdWcu8BvMC1N6Z3c7A%40mail.gmail.com.
reply other threads:[~2020-09-11 6:33 UTC|newest]
Thread overview: [no followups] expand[flat|nested] mbox.gz Atom feed
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=CAB0nkh1qFFEtkb90aj7RBy+f407nJRwjLdWcu8BvMC1N6Z3c7A@mail.gmail.com \
--to=andrej.bauer@andrej.com \
--cc=homotopytypetheory@googlegroups.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).