The seminar below is held as a part of JSPS Core-to-Core Program,
A. Advanced Research Networks, and EU FP7 Marie Curie Actions IRSES project CORCON. (http://www.jaist.ac.jp/logic/ja/core2core, https://corcon.net/)
Wednesday 28 September, 2016, 15:20-17:00 in JAIST, Collaboration room 7 (I-56)
Dr Chuangjie Xu (Ludwig-Maximilians-Universität München) Continuity in Type Theory
If all functions (N -> N) -> N are continuous then 0 = 1. We
establish this in intuitionistic type theory, with existence in the
formulation of continuity expressed as a Sigma-type via the
Curry-Howard interpretation. But with an intuitionistic notion of
anonymous existence, defined as the propositional truncation of
Sigma, it is consistent that all such functions are continuous. On
the other hand, any of these two intuitionistic conceptions of
existence give the same, consistent, notion of uniform continuity
for functions (N -> 2) -> N. Moreover, we constructively develop a
model of uniform continuity and implemented it within type theory
Unfortunately, Professor Erik Palmgren (Department of Mathematics, Stockholm University) cannot come to JAIST in March 2015, so the previously announced seminars have been cancelled.
In the JAIST Logic Seminar Series, Professor Erik Palmgren (Department of Mathematics, Stockholm University) will give a series of lectures:
Lectures on type theory with a view towards formalizing Bishop-style mathematics
In this series of three lectures we give an introduction to Martin-Lof type theory and the tools it provides for formalizing Bishop-style constructive mathematics.
The first lecture will cover basic principles of type theory and give an introduction to its manifestation in the well-known proof assistant Coq.
In the second lecture we consider “Bishop’s set theory” (Bishop and Bridges 1985) from the point of view of type theory, which will involve a development the theory of setoids and subsetoids.
The third lecture will cover models constructive set theory (CZF) in type theory, and how it can be used to solve the problem of universes of setoids and development of category theory.
Throughout the lectures we provide examples and suggestions how you can yourself experiment with the Coq system in the formalization of constructive mathematics.
E. Bishop and D.S. Bridges. Constructive Analysis. Springer 1985.
E. Palmgren. Lecture notes on Type Theory. Stockholm 2014.
E. Palmgren and O. Wilander. Constructing categories and setoids of setoids in type theory. Logical Methods in Computer Science. 10(2014), Issue 3, paper 25.
Lecture 1. Monday 9 March, 2015, 15:10-16:40
Lecture 2. Tuesday 10 March, 2015, 15:10-16:40
Lecture 3. Wednesday 11 March, 2015, 15:10-16:40
All the lectures will take place at JAIST, Lecture room I3-I4
Thanks to our kind colleagues in JAIST, we would like to signal to whoever may be interested this opportunity for further cooperation under the themes of the CORCON project:
If interested, feel free to contact Professor Ishihara at the Japan Advanced Institute for Science and Technology.
JAIST Logic Workshop Series 2015:
Constructivism and Computability
Shiinoki Cultural Complex, Kanazawa, Japan
2 March 2015 – 6 March 2015
Toshiyasu Arai (Chiba University)
Andrej Bauer (University of Ljubljana)
Ulrich Berger (Swansea University)
Hajime Ishihara (JAIST)
Masahiro Kumabe (Open University of Japan)
Erik Palmgren (Stockholm University)
Peter Schuster (University of Leeds)
Helmut Schwichtenberg (LMU Munich)
Dieter Spreen (University of Siegen, UNISA Pretoria)
Kazuyuki Tanaka (Tohoku University) (to be confirmed)
Hajime Ishihara (JAIST)
Takayuki Kihara (JAIST)
Takako Nemoto (JAIST)
Keita Yokoyama (JAIST)
JAIST Logic Workshop Series is a workshop series bringing together researchers from mathematical logic and its application, especially to artificial intelligence and software science. Each workshop has its own focus on a specific area of research in mathematical logic and its application. Previous workshops have been held in Kanazawa 2013, 2014 and 2014:
In 2015, JAIST Logic Workshop Series focuses on “Constructivism and Computability” aiming at interaction and knowledge transfer between constructive mathematics and computability theory. The workshop is held being affiliated with EU FP7 Marie Curie Actions IRSES projects COMPUTAL (http://computal.uni-trier.de/) and CORCON (https://corcon.net/), but is open to all researchers in the areas.
constructive mathematics including intuitionistic logic and type theory, proof theory, constructive analysis and topology, program extraction from proofs, constructive reverse mathematics etc., and computability theory including recursion theory, computable analysis and topology, real number computation, reverse mathematics, algorithmic randomness etc.
On Friday, June 27th, Dr John Stell from the University of Leeds, UK, will give a talk at JAIST.
Bi-Intuitionistic Modal Logic and Hypergraphs
I will discuss motivations from spatial reasoning and mathematical morphology (as used in image processing) for the notion of a relation on a graph. I will show how the algebra of these relations is weaker than that of relations on a set. This leads to a generalization of relation algebras in which the Boolean algebra is replaced by a symmetric Heyting algebra.
These relations can be used as the accessibility relations for a modal logic in which propositions are interpreted as subgraphs of a graph or more generally a hypergraph.
Thanks to Neil Ghani, we would like to signal the workshop
Workshop on Applications on Fibrations in Computer Science
University of Strathclyde, June 23-24, 2014
which is strictly related to the themes of the CORCON project.