* [HoTT] Every proof assistant seminar series: Cubical Agda (September 17, 2022)
@ 2020-09-11 6:32 Andrej Bauer
0 siblings, 0 replies; only message in thread
From: Andrej Bauer @ 2020-09-11 6:32 UTC (permalink / 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,
CUBICAL AGDA: A DEPENDENTLY TYPED PROGRAMMING LANGUAGE WITH UNIVALENCE
AND HIGHER INDUCTIVE TYPES
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 HomotopyTypeTheoryemail@example.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAB0nkh1qFFEtkb90aj7RBy%2Bf407nJRwjLdWcu8BvMC1N6Z3c7A%40mail.gmail.com.
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2020-09-11 6:33 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2020-09-11 6:32 [HoTT] Every proof assistant seminar series: Cubical Agda (September 17, 2022) Andrej Bauer
Discussion of Homotopy Type Theory and Univalent Foundations
This inbox may be cloned and mirrored by anyone:
git clone --mirror http://inbox.vuxu.org/hott
# If you have public-inbox 1.1+ installed, you may
# initialize and index your mirror using the following commands:
public-inbox-init -V1 hott hott/ http://inbox.vuxu.org/hott \
Example config snippet for mirrors.
Newsgroup available over NNTP:
AGPL code for this site: git clone https://public-inbox.org/public-inbox.git