Tag Archives: Talk

Seminars in JAIST

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)
(Access: http://www.jaist.ac.jp/english/location/access.html)

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
using Agda.

Talk announcement

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.