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,HTML_MESSAGE, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-ed1-x53b.google.com (mail-ed1-x53b.google.com [IPv6:2a00:1450:4864:20::53b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 6a5f0001 for ; Tue, 2 Apr 2019 13:26:37 +0000 (UTC) Received: by mail-ed1-x53b.google.com with SMTP id k8sf5852555edl.22 for ; Tue, 02 Apr 2019 06:26:37 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1554211596; cv=pass; d=google.com; s=arc-20160816; b=1CxmubYZUqCk9FpmHyMJRR6eVsgtKPddC4Tm6H5eCevsnOXlhI7KE/7g8bKgbpKxKl NIKtw085GMvd0j9MuatME+sxnjJ/hHEve1BaYtiwZioF3Av5FQ2W7hXd82IQ7pwxdrii 3XDqTgH6h3f1P68sWe7s1zoOuP+6Cn+fSwVXNgnr/i1LaHqYWWUPglxHCq7YZrZlKqPt Ig4FlJR5xbCbJHql/VQdEekDwkUMhu0N37IJSrYo+6jxI6OHwrbG437WBKO8+02dB+i1 ylX8vJKPfV0GnrZPakEMOG39VgPHG56p3iIUk+jPYMmyVjzl3ujYeSa8537j39nT6vQM q+DA== 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:mime-version:content-language :accept-language:message-id:date:thread-index:thread-topic:subject :to:from:sender:dkim-signature; bh=Bi/lRLbkLtnpgp2mUHrHKqltkTEerkrcjaThWkgNOTE=; b=AZKCGYs02dONzyAlbOQgraTNfBTqh+G2Djx6U8cUt456OY2vaxSlizsgkPQrxWPaJL 4FnED6H6+FfkyjFmJ4tN8cPWH3qx8bE4+ESZAOI1bBwTpAa81w9x3wt4JtXNCd+GwkmR 5Ya3XoxyO/I6/XPJrpdh80wJzkqOA7OI4OpvmiNH1uNeyNYLj06GjI3l9AT6IzCaLp+D i5Aw0j1qH/+9BVampObLF/k2sWD3KaEryGU3cVdIIovy/EMbozHqS4gfH/k+I08/HwZ0 XJsU56gPADN8oG7H1B++IfVs4hgY03fbWyeZAaLawmzy78SjZNreDWI+l4Z/k7nC+oFd 5QIw== 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:from:to:subject:thread-topic:thread-index:date:message-id :accept-language:content-language:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=Bi/lRLbkLtnpgp2mUHrHKqltkTEerkrcjaThWkgNOTE=; b=OpGTczJ1qYjFjxxB7r0DfnkusWOBqoKTU9RIO/6oKfWcJUuZcfcDfwNZpJy0LAd7XO RAXrx2GT0QzFlbq3k73cS4/K27sS/hzt5SRCJVSgKXsivYqi7V7FQNPiV8XJky2UIagl QjLfembCyxGQ4kEYmu+Iyn1G8yhQ9ljqcIt4hJBHhvvY9yPlgvoHRGuRZcmCPqCgs1PZ i6mywLuL9PgjFcCCHVyfea2UezXuk83n2ll+RvjsOIhBR5LwJqcmYQxOBWxv5X0w1XeG 8ZfbqZ51TyxDQQN+QYy+SOlv1w/0PysbSiSnDmhLEf7B2zkGxJ+fxMKzrvHtqZcqkV45 yAqQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:subject:thread-topic:thread-index :date:message-id:accept-language:content-language:mime-version :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=Bi/lRLbkLtnpgp2mUHrHKqltkTEerkrcjaThWkgNOTE=; b=gTCUOCCA3gNFxvM2Er87GZXRN4K7x5AO3qs+bIoDiVeLH4AWq2J6wxuWHHq4zdihBc lLTYyaz4fEugl25AEMZjhxz6KNIR37YGkyLFVpzXTtBe2s9/FLd8s+g28FXTgi6qiCX+ SLYJvcZflwn2igwfg+g4SUohCF3V+imZ9Go9AvpCooKas+sc4hfprWWC3PlHGJTQuT+Y mXSOjBcvjjgXGWxBQP3UuOFzQAHx7D5iYkqHVSq0oEI3ZHId3STo883iBX7IeYG32z8m QPkO/CmzeLK2EnlTq4wPyDrSz5kWQMl7HnzvMo21Gvk/Hv/HZcBnk4c39AlUeu6Z8Wj/ zJDQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXAWva6Uj4P93zU5v6xdzikSkL6s7+pfTOEa5GROJU+RbyB3DUR AvGjOG7KkdEopyhGpns10XE= X-Google-Smtp-Source: APXvYqwPgp3w/HXD/defKpfK6/gxc/QiD2VpyGjohk9qomh61WcCVwYnLWpRGJQ1L7xJ02JhgeyujA== X-Received: by 2002:a17:906:641:: with SMTP id t1mr21360397ejb.158.1554211596617; Tue, 02 Apr 2019 06:26:36 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a50:8ebb:: with SMTP id w56ls3631902edw.2.gmail; Tue, 02 Apr 2019 06:26:36 -0700 (PDT) X-Received: by 2002:a50:928a:: with SMTP id k10mr5052087eda.10.1554211595961; Tue, 02 Apr 2019 06:26:35 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1554211595; cv=none; d=google.com; s=arc-20160816; b=umJ4whWSyTKcTSB7OaDWhGYpc5+Jx//HbYnCqOAE/iJh5hugGxvUEEpvxjLBvdZBU4 LpPX3Xm42w7UMvu3FSeRMfiAePi3WMAFO3scEDJ5BImmfRqZQiEDo/MmmOk/PNjhB9Mj nd8gyY3cbkGe0BpsRDnk5AXRx7g4rS/a+IVho6GcX0sXC4PF8ag6ku7t5HceBaYplTcd av3PgjkNiLhHIX5gsGGJpqDaQ6CHzEy6JvaFmfKwJ22oho2K2MWoebaWhMaLX0n8ZoqB y1BDzFqLCmB+I5regqkLb6PaCJZGuQFmALfYiHrUtR9v0gVqCz9tmMExvUnZ5DzuDKj0 eNXA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-language:accept-language:message-id:date :thread-index:thread-topic:subject:to:from; bh=x7ZNm4flRTRzCqT5oAcmqWsVbWZ4Bmwr5aI5d2lkkMY=; b=ypB4VC/30rkCcNEev8imT7BTtyYoSH6Y24hFnJO4z0YHzqtbh5b1bsAMYHdzDi7AH8 sJLoYGlFMAbj7epRHGCU9JDDBnPTffuCfKQt30eWUSDCJW8nr3+7by7oErtLlUFECDC3 4iScpZE9y4vTIvlcPu0ihtqzAiE6p/IqVv0JRBW/idw+wcsElHDrX8GCzX3N5PIr8SOA oLcvrAW+Z2nxnExkbmjU8ZguI0WfhvtGPvm3iuhcNMtfx7fHdie66KcBTwPS/rRYk/GF 8lxmJk+QS+8R6c4/dQRrmlzRpBfRnQk+6rWlxrVMfGFD2iHYIavjtXWaXKmwcSMrHdkP b1eQ== 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 ck11si532642ejb.0.2019.04.02.06.26.35 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 02 Apr 2019 06:26:35 -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-mailfilter02.sunet.se (e-mailfilter02.sunet.se [IPv6:2001:6b0:8:2::202]) (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 44YVNW2jlBzxcJ for ; Tue, 2 Apr 2019 15:26:35 +0200 (CEST) Received: from smtp.su.se (mail-prod-smtp03.it.su.se [130.237.181.83]) by e-mailfilter02.sunet.se (8.14.4/8.14.4/Debian-8+deb8u2) with ESMTP id x32DQYVt051424 (version=TLSv1/SSLv3 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NO) for ; Tue, 2 Apr 2019 15:26:34 +0200 Received: from EBOX-PROD-SRV14.win.su.se (unknown [IPv6:2001:6b0:5:1162:10ee:1df:f550:9b8d]) by smtp.su.se (Postfix) with ESMTPS id 44YVNV1b7pzxbN for ; Tue, 2 Apr 2019 15:26:34 +0200 (CEST) Received: from ebox-prod-srv13.win.su.se (2001:6b0:5:1162:f071:3d85:b2d0:c2f6) by EBOX-PROD-SRV14.win.su.se (2001:6b0:5:1162:10ee:1df:f550:9b8d) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256) id 15.1.1713.5; Tue, 2 Apr 2019 15:26:33 +0200 Received: from ebox-prod-srv13.win.su.se ([fe80::f071:3d85:b2d0:c2f6]) by ebox-prod-srv13.win.su.se ([fe80::f071:3d85:b2d0:c2f6%2]) with mapi id 15.01.1713.004; Tue, 2 Apr 2019 15:26:33 +0200 From: Erik Palmgren To: "homotopytypetheory@googlegroups.com" Subject: [HoTT] MLoC 2019: Mathematical Logic and Constructivity, Stockholm (Sweden), Aug 20-23, 2019 Thread-Topic: MLoC 2019: Mathematical Logic and Constructivity, Stockholm (Sweden), Aug 20-23, 2019 Thread-Index: AQHU6VewllrkmoujSki9Ewb6NhHmig== Date: Tue, 2 Apr 2019 13:26:33 +0000 Message-ID: <34403B87-4966-4C69-924A-876E440FEE45@math.su.se> Accept-Language: sv-SE, en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-mailer: Apple Mail (2.3124) x-originating-ip: [130.237.154.251] Content-Type: multipart/alternative; boundary="_000_34403B8749664C69924A876E440FEE45mathsuse_" MIME-Version: 1.0 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.83; 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: 0aXTpqyKE - 2d35a8582778 - 20190402 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: , --_000_34403B8749664C69924A876E440FEE45mathsuse_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable =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 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, Waseda University, 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 (max 2 pages). 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. 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. --_000_34403B8749664C69924A876E440FEE45mathsuse_ Content-Type: text/html; charset="UTF-8" Content-ID: Content-Transfer-Encoding: quoted-printable
=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

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 als= o
be studied for systems that make fewer ontological assumptions, which
is important for reverse mathematics.   To the surprise of many i= n
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, Waseda University, 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:

htt= ps://easychair.org/conferences/?conf=3Dmloc19

Suggested length of abstract: half a page (max 2 pages).

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 Univ= ersity
* 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.

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

--
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.
For more options, visit http= s://groups.google.com/d/optout.
--_000_34403B8749664C69924A876E440FEE45mathsuse_--