Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
* [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)
  To: HomotopyTypeTheory@googlegroups.com

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.

^ 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 \
		homotopytypetheory@googlegroups.com
	public-inbox-index hott

Example config snippet for mirrors.
Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.hott


AGPL code for this site: git clone https://public-inbox.org/public-inbox.git