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-wr1-x439.google.com (mail-wr1-x439.google.com [IPv6:2a00:1450:4864:20::439]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 7cce33d5 for ; Sat, 4 May 2019 19:54:32 +0000 (UTC) Received: by mail-wr1-x439.google.com with SMTP id l2sf7289622wrn.23 for ; Sat, 04 May 2019 12:54:32 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1556999672; cv=pass; d=google.com; s=arc-20160816; b=f9+xiwwR+2xdeL8mv/+wqxp6Fz5SJOktblXBw37hhnM8lwu9GSONxFCm+t3Rqgx/HW 0c15uHPVnZX11ogEYISNUi3XG+OdirftMajXaYhlnNMbti+ISpXXkLasaV0g/IxDQA2m Bl4m5dRkuamBQQ1Ikgcb0VvbR8VfiUzL6NfkXJQL3r5fmH58haZ+RETJ8y5c/4uVZElM 7xnpElyykeOHygHDBKdt1QlvAg4D+qWg4hLRcouNCYxpmSbGFR3+F/BluylPX9VBSah+ z3YcOBGFh3EPWSU6aI4lMt+4Hj4kCQiNno9C8CmlhkA6pw/z+LJEXR+M7Q7OuS2SDlCV RdGw== 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 :mime-version:user-agent:date:message-id:subject:from:to:sender :dkim-signature; bh=JCCq/e11VLlo8v9YAEBiR9lqt+LxsKEe/d51wsnuBk0=; b=ooS+baqzLsVyqAlW1arPD+CWEnzOaME/rgCneAa5FXztoyHJppF1EEKNTkVghZpiPg RGiPdVjsPppoBdJvNqT7cqat9hTTDGZ5Bz+0jLPZA3dncdDtQAmB+rcPZaLSSEmplPXT 8EXdLwNUpTEnK5n9rHqn7feLaeqDguTnM9Gx2Om62jOudOHv+Hj18/C8EIkWT5kUjqaK fsRoaeWUDdwHysBruaiu5U4mmVOHHtRY39yfQWjJrNiGt7hYG2N14TcDQpL4wMHnegI9 tuhP8TSb/w3kSEBnOtRxTBrqSMho1ffQTUYtCcj2/dGi534QLFKlwisI/YBbTEWx6mH7 /Vag== 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:to:from:subject:message-id:date:user-agent:mime-version :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=JCCq/e11VLlo8v9YAEBiR9lqt+LxsKEe/d51wsnuBk0=; b=BXVQTDqtDtGjC9a2gPkWpaCdNqUccy3g4cc0RKsZxxqxamuID44stPb0h/BMcDO34F XwH0TVKlL9cfZO5Kt+PcRXOKNtCqCVDokUL/S9MBF8noXB0YAVaPRN7q4RhbKsHdlFaO wimQwyw/CJB9+bfpRkay1STP+zc/wwUwgTAJ86hI4U3+UW3tK77mAmzbcuG1euenfADJ EygnIkYNYqNVhC1b8lu7l60esNmmwDNg2IiASaA/Ql69mkwKGJx6p9i0fBB+u8wJYQjK cQhZzA6VbqpOleXMIPAM0spNHT8Tg+wvJ7tQCQ3zJ9noYnECq7zkyxDsn6t/xcp5u9oO 0fpw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender: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:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=JCCq/e11VLlo8v9YAEBiR9lqt+LxsKEe/d51wsnuBk0=; b=NYJRWWzmjR2t3WQ2f6OfNKjCSOhwcbhoJd2ViRjL+avUf2P69aA1gII1H6zRCk3Z+o 5Ao7isAnGTfJ6YqlwLmahkAgMRIerkat4YCYmxM4Aahpz81a4ymI2NJXY2ZVybaj9MWg isbAeFLZ9NG8H7i/UCxSZQPRDrECcVNkL5/p0+3wzJWwuOlCFgfOKJ21qNo/CU5XX1aa 5OFIWMWTHZtEpVy1QFKlS2BlwCKypNZfxoFFMhqMNyESYlVzYloMtEIAq7ledoiZYo2p 4V/FsZhAIVBH0kD2oWDryEoTuVN5k4xF9aQZEWrgSyUBM78Onc9PbnnZy5DOXKm9bd1q AUXg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAW/IpmTWICkgdSrr4+ZUp6WOc2xrPMoq7N5IR0oONg7TSg8nwxo JDX/m4+JjRS9RGTZTPogTuc= X-Google-Smtp-Source: APXvYqxIB/U/720DFw/12opDCaWfPzZw3PYb2aYnComCRDyZZLratb/8XJDIQzpfNREtmmNcJAVKgA== X-Received: by 2002:a05:600c:24d2:: with SMTP id 18mr11449321wmu.117.1556999672114; Sat, 04 May 2019 12:54:32 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:6342:: with SMTP id x63ls2602652wmb.0.canary-gmail; Sat, 04 May 2019 12:54:31 -0700 (PDT) X-Received: by 2002:a1c:c287:: with SMTP id s129mr11126598wmf.63.1556999671448; Sat, 04 May 2019 12:54:31 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1556999671; cv=none; d=google.com; s=arc-20160816; b=X7NM5f9BNPyiGliHA0SFRVIcJH/fXctsaJmcqvQ/YP+xBP12NQ6JE2gpyHKNSOT/nY xUlNGMRCWpu+bQmJvDtiXeUpdWQiEPZbORdXxumndwIOinvb3n4odPngiIda7rzKcLNC jJBdzhJu4txWB6hgAgM/lcPXxbwbS03Y0N8mLurqpKdYcg1nvu5LDiH84CDKczJM5bDp vn5ILgNyCCNaDbc/kIlub7mCM3+Uzrgxz4UrwuTQ6ggdMEQF31hnCYjIlTERJscee2Qz IjZiZG6BVuhf1VE2HYb5Vfy2/Hev/Io5ARavkYCZs7D36Mm7lhEHoO4i4R0fG2H9wtbb 6BuA== 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=oVYYSuulPtZZyrGLyCDaqFN09O68dUIaYvoAw/ma0Kc=; b=BH91O30M8FJ207dGMC9nMEa6lC0koa352S900PH4n5u9kdPW1NXxM1rhyXzeYKFZnf 48ZVR52QobsARV/0B/jJiA6bcQQax3lRpIV7+QJ8Ge4lck5hrOlzKkmkBo4XBI5fVwNx JMqXwffDTys5ap9SohJSkEO05/eiC13UMHyInt/a5gTeP1q4swJO9KoXWqbezwuHAhUg M1ixYrWPEQ40ojzGUYtMv8QFflH5kzPREO616Ycx1PjyPpvGMrdNRpANRYmB/LJNweev ISd+fclnSWOwwGne6dGco6d2kTCz21p5c/sZTyTZXbqojjdycw3ePSOGelGz+Y6tWQoV n4gw== 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 z185si514920wmb.0.2019.05.04.12.54.31 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sat, 04 May 2019 12:54:31 -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 44xKTL5dsBzxfy for ; Sat, 4 May 2019 21:54:30 +0200 (CEST) Received: from smtp.su.se (mail-prod-smtp04.it.su.se [IPv6:2001:6b0:5:132:250:56ff:fe94:2456]) by e-mailfilter01.sunet.se (8.14.4/8.14.4/Debian-8+deb8u2) with ESMTP id x44JsTL1175733 (version=TLSv1/SSLv3 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NO) for ; Sat, 4 May 2019 21:54:30 +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 44xKTK62HQz38SN for ; Sat, 4 May 2019 21:54:29 +0200 (CEST) To: homotopytypetheory From: Erik Palmgren Subject: [HoTT] Second CFP - MLoC 2019 : The Scope and Limits of Neutral Constructivism (Stockholm, August 20-23) Message-ID: <581f8043-a2a4-e9ee-2e45-82b9ee6b8d2f@math.su.se> Date: Sat, 4 May 2019 21:54:29 +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 Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Language: sv Content-Transfer-Encoding: quoted-printable X-Bayes-Prob: 0.9999 (Score 5, tokens from: outbound, outbound-su-se:default, su-se:default, base:default, @@RPTN) X-CanIt-Geo: ip=2001:6b0:5:132:250:56ff:fe94:2456; 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: 0908jStNC - 628ef0804afb - 20190504 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 Second 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 * Hideki Tsuiki, Kyoto University, Japan (to be confirmed) * 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 contributed speakers and/or younger participants. Please write to 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. For more options, visit https://groups.google.com/d/optout.