Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / Atom feed
From: Erik Palmgren <palmgren@math.su.se>
To: homotopytypetheory <homotopytypetheory@googlegroups.com>
Subject: [HoTT] Final CFP - MLoC 2019 : The Scope and Limits of Neutral Constructivism (Stockholm, August 20-23)
Date: Fri, 24 May 2019 18:44:20 +0200
Message-ID: <21fc268e-faf6-01ae-57c5-e3721aef82c3@math.su.se> (raw)
In-Reply-To: <f24e54ff-866b-0640-ebae-e683ddfa753d@math.su.se>


Final Call for Participation and Contributed Papers


Mathematical Logic and Constructivity:

The Scope and Limits of Neutral Constructivism

Stockholm, Sweden, August 20-23, 2019
Deadline for contributed talks:  May 31, 2019


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öf 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

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.


* Douglas S. Bridges, University of Canterbury, Christchurch, New Zealand
* Thierry Coquand, Chalmers and Göteborg 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é Franche-Comté, 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


* Hajime Ishihara, JAIST, Japan
* Anders Mörtberg, Carnegie Mellon University and Stockholm University


Proposals for contributed talks are welcome and are to be submitted
via the EasyChair system:


Suggested length of abstract: half a page.

Deadline for contributed talks:  May 31, 2019 (anywhere on Earth)
Notification of acceptance: June 14, 2019


* Hajime Ishihara, JAIST, Japan (co-chair)
* Tatsuji Kawai, JAIST, Japan
* Peter LeFanu Lumsdaine, Stockholm University
* Anders Mörtberg,  Carnegie Mellon University and Stockholm University
* Erik Palmgren, Stockholm University (co-chair)


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.


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.


Department of Mathematics, Stockholm University, Sweden




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 "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email 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.

           reply index

Thread overview: expand[flat|nested]  mbox.gz  Atom feed
 [parent not found: <f24e54ff-866b-0640-ebae-e683ddfa753d@math.su.se>]

Reply instructions:

You may reply publically to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=21fc268e-faf6-01ae-57c5-e3721aef82c3@math.su.se \
    --to=palmgren@math.su.se \
    --cc=homotopytypetheory@googlegroups.com \


* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link

Discussion of Homotopy Type Theory and Univalent Foundations

Archives are clonable: git clone --mirror http://inbox.vuxu.org/hott

Example config snippet for mirrors

Newsgroup available over NNTP:

AGPL code for this site: git clone https://public-inbox.org/public-inbox.git