From: Reiko Heckel <reiko.heckel@gmail.com>
To: "gratra@upb.de" <gratra@upb.de>, "categories@mta.ca" <categories@mta.ca>
Subject: FW: Invitation: GReTA-ExACT online workgroup, Friday December 10, 2021, 15:00 CET
Date: Mon, 6 Dec 2021 10:54:57 +0000 [thread overview]
Message-ID: <E1mumwG-00065m-Sd@rr.mta.ca> (raw)
FYI, Reiko
On 06/12/2021, 08:37, "GReTA Seminar organisers" <greta@irif.fr> wrote:
Dear colleagues,
It is our great pleasure to invite you to the next session of the “GReTA-ExACT - Executable Applied Category Theory” online workgroup:
Friday December 10, 15:00 CET
"Formalizing Category Theory using Type Theory: A Discussion", E.J. Gallego Arias
(abstract, Zoom and YouTube links attached below)
In the context of the GReTA - "Graph TRansformation Theory and Applications" online seminar series hosted at IRIF (https://www.irif.fr/~greta/), the GReTA ExACT (Executable Applied Category Theory) online workgroup aims at providing an interdisciplinary forum for exploring the diverse aspects of applied category theory relevant in graph transformation systems and their generalizations, in developing a methodology for formalizing diagrammatic proofs as relevant in rewriting theories via proof assistants such as Coq, and in establishing a community-driven wiki system and repository for mathematical knowledge in our research field (akin to a domain-specific Coq-enabled variant of the nLab). A further research question will consist in exploring the possibility for deriving reference prototype implementations of concrete rewriting systems (e.g., over multi- or simple directed graphs) directly from the category-theoretical semantics, in the spirit of the translation-based approaches (utilizing theorem provers such as Microsoft Z3). Please refer to https://www.irif.fr/~greta/gretaexact/ for further details (including information on how to register for participating in the Zoom meetings).
With best regards,
Nicolas Behr, Andrea Corradini, Jean Krivine and Reiko Heckel
(GReTA organisers)
___________________________________________________
Date and time: Friday December 10, 2021, 15:00 CET
Title: Formalizing Category Theory using Type Theory: A Discussion
Speaker:
Emilio Jesús Gallego Arias (Université de Paris, CNRS, IRIF, France)
Abstract:
Since its inception at the start of the 20th century, type theory has become a core foundational tool for those interested in the logical foundations of mathematics and computer science.
A key milestone on the field is the Calculus of Inductive Constructions, the type theory that lies at the heart of modern interactive proof assistants such as Coq or Lean. The CiC is remarkably expressive, yet remains computationally tractable, leading to important milestones in computer-checked mathematical results such as the 4 color theorem or the Feit-Thompson theorem.
In this talk, we will present the calculus of inductive constructions as currently implemented in the Coq proof assistant, and we will explore the encoding of basic constructions of category theory in Coq, placing a particular emphasis the usability and modularity of our definitions.
Zoom registration link:
https://u-paris.zoom.us/meeting/register/tZwrdO2hrDssHtEB5TYi6tZPmm2hn1QCrspV
Link to YouTube live stream:
https://youtu.be/lM0b3oHDunU
___________________________________________________
----------------------------------------------------------------------------
GReTA - Graph TRansformation Theory and Applications
International Online Seminar Series
----------------------------------------------------------------------------
Contact: greta@irif.fr
Webpage: www.irif.fr/~greta<http://www.irif.fr/~greta>
YouTube: https://www.youtube.com/channel/UC6j-G6oPmkqCgOx6UQOUhSQ
Twitter: https://twitter.com/GReTAseminars
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
reply other threads:[~2021-12-06 10:54 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=E1mumwG-00065m-Sd@rr.mta.ca \
--to=reiko.heckel@gmail.com \
--cc=categories@mta.ca \
--cc=gratra@upb.de \
/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).