From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.31.174.209 with SMTP id x200mr5161483vke.8.1487849034425; Thu, 23 Feb 2017 03:23:54 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.36.15 with SMTP id p15ls3678500ota.27.gmail; Thu, 23 Feb 2017 03:23:54 -0800 (PST) X-Received: by 10.129.82.77 with SMTP id g74mr12744780ywb.50.1487849034000; Thu, 23 Feb 2017 03:23:54 -0800 (PST) Return-Path: Received: from mail-qk0-x22e.google.com (mail-qk0-x22e.google.com. [2607:f8b0:400d:c09::22e]) by gmr-mx.google.com with ESMTPS id r6si354141ywb.6.2017.02.23.03.23.53 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 23 Feb 2017 03:23:53 -0800 (PST) Received-SPF: pass (google.com: domain of andrew....@gmail.com designates 2607:f8b0:400d:c09::22e as permitted sender) client-ip=2607:f8b0:400d:c09::22e; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of andrew....@gmail.com designates 2607:f8b0:400d:c09::22e as permitted sender) smtp.mailfrom=andrew....@gmail.com Received: by mail-qk0-x22e.google.com with SMTP id n127so28517439qkf.0 for ; Thu, 23 Feb 2017 03:23:53 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:sender:from:date:message-id:subject:to:cc :content-transfer-encoding; bh=qeWNT5E8SVpPEXT/CI/Dl7EWKqOK2ME8kLAi/ZJPhWA=; b=TpX0KTFczC//Eo1gqfN2HyozwOIo/6zDLfX2I2q79fTz5JqE2WFpHSVVZI0iNB2t68 LxeTSgyDQJpUjdfEfVeq9w+YH1Ap+CcFtqGal8s0Rx+86A4Fr1aHY5YBkxPDzMg7CyoY 9m1ZfSUlVo+Te7vIDFlxGG3PQ90KJcPqQdUXjNH4faKtSDnVHuNXtHXwuOPjci+k2Kdt MKvjnKZQHJ0Jyr37vdwXv1XFzbfjApmldD4oms0sBu2BkRlfmrGqOaJFt2pQuQ0bn/T9 ZQKQ+7XPeIe98D5IfjvyKVMcOAvwpv5meBnhYtzh//nw3q0PRJE7Fe31JyZJJaMk2gaA 40iA== X-Gm-Message-State: AMke39kZCj87JzJ6ZxfgiYx1WmShn8eFjkRGAZK5Yt6Mqs0AyRpIDaNKR6UfLY8jHkkgKCT4S3lCSxq5E2SYmw== X-Received: by 10.55.106.134 with SMTP id f128mr2496913qkc.16.1487849033764; Thu, 23 Feb 2017 03:23:53 -0800 (PST) MIME-Version: 1.0 Sender: andrew....@gmail.com Received: by 10.140.31.4 with HTTP; Thu, 23 Feb 2017 03:23:33 -0800 (PST) From: Andrew Pitts Date: Thu, 23 Feb 2017 11:23:33 +0000 Message-ID: Subject: Call for participation: Workshop on Computer-aided Mathematical Proof, Cambridge UK, 10-14 July 2017 To: "HomotopyT...@googlegroups.com" Cc: "Prof. Andrew M Pitts" , Jeremy Avigad Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable The following workshop may be of interest (since it will feature some HoTT-related talks): =E2=80=94=E2=80=94 Workshop on Computer-aided Mathematical Proof, Cambridge UK, 10-14 July 201= 7 Applications are invited, closing date 8 April, to take part in a workshop on Computer-aided Mathematical Proof, part of the =E2=80=9CBig pro= of=E2=80=9D programme at the Isaac Newton Institute in Cambridge. Speakers include: Jeremy Avigad, Steve Awodey, Jasmin Blanchette, Leo De Moura, Stephanie Dick, Martin Escardo, Jacques Fleuriot, Georges Gonthier, Tom Hales, Marjin Heule, Patrick Ion, Mateja Jamnik, Michael Kohlhase, Ekaterina Komendantskaya, Dan Licata, Peter Lumsdaine, Assia Mahboubi, Ursula Martin, Tobias Nipkow, Grant Passmore, Larry Paulson, Alison Pease, Floris van Doorn and Vladimir Voevodsky For more details and to apply see https://www.newton.ac.uk/event/bprw01 This event is part of the activities for the programme on Big proof (26 June -- 4 August 2017) organised by Jeremy Avigad, Georges Gonthier, Ursula Martin, J Strother Moore, Larry Paulson, Andrew Pitts and Natarajan Shankar. The workshop brings together mathematicians interested in employing proof technology in their research, logicians exploring pragmatic and foundational issues in the formalisation of mathematics, and computer scientists engaged in developing and applying proof technology. It will explore foundational, theoretical, and practical challenges in exploiting proof technology to transform mathematical practice across a range of scientific and engineering disciplines.