From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.4 Received: from mail-il1-x140.google.com (mail-il1-x140.google.com [IPv6:2607:f8b0:4864:20::140]) by inbox.vuxu.org (Postfix) with ESMTP id CC23821471 for ; Thu, 18 Apr 2024 16:02:16 +0200 (CEST) Received: by mail-il1-x140.google.com with SMTP id e9e14a558f8ab-36b34b3a5fdsf11386075ab.0 for ; Thu, 18 Apr 2024 07:02:16 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1713448934; cv=pass; d=google.com; s=arc-20160816; b=Dq4KCD+O5bDhNb7ErXpHKSev9C7v2mpIFr2UGIeBuAPrpyZkmuNUqGkIhlcT+lZKJJ sHNhTyLyLtk3zlYpbjUN1q7Ayf1MFfcSPuShFC04+RJym/jQWSV6+LYLeAjwhLKe3hfL QvZ/IE1+Xl+QzXT0/vGhR3oZ0VEe81wgTG0sRgYruMSxLGhw5flb0ot6prnNw2MLifvh oWMQAUfUZ5cEqnK2FQ7vKC89HmirEhhCXdMoI2I+RztV82PaoU8HTMdu89Z3ki/zem4g ynr8T6QXSJH171ZQhiKS8Y1Sf6bXkf/i2uTN3N9HkWg8AUuVsRLK42OnK0ustkNt6HFg TSPg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:to:subject:message-id:date:from :mime-version:sender:dkim-signature:dkim-signature; bh=/krIlRrJBBX1VSsdZigUoj539mM0S6DWaEJ8pb/Op5I=; fh=mjVGZ7IO76MU1Lb0b3BjUBKhp3BujA1RLZuCHGD0TR0=; b=ty0NlWBm85lP3Cbbt85kVxoyuKDIFwFgqgZ/YZvS4Ze1HKA7LCt1iDwcis4JIjjhf2 NdmyUTbu3EjuT0D0Xqbw4BSjItBtJFQIQ7kYLCkbatc3CmpuitjJL6ExS7uuq0mU6DTJ WNGFQ33n2Wo3iufJOfydt53LSF4bRohsZbIV7DQRO/Dw9rVpG37pGP8cXWru8BKOjcRi 4zZz8BcmtFrwWeBu5otOmbY1KtqYncd0MfdCW1r7P0nE3CKB8v/ROfGjn90PRXEI61SU dIMp8TaC9H8ze3UrCoGta5JjrwjzKmCnsUS9ci4K0OBTliw4FK1FrH43KqGWoK0ejlAe KF7w==; darn=inbox.vuxu.org ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=I5FKGP84; spf=pass (google.com: domain of rmogelberg@gmail.com designates 2607:f8b0:4864:20::b2f as permitted sender) smtp.mailfrom=rmogelberg@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20230601; t=1713448934; x=1714053734; darn=inbox.vuxu.org; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:x-original-authentication-results :x-original-sender:to:subject:message-id:date:from:mime-version :sender:from:to:cc:subject:date:message-id:reply-to; bh=/krIlRrJBBX1VSsdZigUoj539mM0S6DWaEJ8pb/Op5I=; b=GRrXmW+85V+Y3cqiQHyQSirB8G5QG7hk0sh2ZuLpp7GaFv/p+i8jUpSkspRv6/z3m+ D+izaTQRk4rZwtxCjXZXrjZwdlaT6Eo59iG0VVjVcCjt01ScoYloLe+NX50ZFJmIF0AP 1+zZ+HiR0ktmublYOP1AV2sD4YOzDNMD750c8SMDX8EwMHtXnlRuSzo+Wa+2uyNIpZVA +DhOP/YkOzuAPfj6VubtSzTpar7G4TmGncTDgLLllbOkNtdEHrNf6EOI+ZIlQqbcIeGc VkUsSsqVL2uWuBIqowrCYqonYcaf159O3kbvsRTP8n7OdHQ/ol3s42Kp4N4fKlfIC1U5 2Ypw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1713448934; x=1714053734; darn=inbox.vuxu.org; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:x-original-authentication-results :x-original-sender:to:subject:message-id:date:from:mime-version:from :to:cc:subject:date:message-id:reply-to; bh=/krIlRrJBBX1VSsdZigUoj539mM0S6DWaEJ8pb/Op5I=; b=B36yyQvFU9arzOIaPBK2dMwqhq+kJvEbkjuyLxtdhnFBHe0OIhUFD/FlAu0nzzYNa3 mgueSZ59kuBruHdIyElICbAgB9at7nhtIj6y5WEPGAvlC/FlGai3MbOKLoPzSd9dxYQH tz1SYxiZFXA6q5bwdDCU8pffOSCg6sj083fWTnp5CKXu+atTKeUSGKaSHs2kBIG78VEJ SIyVV+H1tcflc0LNa00NItRIsK6wtZL3sXlXcu3oZcs3x2VWEz7wgnuf6Eg2ck+fzTHq m+7tfyy+zBkaHjT9yLwzkUp5Pv51YLr+/fC+08tuDS/LbdJK7Fn0IWhFRUQZQ517b3GO Zymw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1713448934; x=1714053734; h=list-unsubscribe:list-archive:list-help:list-post :x-spam-checked-in-group:list-id:mailing-list:precedence :x-original-authentication-results:x-original-sender:to:subject :message-id:date:from:mime-version:x-beenthere:x-gm-message-state :sender:from:to:cc:subject:date:message-id:reply-to; bh=/krIlRrJBBX1VSsdZigUoj539mM0S6DWaEJ8pb/Op5I=; b=mrFwKmZT4mr7cjTBDnA7XJeJ8SdAKFbjjXLBqqS4TjpQBkf39BcoA/1mnTFZbX6ynV hGEvSRlg33/FjNWmqNm+UgNwNbGqLnIsoPbFOXyH/7Vkonqyz+viPfWrS9A96KPkwuH9 BAxynPnZ3HINXwIheMv2rFM4QQSDwh2rloofu7OW+Et6/yvnqZXSlFgeoC183VU7g1F7 0lVJ/ftQBhqs84MiHAHm7CmaDB1qWvGWTDv3kpzcIXkj6MCQmVzVGD4dKMHLserPqcsd JNNcgU3n/BFiZc+KuNSrU22SzZMTjrsr2g3bR28Up9jBJl/PRchcfOyWVQ5CVq5cc/b0 GRhA== Sender: homotopytypetheory@googlegroups.com X-Forwarded-Encrypted: i=2; AJvYcCU/DFJVv/iUDNQF4oJYQpU2c6dZ4LXYzDsJ/Oo53R3ujfjBtXcAJxq3cIMxwSJnyj9LAWxoYs4s3leYYYKPNa48lQ== X-Gm-Message-State: AOJu0YxOrS+DBanzw4UEY5FiucvIU/pevbEbtnvpTaLEA9NZL6WpBiQE Ax7cFXdfAF0/pbWQS9+aTZntERaDJPE79c6cZYPREvSaoBT9ItsF X-Google-Smtp-Source: AGHT+IGvLh99GrC9MosemfLT1XvuJLYwP4YHzJh5TEHAbcocvlEEnMNPu9R5Oq5skXH+IwETzhj9GA== X-Received: by 2002:a92:6f01:0:b0:36b:fa6e:5be1 with SMTP id k1-20020a926f01000000b0036bfa6e5be1mr630319ilc.20.1713448934589; Thu, 18 Apr 2024 07:02:14 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a92:7f0d:0:b0:36b:80c:135a with SMTP id a13-20020a927f0d000000b0036b080c135als94814ild.2.-pod-prod-03-us; Thu, 18 Apr 2024 07:02:12 -0700 (PDT) X-Received: by 2002:a05:6e02:1788:b0:36a:a6c4:b6da with SMTP id y8-20020a056e02178800b0036aa6c4b6damr3716933ilu.4.1713448931699; Thu, 18 Apr 2024 07:02:11 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1713448931; cv=none; d=google.com; s=arc-20160816; b=PR3r9T1TMzDml2p0kQr9HVHp0dZ8db3pPxVkSWNCgQXCmuvnUUucNwTVdxdnHCddHM QoryAWHW3faNoOar24JUDpty+nzWjyYAOQgDDjML2fidOGxpF6x9DoqOdfWTxwlH/9J+ ODImrbJnwCVmpKW5PffQRv9S8CzGRE8iIVLyh5RPtx/K1AvedoLxwOqXwd2aJkKZ0g0+ s7eKMXwDVhQJ5caG7gwA8T1ZHjBQfO7phrfE2BSCi/ol9yXBTOoFGmwZFyF8CUEqCQdx IdcORxSJSNr8hMfkPDe3V4+wexvqytsotUWfGWJvnfST2/PtvVmCqQaQxTaiwFPfS9fH kpOQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=+C/5A5PW9DJ3ID/OB5MiqnMrVxTmpTVp2G9LRDeDW88=; fh=3sIP6N/TEjoc1Uq37Y498r2kAtX4ApZak0DpOSnwMFI=; b=EN8wpoqDjn1UqjvUOgLq7vmPQDNdzhEQ02Yh1C27kIGqcjQtTzi3WDT97oeccw5xb1 qGdesB+41YCUddzAgvqK/rxn/McSsIW6xPdq4KNpH4NU7Csz3JHUctX02wNbAZC/pW4i lCx98Bn5vH6uRI4t2DjfAJVxOoMphw1r0c1XLbRJ2m2vzwSsZgKxi8+il1Ag5inYCklU QyRbch0hR58PpV5Lp9eV6gHtVsXZoqqvthj4ExCWHyK84pQ863gTiW6iKi3kpq9UuB2r VIy6QrqPFLGAnuf5/rUYkWAFG8++yyzXBuFzriRvLmGbPjSsPI3eH6pvhEMUKtf9y88M QcvA==; dara=google.com ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=I5FKGP84; spf=pass (google.com: domain of rmogelberg@gmail.com designates 2607:f8b0:4864:20::b2f as permitted sender) smtp.mailfrom=rmogelberg@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-yb1-xb2f.google.com (mail-yb1-xb2f.google.com. [2607:f8b0:4864:20::b2f]) by gmr-mx.google.com with ESMTPS id s12-20020a056e021a0c00b00365e9e3139fsi121168ild.2.2024.04.18.07.02.11 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Thu, 18 Apr 2024 07:02:11 -0700 (PDT) Received-SPF: pass (google.com: domain of rmogelberg@gmail.com designates 2607:f8b0:4864:20::b2f as permitted sender) client-ip=2607:f8b0:4864:20::b2f; Received: by mail-yb1-xb2f.google.com with SMTP id 3f1490d57ef6-d9b9adaf291so957660276.1 for ; Thu, 18 Apr 2024 07:02:11 -0700 (PDT) X-Received: by 2002:a25:ae1f:0:b0:dda:e401:df8c with SMTP id a31-20020a25ae1f000000b00ddae401df8cmr3151375ybj.48.1713448930681; Thu, 18 Apr 2024 07:02:10 -0700 (PDT) MIME-Version: 1.0 From: =?UTF-8?Q?Rasmus_M=C3=B8gelberg?= Date: Thu, 18 Apr 2024 16:01:59 +0200 Message-ID: Subject: [HoTT] Types 2024, Call for Participation To: homotopytypetheory@googlegroups.com Content-Type: multipart/alternative; boundary="000000000000dab57206165f6adf" X-Original-Sender: rmogelberg@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20230601 header.b=I5FKGP84; spf=pass (google.com: domain of rmogelberg@gmail.com designates 2607:f8b0:4864:20::b2f as permitted sender) smtp.mailfrom=rmogelberg@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , --000000000000dab57206165f6adf Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Call for Participation TYPES 2024 30th International Conference on Types for Proofs and Programs Copenhagen, Denmark, 10 - 14 June 2024 https://types2024.itu.dk REGISTRATION ------------ Registration is now open at https://types2024.itu.dk/Registration.html * Early registration until May 13 * Late registration until May 30 Students can register at a reduced fee. For details, see the above link. ACCOMMODATION ------------ We have reserved a number of hotel rooms at reduced rates. * Some rooms are only available until April 24! A small number of rooms may be available as late as May 24, but supply is limited after April 24. We therefore encourage participants to book these soon. More details at https://types2024.itu.dk/Venue.html INVITED SPEAKERS ---------------- * Brigitte Pientka (McGill University, Canada) * Egbert Rijke (University of Ljubljana, Slovenia) * Talia Ringer (University of Illinois at Urbana-Champaign, USA) There will also be a special session in memory of Peter Aczel, organised by Peter Dybjer. The session will consist of talks by * Nicola Gambino (University of Manchester, UK) * Michael Rathjen (University of Leeds, UK) BACKGROUND ---------- The TYPES meetings are a forum to present new and on-going work in all aspects of type theory and its applications, especially in formalised and computer assisted reasoning and computer programming. The TYPES areas of interest include, but are not limited to: * foundations of type theory and constructive mathematics; * applications of type theory; * dependently typed programming; * industrial uses of type theory technology; * meta-theoretic studies of type systems; * proof assistants and proof technology; * automation in computer-assisted reasoning; * links between type theory and functional programming; * formalizing mathematics using type theory. We encourage talks proposing new ways of applying type theory. In the spirit of workshops, talks may be based on newly published papers, work submitted for publication, but also work in progress. PROGRAMME COMMITTEE ------------------- Patrick Bahr (IT University of Copenhagen, Denmark) (co-chair) Henning Basold (Leiden University, The Netherlands) Andrej Bauer (University of Ljubljana, Slovenia) Marco Carbone (IT University of Copenhagen, Denmark) Jesper Cockx (TU Delft, The Netherlands) Greta Coraglia (University of Milan, Italy) Peter Dybjer (Chalmers University of Technology, Sweden) Yannick Forster (INRIA, France) Hugo Herbelin (INRIA, France) Patricia Johann (Appalachian State University, USA) Marie Kerjean (CNRS, France) Ekaterina Komendantskaya (University of Southampton, United Kingdom) Meven Lennon-Bertrand (University of Cambridge, United Kingdom) Assia Mahboubi (INRIA, France) Sonia Marin (University of Birmingham, United Kingdom) Anders M=C3=B6rtberg (Stockholm University, Sweden) Rasmus Ejlers M=C3=B8gelberg (IT University of Copenhagen, Denmark) (co-ch= air) Benjamin Pierce (University of Pennsylvania, USA) Jakob Rehof (Technical University of Dortmund, Germany) Simona Ronchi Della Rocca (University of Turin, Italy) Kristina Sojakova (Vrije Universiteit Amsterdam, The Netherlands) Ana Sokolova (University of Salzburg, Austria) Bas Spitters (Aarhus University, Denmark) Wouter Swierstra (Utrecht University, The Netherlands) Philip Wadler (University of Edinburgh, United Kingdom) TYPES STEERING COMMITTEE ------------------------ Sandra Alves (University of Porto, Portugal) Eduardo Hermo Reyes (Formal Vindications, Spain) Rasmus Ejlers M=C3=B8gelberg (IT University of Copenhagen, Denmark) Paige Randall North (Utrecht University, The Netherlands) (chair) Matthieu Sozeau (INRIA & Universit=C3=A9 de Nantes, France) Benno van den Berg (University of Amsterdam, The Netherlands) (secretary) ABOUT TYPES ----------- The TYPES meetings from 1990 to 2008 were annual workshops of a sequence of five EU funded networking projects. From 2009 to 2021, TYPES has been run as an independent conference series. Previous TYPES meetings were held in Antibes (1990), Edinburgh (1991), B=C3=A5stad (1992), Nijmegen (1993), B=C3=A5stad (1994), Torino (1995), Aussois (1996), Kloster Irsee (1998), L=C3=B6keberg (1999), Durham (2000), Berg en Dal near Nijmegen (2002), Torino (2003), Jouy-en-Josas near Paris (2004), Nottingham (2006), Cividale del Friuli (2007), Torino (2008), Aussois (2009), Warsaw (2010), Bergen (2011), Toulouse (2013), Paris (2014), Tallinn (2015), Novi Sad (2016), Budapest (2017), Braga (2018), Oslo (2019), Virtual (2021), Nantes (2022), Val=C3=A8ncia (2023). CONTACT ------- Email: types2024@easychair.org ORGANIZERS ---------- Patrick Bahr (IT University of Copenhagen, Denmark) Marco Carbone (IT University of Copenhagen, Denmark) Rasmus Ejlers M=C3=B8gelberg (IT University of Copenhagen, Denmark) --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/CAO0VQQaAZUr2jdcDNhLv0RW6dJcRsdmy4hdhZ0c%2BORg0LO2Oww%40= mail.gmail.com. --000000000000dab57206165f6adf Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
=C2=A0 =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 Call=C2=A0for Participation
=C2=A0 =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 =C2=A0 =C2=A0TYPES=C2=A02024
=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 30th International C= onference on
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0Types=C2=A0for Proofs and Programs
=C2=A0
=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 Copenhagen, Denmark, 10 - 14 = June 2024
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0https://types2024.itu.dk

=C2=A0 = =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0

REGI= STRATION
------------

Registration is now open at

https://types2024.itu.dk/Re= gistration.html

* Early registration until May 13
* Late regi= stration until May 30

Students can register at a reduced fee. For de= tails, see the above link.


ACCOMMODATION
------------
We have reserved a number of hotel rooms at reduced rates.

* Some = rooms are only available until April 24!

A small number of rooms may= be available as late as May 24, but supply is
limited after April 24. = We therefore encourage participants to book these
soon. More details at=
=C2=A0
https://types= 2024.itu.dk/Venue.html


INVITED SPEAKERS
----------------<= br>
* Brigitte Pientka (McGill University, Canada)
* Egbert Rijke (Un= iversity of Ljubljana, Slovenia)
* Talia Ringer (University of Illinois = at Urbana-Champaign, USA)

There will also be a special session in me= mory of Peter Aczel, organised
by Peter Dybjer. The session will consist= of talks by

* Nicola Gambino (University of Manchester, UK)
* M= ichael Rathjen (University of Leeds, UK)


BACKGROUND
---------= -

The TYPES meetings are a forum to present new and on-going work in= all
aspects of type theory and its applications, especially in formalis= ed
and computer assisted reasoning and computer programming.

The = TYPES areas of interest include, but are not limited to:

* foundatio= ns of type theory and constructive mathematics;
* applications of type t= heory;
* dependently typed programming;
* industrial uses of type the= ory technology;
* meta-theoretic studies of type systems;
* proof ass= istants and proof technology;
* automation in computer-assisted reasonin= g;
* links between type theory and functional programming;
* formaliz= ing mathematics using type theory.

We encourage talks proposing new = ways of applying type theory. In the
spirit of workshops, talks may be b= ased on newly published papers,
work submitted for publication, but also= work in progress.


PROGRAMME COMMITTEE
-------------------
Patrick Bahr =C2=A0(IT University of Copenhagen, Denmark) (co-chair)Henning Basold =C2=A0(Leiden University, The Netherlands)
Andrej Bauer= =C2=A0(University of Ljubljana, Slovenia)
Marco Carbone =C2=A0(IT Unive= rsity of Copenhagen, Denmark)
Jesper Cockx =C2=A0(TU Delft, The Netherla= nds)
Greta Coraglia =C2=A0(University of Milan, Italy)
Peter Dybjer = =C2=A0(Chalmers University of Technology, Sweden)
Yannick Forster =C2=A0= (INRIA, France)
Hugo Herbelin =C2=A0(INRIA, France)
Patricia Johann = =C2=A0(Appalachian State University, USA)
Marie Kerjean =C2=A0(CNRS, Fra= nce)
Ekaterina Komendantskaya =C2=A0(University of Southampton, United K= ingdom)
Meven Lennon-Bertrand =C2=A0(University of Cambridge, United Kin= gdom)
Assia Mahboubi =C2=A0(INRIA, France)
Sonia Marin =C2=A0(Univers= ity of Birmingham, United Kingdom)
Anders M=C3=B6rtberg =C2=A0(Stockholm= University, Sweden)
Rasmus Ejlers M=C3=B8gelberg =C2=A0(IT University o= f Copenhagen, Denmark) (co-chair)
Benjamin Pierce =C2=A0(University of P= ennsylvania, USA)
Jakob Rehof =C2=A0(Technical University of Dortmund, G= ermany)
Simona Ronchi Della Rocca =C2=A0(University of Turin, Italy)
= Kristina Sojakova =C2=A0(Vrije Universiteit Amsterdam, The Netherlands)
= Ana Sokolova =C2=A0(University of Salzburg, Austria)
Bas Spitters =C2=A0= (Aarhus University, Denmark)
Wouter Swierstra =C2=A0(Utrecht University,= The Netherlands)
Philip Wadler =C2=A0(University of Edinburgh, United K= ingdom)

TYPES STEERING COMMITTEE
------------------------

= Sandra Alves (University of Porto, Portugal)
Eduardo Hermo Reyes (Formal= Vindications, Spain)
Rasmus Ejlers M=C3=B8gelberg (IT University of Cop= enhagen, Denmark)
Paige Randall North (Utrecht University, The Netherlan= ds) (chair)
Matthieu Sozeau (INRIA & Universit=C3=A9 de Nantes, Fran= ce)
Benno van den Berg (University of Amsterdam, The Netherlands) (secre= tary)

ABOUT TYPES
-----------

The TYPES meetings from 1990= to 2008 were annual workshops of a sequence
of five EU funded networkin= g projects. From 2009 to 2021, TYPES has been
run as an independent conf= erence series. Previous TYPES meetings were
held in Antibes (1990), Edin= burgh (1991), B=C3=A5stad (1992), Nijmegen
(1993), B=C3=A5stad (1994), T= orino (1995), Aussois (1996), Kloster Irsee
(1998), L=C3=B6keberg (1999)= , Durham (2000), Berg en Dal near Nijmegen
(2002), Torino (2003), Jouy-e= n-Josas near Paris (2004), Nottingham
(2006), Cividale del Friuli (2007)= , Torino (2008), Aussois (2009),
Warsaw (2010), Bergen (2011), Toulouse = (2013), Paris (2014), Tallinn
(2015), Novi Sad (2016), Budapest (2017), = Braga (2018), Oslo (2019),
Virtual (2021), Nantes (2022), Val=C3=A8ncia = (2023).

CONTACT
-------

Email: types2024@easychair.org

ORGANIZERS
----------=

Patrick Bahr (IT University of Copenhagen, Denmark)
Marco Carbon= e (IT University of Copenhagen, Denmark)
Rasmus Ejlers M=C3=B8gelberg (I= T University of Copenhagen, Denmark)

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAO0VQQaAZUr2jdcDNhLv0RW6dJcRsd= my4hdhZ0c%2BORg0LO2Oww%40mail.gmail.com.
--000000000000dab57206165f6adf--