From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.2 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_AU,DKIM_VALID_EF,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-wm1-x33c.google.com (mail-wm1-x33c.google.com [IPv6:2a00:1450:4864:20::33c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 717295b0 for ; Fri, 1 Feb 2019 02:04:14 +0000 (UTC) Received: by mail-wm1-x33c.google.com with SMTP id t21sf1193414wmt.3 for ; Thu, 31 Jan 2019 18:04:14 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1548986654; cv=pass; d=google.com; s=arc-20160816; b=HrKzDUI4MktyGjNaZc2VCcx8TY41yfUwnPkDfnkEVHw1AFrT8yon3Izz/B3KHUX7gQ bqqhUMy/3ec+06BrSbWkaxG9lVWKal8fL6YVmC9KqsCaRtm7E+60NdbYXZR9fSftU8ux iFzm/uEV9RaIJHXmQd2mXtz6gdqFjmdI8V1n/TlGceHMWE5hWgsoS9ysagN8n6bsHz1Q 1X3L9jf9qS7BaxGgba+YFdzaPCVPhxbOq3vTigzZ52GOFt5JwXZ1kQ6woL5qWhVQDSLq /sNvSP5kXPU/Rkv9mYfwPuA1TjLNtA3fjobiiDmBc3SZI4a2IQ58qbVE6pWPMbJr6rwa +9NQ== 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:reply-to:content-transfer-encoding :content-language:mime-version:user-agent:date:message-id:subject :from:to:dkim-signature; bh=fdnXINnvKWsc6YfViexulvY9/nFi7iQo6ie6PtbNUU4=; b=qagYSI1hbgEa5TCKSZNSUAgufl6OAlopZttvYyiGwLYjY26nHk9OBA/K7dP8IbiCz4 3HiYgjr/qODUG91vUzL/7ZxFVtRCw3Gm+rXS9gN5wsmpQE9En6aRmZ64EjGCpDIMQBnr qjL/yubSd2kWNAxIBuOEnqqJKe+HD2+SqU7KKWnN94x8p0SuQUDVUJCLAsjVEujbJ58T ers2ebeU/EN2Js6PvFFByZpglI4FXosSO1UGSd/yQ5e1tW3utxazAz7boyEW/BqtwkW1 rM30JPeDPmYIORLsLzuEQTmHQi1goOY5H5DJSSwAOYuHPy4DRHye8VsVqkXUlZHPpRCy f9tQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo.martin@googlemail.com does not designate 147.188.128.137 as permitted sender) smtp.mailfrom=escardo.martin@googlemail.com; dmarc=fail (p=QUARANTINE sp=QUARANTINE dis=QUARANTINE) header.from=googlemail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=to:from:subject:message-id:date:user-agent:mime-version :content-language:content-transfer-encoding:x-original-sender :x-original-authentication-results:reply-to:precedence:mailing-list :list-id:list-post:list-help:list-archive:list-unsubscribe; bh=fdnXINnvKWsc6YfViexulvY9/nFi7iQo6ie6PtbNUU4=; b=Xjx1EE8qneNoTUhRzpQT7/ElRHQlvOFYP2VssFRP0m+T1++DJhULhuULiP/UgJNI29 jdjuKALsFFX069mBoBQ0Q9OghbZ4oUZuARpsyfCH1oo2z3SgbH8sDOWU/tUphKzcQ8+s aLtwahmmhMfezB1NE4V5RClmof76CyRk2W274NC5v2KrMdsb41CumMu0ZVZPoRyDuZpm 4cZkYLRbqNiAXA3mUuA+G+vwnmL3racJYwtc+8/hiql/2V3MQzFGGEd4KD2+JWM0mIRN /kYfff/tOYyCuRN8pEIYJ4E5KaQtvwQJ3H8u0goQhvVDoU/afexcno0ugkQbGNUBzLQB ZSVA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:to:from:subject:message-id:date:user-agent :mime-version:content-language:content-transfer-encoding :x-original-sender:x-original-authentication-results:reply-to :precedence:mailing-list:list-id:x-spam-checked-in-group:list-post :list-help:list-archive:list-unsubscribe; bh=fdnXINnvKWsc6YfViexulvY9/nFi7iQo6ie6PtbNUU4=; b=jt/jIqV33PJ0MFrPzSJNeMP8qzt7zVUnIOn0l93f3S3aO/8NbJ/9UOmj1J9ycBOtMo X+xd0ffbcl6nqd/P1KVi2bDJ+hD3bg8pm5q+fMEWLjmBaMrxQqTnJZAi7AsqTtlxNzll 8NIhxl3O4L4fW/hoDjYWXg+gFViq7VlvOfgNtAgMfopiR6QdJr6D+7tQOMqQkXZTogRn QetQURJFfMrBiVoOkRlGTBWMSUalsnGQDn2N6EeibRbquu97tNBd4S9Ul1yKMI6oZ8zG jYaaCtSAa016tuN94vBNwb228GEnDsuFS9qZAIKU9Tv04g1aWdNKS8CSZZPT7O2/gY6H 0KqA== X-Gm-Message-State: AHQUAuYQSnZdtUBWrntu0SmEC4QoOgG+y8Bq0DD5WHwT2lVhiK338wfd XGJDxIAM+HmYDWijb3zheNA= X-Google-Smtp-Source: AHgI3IZLzf+F6etjO5xNXhuBen1tu8dLpuoQD0mjW3qYdB2afl0V+wW4zm9Y7EOIU778J/wlVBc7cw== X-Received: by 2002:adf:e743:: with SMTP id c3mr192160wrn.5.1548986654253; Thu, 31 Jan 2019 18:04:14 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:80c4:: with SMTP id b187ls608712wmd.0.canary-gmail; Thu, 31 Jan 2019 18:04:13 -0800 (PST) X-Received: by 2002:a1c:6584:: with SMTP id z126mr32859wmb.18.1548986653720; Thu, 31 Jan 2019 18:04:13 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1548986653; cv=none; d=google.com; s=arc-20160816; b=Dia6mzvAs4M2AonPR18xxcr5VDWfnSp+63eByUMS1OC5eYufHmpGkb2q2mCZnJOaRz 7YGZr867yYHmHAOuU8NsA+r7leuET0w7383R0hCKD+4hX01fVK1Os+wLPmxFgzimOXjt bN8+ZaHCNPr2BM3+LBohci4/krOzFa0VuSaS23HCKzZ1sReNFDHYGjnerYt7grZyp3Qp eanss2aE2XBQljHE7QOTwKXQVWEppYrXX6AjgoMo1AEwzLz5ScCzPeXJAaU7gHOf4Ufw G8drQ+QGh6hM3kpPdqqbFW3YyL/pF0nJNz4dz3RB5YnxGgjE3NL+GGriQ7TOtHznC/Tg eEqA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:mime-version:user-agent :date:message-id:subject:from:to; bh=QS9bRqEO0AWeIS6sdS6AGz+9+fPEEooXvakx/oKwGaM=; b=YfB1ZdYXgn7CxmHvP3THLn3Pcosje6VJMTlX/KkErNQhxq4o9XCbmmJkwFApSrW07E C7gOQX3uG127KaVaOSb58PybYvc0Rs9agC3xTUFzzrzRAm8A9Pv6LlMKc8f//8AiGOJf ASVzVCIknbuWhdr1C7rjf6XSRW7oXIQMkPp7bnVg11VohPXDarjDlIRnnXTqFCZD5osj rfd4jpy8l44Fp9GWP6WZ+vMPYSS8QOsuEcD4XP7Q6crYNl+Pd3QWl4KJ7cvIN03R14LO NC0Ne3OHMXFlUQBDGYSbx9Y6cSDTQDRutU+NbRLhslIzQ90lh6zR1gUe2hcNmSqJsCgb 6hEg== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo.martin@googlemail.com does not designate 147.188.128.137 as permitted sender) smtp.mailfrom=escardo.martin@googlemail.com; dmarc=fail (p=QUARANTINE sp=QUARANTINE dis=QUARANTINE) header.from=googlemail.com Received: from sun60.bham.ac.uk (sun60.bham.ac.uk. [147.188.128.137]) by gmr-mx.google.com with ESMTPS id j45si217730wre.0.2019.01.31.18.04.13 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 31 Jan 2019 18:04:13 -0800 (PST) Received-SPF: softfail (google.com: domain of transitioning escardo.martin@googlemail.com does not designate 147.188.128.137 as permitted sender) client-ip=147.188.128.137; Received: from [147.188.128.127] (helo=bham.ac.uk) by sun60.bham.ac.uk with esmtps (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256) (Exim 4.90_1) (envelope-from ) id 1gpOBh-0005tu-Ng; Fri, 01 Feb 2019 02:04:13 +0000 Received: from 174.58.189.80.dyn.plus.net ([80.189.58.174] helo=[192.168.1.93]) by bham.ac.uk (envelope-from ) with esmtpsa (TLSv1.2:ECDHE-RSA-AES128-GCM-SHA256:128) (Exim 4.90_1) id 1gpOBh-0007gK-DU using interface auth-smtp.bham.ac.uk; Fri, 01 Feb 2019 02:04:13 +0000 To: constructivenews , "HomotopyTypeTheory@googlegroups.com" From: "'Martin Escardo' via Homotopy Type Theory" Subject: [HoTT] Midlands Graduate School 2019 in the Foundations of Computing Science Message-ID: <8182c918-b569-dbed-2a51-9e42173633d3@googlemail.com> Date: Fri, 1 Feb 2019 02:04:12 +0000 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.4.0 MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Language: en-US Content-Transfer-Encoding: quoted-printable X-BHAM-SendViaRouter: yes X-BHAM-AUTH-data: TLSv1.2:ECDHE-RSA-AES128-GCM-SHA256:128 via 147.188.128.21:465 (escardom) X-Original-Sender: escardo.martin@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; spf=softfail (google.com: domain of transitioning escardo.martin@googlemail.com does not designate 147.188.128.137 as permitted sender) smtp.mailfrom=escardo.martin@googlemail.com; dmarc=fail (p=QUARANTINE sp=QUARANTINE dis=QUARANTINE) header.from=googlemail.com X-Original-From: Martin Escardo Reply-To: Martin Escardo 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: , Midlands Graduate School 2019 14-18 April 2019, Birmingham, UK http://events.cs.bham.ac.uk/mgs2019/ BACKGROUND: The Midlands Graduate School (MGS) in the Foundations of Computing Science provides an intensive course of lectures on the mathematical foundations of computing. The MGS has been running since 1999, and is aimed at PhD students in their first or second year of study, but the school is open to everyone, and has increasingly seen participation from industry. We welcome participants from all over the world! COURSES: Eight courses will be given. Participants usually take all the introductory courses and choose additional options from the advanced courses depending on their interests. Invited course - Adventures in Property Based Testing, John Hughes Introductory courses - Lambda Calculus, Venanzio Capretta - Category Theory, Thorsten Altenkirch - Univalent Type Theory in Agda, Mart=C3=ADn Escard=C3=B3 Advanced courses - Calculating programs, Jennifer Hackett - Type Refinement Systems, Noam Zeilberger - Synthesis of Reactive Systems, Rayna Dimitrova - Monoidal Categories, Higher Categories, Jamie Vicary REGISTRATION: Registration is =C2=A3220 for student, academic and independent participants, and =C2=A3420 for industry participants. Accommodation is not included; please see the conference webpage for advice. The registration deadline is ** Sunday, 31 March **. Spaces are limited, so please register early to secure your place. SPONSORSHIP: We offer a range of sponsorship opportunities for industry (bronze, silver, gold and platinum), each with specific benefits. Please see the website for further details. --=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. For more options, visit https://groups.google.com/d/optout.