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.1 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ed1-x538.google.com (mail-ed1-x538.google.com [IPv6:2a00:1450:4864:20::538]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 3e49728a for ; Fri, 24 May 2019 16:44:23 +0000 (UTC) Received: by mail-ed1-x538.google.com with SMTP id f41sf15006146ede.1 for ; Fri, 24 May 2019 09:44:23 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1558716262; cv=pass; d=google.com; s=arc-20160816; b=m2g6Il5MniwLi4nSopdu9fdPKoA9T7EXAYEOMk4vdoknfU9tg3C2f7LmfsHH8bbuel K+qAT1m/F/8um1u4sAQRRXX1P2gd1wCo/8ruPHVu9m9KbFcSBfvnxLSF0fyiPNKPYdZP ND7eOgXxDivDUEzfUSRrdEG/DBsXMxXpMz5qZRpK9OCGJFqH/1YwtdB1f2t//Odpzdqf LbTHVNOFrmaYLacxuofcinO6IDnONtcLKuwCAAvTNnYBYDggwuhbvNooTcTofcvaAfcz dbNLOESgw2PXw+n7UWuLr+NUed7+yF9Tvo5JkFhV+aTyCzonQqxLk5uf6os8s7dd1wiy piVA== 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:content-transfer-encoding:content-language :in-reply-to:mime-version:user-agent:date:message-id:from:to :references:subject:sender:dkim-signature; bh=JraEsSNbowkwlE0t7tATdRMTDhE7MRZZHaH4t6CMKqo=; b=hfj508oIZHkAqqARMIM8Z+yAUIfzFyfcENBybQqyOnckdUN9XSOhIdGA1PWPvQ8d89 XBXkAkiwunkvFUBYZ6//kZFH3XN2ydWf9niMZXT+E6a6aGUKJ8rySYfA61455Uc+hFFl yUdsXMYOl2aGu7x6XT/89bfIwja0ciRVCsBeaRko3DCL236srPZjO6nq1jjScyLZi7sl 2yyazBxuZmrW7Qiip36DYjdlaE5er7Ah+qLcTvUzaRGnGYA+1/ugbvoNbk5/AuOac+qm EnRsihd8+Soi8Ys2e/MLd7CmfQY9CS03Io0SH0R5FgitkahecLmKnwNXHOdKQ+Wi7VcR hfsA== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of palmgren@math.su.se designates 77.238.35.140 as permitted sender) smtp.mailfrom=palmgren@math.su.se DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:subject:references:to:from:message-id:date:user-agent :mime-version:in-reply-to:content-language:content-transfer-encoding :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=JraEsSNbowkwlE0t7tATdRMTDhE7MRZZHaH4t6CMKqo=; b=dZudRH3gYTHT8mhYOUb3S5IaUnLJ15l3J6FscWA1iUIQJyVxtrD/4XEQhUYs+KJtuQ yaEQ2i9Ph1gNbQLvlWQ6LFmyhsR50bRRc8+H7rpBExxteZPC+CmxHbe+O6Z35+yxn40x xnZM+CYjTUzVbBvCUs7OOz4HACYRHoPZBTpVZPwBtuvYtMyMWCMTfJEu8g2GRg3b9NMm hRi+++qcxqBv99llFMfg++VlP8S8e581CGuTyMBMf4MFUn812fufl7OqWe66j8RIDI35 T6uhnSxX5Mv54Gt1mxphKuO07r0YeF3MwzzJ6UnDOoq5RzjJCjJysTP5XUT8jALotaYS uPGw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:subject:references:to:from:message-id :date:user-agent:mime-version:in-reply-to:content-language :content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=JraEsSNbowkwlE0t7tATdRMTDhE7MRZZHaH4t6CMKqo=; b=rnxQHKXYGgrWhrtwATk7AzmwA/4QFSFLi9whP+YtqnmPE5reziTSxcI/AXvmnEvG1h T0dpOaiPIs5/5IhYDQYubGEILTo9qhyCtl4yP9EibarScb+Rl2FHGJbXCxoSqhvvJv1x t9o6AG8aNx/mg6G7wDFYhbjAaqAI0F7EV2GUjIDxubFBNSsCwx2KaOaGMxbZFl/zdrVL nEgKSSWutrg9mqJRNS/PDKLNTLkxuZYVLqaJB0pb3Je5VKmycc0NYRRZesG7caAR2SwT kE/93uuBCE1f66oFr18jmotALlv7onl2WqLBV2TtkwTwl6wlhV3OyvBzHx2gRTEo/Ik4 Es3A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVat6lvF3v9c8LnJMJQtdOBA63tfDJDuoR1u9DqxxZO6o4FyCMr flXUH3bNJKKd2IawMTl9RH4= X-Google-Smtp-Source: APXvYqxjr9/K58W0cNq0WEF0WXMzjnevktJPBxN9yme8I8YA2jaYAerK/1L7dzQJ4edd2BQtOwLewQ== X-Received: by 2002:aa7:cd14:: with SMTP id b20mr1414469edw.305.1558716262490; Fri, 24 May 2019 09:44:22 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a17:906:7807:: with SMTP id u7ls2273296ejm.13.gmail; Fri, 24 May 2019 09:44:21 -0700 (PDT) X-Received: by 2002:a17:906:5c12:: with SMTP id e18mr16851760ejq.157.1558716261946; Fri, 24 May 2019 09:44:21 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1558716261; cv=none; d=google.com; s=arc-20160816; b=wTiIvN6gb0FDa3ST9Z3XzThvZQLOb0P6mVZAy8E7HMLTjgHjaCueJDmb5f4BUNoh7a OJC4Mfc1VA037aEYuN3/uQOBRfZPmnhYLfPFBKYPmNPP35fjrmOEFkbTPD9HPnmMdAzD ExVE29saDOmJFUpjtXLyA4yWyGWIux+ja0Y3pm9Vkd9choEF8rx0Gg2x0AOUt6QEmxwT 48ZfmMDwYdJwt2Dop6LBkte+5IqwW5nQDgU8IU/uKioSG60ZmzQunqv4f/thvG24Aa42 +CN81WYh/HoenQkaDsJCBnGDABrq0LQlZK6Fi6AxQROVdvQUyWw2cEmZmeVPcnwLxO1G yTiA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:content-language:in-reply-to:mime-version :user-agent:date:message-id:from:to:references:subject; bh=9/QOgYuLgGo1gTeC0x8zED4ky9ODVu8V0h4oNgjf9ik=; b=r6DqXPI++jNFZLgj9bnpX2rp0g+iCYQEbDA4E0URdUn592lCqDP3ddGyyDDTrgJ7jZ tBYGGEIPgfqbEDGpFv8UFqZ5JtSc8EOzaHm6dba5PJsRuPPATTrQekgYnMtrpqoixIS/ 7YXKk/IHZiZJ3iJ/l8RqJ4jHNaqVK+AoYRvb1y4ZseWGfkAiOq9HDPLnWcN6MSGTTBsK EIPgS5p7CwFff6aM8rwsqPsDmpGrj/i3CvBGyk7r8qYWssF/onobQPOyJPL+u9MqKI41 uL6W/ImeSLcbejAbN20kA4BcyBbQzzUM8+J/jk8B0FZfFoRHGjG3nxemHfxA2pqvEVmH x2oQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of palmgren@math.su.se designates 77.238.35.140 as permitted sender) smtp.mailfrom=palmgren@math.su.se Received: from mail-prod-route02.it.su.se (mail-prod-route02.it.su.se. [77.238.35.140]) by gmr-mx.google.com with ESMTPS id n9si172560ejz.0.2019.05.24.09.44.21 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 24 May 2019 09:44:21 -0700 (PDT) Received-SPF: pass (google.com: domain of palmgren@math.su.se designates 77.238.35.140 as permitted sender) client-ip=77.238.35.140; Received: from e-mailfilter01.sunet.se (e-mailfilter01.sunet.se [IPv6:2001:6b0:8:2::201]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by mail-prod-route02.it.su.se (Postfix) with ESMTPS id 459XJj3HqBzxds for ; Fri, 24 May 2019 18:44:21 +0200 (CEST) Received: from smtp.su.se (mail-prod-smtp04.it.su.se [130.237.181.99]) by e-mailfilter01.sunet.se (8.14.4/8.14.4/Debian-8+deb8u2) with ESMTP id x4OGiKmx055704 (version=TLSv1/SSLv3 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NO) for ; Fri, 24 May 2019 18:44:20 +0200 Received: from Eriks-Palmgrens-MacBook-Air.local (c80-216-86-31.bredband.comhem.se [80.216.86.31]) (Authenticated sender: epalm) by smtp.su.se (Postfix) with ESMTPSA id 459XJh4M3Wz2vPD for ; Fri, 24 May 2019 18:44:20 +0200 (CEST) Subject: [HoTT] Final CFP - MLoC 2019 : The Scope and Limits of Neutral Constructivism (Stockholm, August 20-23) References: To: homotopytypetheory From: Erik Palmgren X-Forwarded-Message-Id: Message-ID: <21fc268e-faf6-01ae-57c5-e3721aef82c3@math.su.se> Date: Fri, 24 May 2019 18:44:20 +0200 User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:60.0) Gecko/20100101 Thunderbird/60.6.1 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Language: sv Content-Transfer-Encoding: quoted-printable X-Bayes-Prob: 0.5 (Score 0, tokens from: outbound, outbound-su-se:default, su-se:default, base:default, @@RPTN) X-CanIt-Geo: ip=130.237.181.99; country=SE; region=Stockholm; city=Stockholm; latitude=59.3333; longitude=18.0500; http://maps.google.com/maps?q=59.3333,18.0500&z=6 X-CanItPRO-Stream: outbound-su-se:outbound (inherits from outbound-su-se:default,su-se:default,base:default) X-Canit-Stats-ID: 090ggIkMv - e4e17d5d4582 - 20190524 X-CanIt-Archive-Cluster: PfMRe/vJWMiXwM2YIH5BVExnUnw X-Scanned-By: CanIt (www . roaringpenguin . com) X-Original-Sender: palmgren@math.su.se X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of palmgren@math.su.se designates 77.238.35.140 as permitted sender) smtp.mailfrom=palmgren@math.su.se 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: , =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D Final Call for Participation and Contributed Papers =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D Mathematical Logic and Constructivity: The Scope and Limits of Neutral Constructivism Stockholm, Sweden, August 20-23, 2019 http://logic.math.su.se/mloc-2019/ Deadline for contributed talks: May 31, 2019 =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D With Errett Bishop's seminal work Foundations of Constructive Analysis 1967, a neutral position in the foundations of constructive mathematics emerged. It avoided Brouwer's assumptions about choice-sequences and continuity, and it did not assume that every total function on the natural numbers is computable. This made the position palatable also to the classical mathematician, and it is in the intersection of the three realms of foundations, commonly designated by the abbreviations INT, RUSS and CLASS. Successful full-fledged formal logical foundations for neutral constructivism exists, among the most well-known are Aczel-Myhill set theory and Martin-L=C3=B6f type theory. Neutral constructive mathematics may also be studied for systems that make fewer ontological assumptions, which is important for reverse mathematics. To the surprise of many in constructive mathematics a new principle about sequences, the boundedness principle BD-N, was discovered, and found to be true in all the three realms without being true in neutral constructvism. Further principles of this kind are being investigated. In type theory new axioms have been discovered, such as the univalence axiom, whose constructive status was only later settled. Important questions are whether new axioms can be modelled indirectly using neutral constructive methods, or whether they can be directly justified. This workshop aims to focus on the scope and limits of neutral constructivism. The study of neutral constructivism paves the way for further developments of interactive proof systems, which is of strategic importance for verification of software, and in particular, correctness-by-construction software. INVITED SPEAKERS INCLUDE * Douglas S. Bridges, University of Canterbury, Christchurch, New Zealand * Thierry Coquand, Chalmers and G=C3=B6teborg University, Sweden * Martin Escardo, University of Birminham, England (to be confirmed) * Makoto Fujiwara, Meiji University Tokyo, Japan * Nicola Gambino, Leeds University, England * Henri Lombardi, Universit=C3=A9 Franche-Comt=C3=A9, France * Maria Emilia Maietti, University of Padova, Italy * Takako Nemoto, JAIST, Japan * Iosif Petrakis, L-M University, Munich, Germany * Thomas Streicher, TU Darmstadt, Germany * Hideki Tsuiki, Kyoto University, Japan * Chuangjie Xu, L-M University, Munich, Germany * Keita Yokoyama, JAIST, Japan FURTHER SPEAKERS * Hajime Ishihara, JAIST, Japan * Anders M=C3=B6rtberg, Carnegie Mellon University and Stockholm University CONTRIBUTED TALKS Proposals for contributed talks are welcome and are to be submitted via the EasyChair system: https://easychair.org/conferences/?conf=3Dmloc19 Suggested length of abstract: half a page. Deadline for contributed talks: May 31, 2019 (anywhere on Earth) Notification of acceptance: June 14, 2019 PROGRAM COMMITTEE * Hajime Ishihara, JAIST, Japan (co-chair) * Tatsuji Kawai, JAIST, Japan * Peter LeFanu Lumsdaine, Stockholm University * Anders M=C3=B6rtberg, Carnegie Mellon University and Stockholm Universit= y * Erik Palmgren, Stockholm University (co-chair) REGISTRATION The workshop is free of charge, but to aid planning please register by sending the organizers an email mloc19@math.su.se with name and affilliation at the latest August 13, 2019. TRAVEL GRANTS A limited number of travel and accommodation grants are available for=20 contributed speakers and/or younger participants. Please write to=20 mloc19@math.su.se if you are interested in applying for these. VENUE Department of Mathematics, Stockholm University, Sweden WEB PAGES http://logic.math.su.se/mloc-2019/ IMPORTANT DATES 2 April 2019 registration opens 31 May 2019 abstracts for contributed talks 14 June 2019 notification of acceptance 13 August 2019 registration closes 20-23 August 2019 conference --=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/21fc268e-faf6-01ae-57c5-e3721aef82c3%40math.su.se. For more options, visit https://groups.google.com/d/optout.