All posts by Marco Benini

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. (,

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

Seminars in JAIST

JAIST Logic Seminar Series

The lectures 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.

On Tuesday 6 September, 2016, 13:30-17:00, JAIST, Lecture room I2

Josef Berger (Ludwig-Maximilians-Universität München), The fan theorem and convexity (joint work with Gregor Svindland)

The fan theorem is the following statement: (FAN) Let B be a decidable set of finite binary sequences. Assume that every infinite binary sequence has an initial part that belongs to B. Then there exist an N such that  every infinite binary sequence has an initial part of length smaller than N that belongs to B.

This axiom plays an important role in Intuitionism, a philosophy of mathematics that was introduced by the Dutch mathematician L.E.J. Brouwer. We work in constructive mathematics in the tradition of Errett Bishop. Here, the fan theorem is neither provable nor falsifiable. Many theorems of analysis are equivalent to the fan theorem. One example for such a theorem is: (POS) Every positive-valued uniformly continuous function on the unit interval has positive infimum.

In our paper Convexity and constructive infamy we have shown that, under the additional condition of convexity of the function, POS is constructively valid.

In this talk, we discuss to which extent this gives rise to a notion of  convex bars and a corresponding constructively valid convex fan theorem.

Anton Setzer and Bashar Igried (Swansea University) Coinductive Reasoning in Dependent Type Theory – Copatterns, Objects, Processes (part on Processes joint work with Bashar Igried)

When working in logic in computer science, one is very often confronted with bisimulation. The reason for its importance is that in computer science, one often reasons about interactive or concurrent programs. Such programs can have infinite execution paths, and therefore correspond to coinductive data types. The natural equality on coinductive data types is bisimulation. Proofs of bisimulation form one of the main principles for reasoning about coinductive data types.

However, bisimulation is often very difficult to understand and to teach. This is in contrast to the principle of induction, where there exists a well established tradition of carrying out proofs by induction. One goal of this talk is to demonstrate that one can reason about coinductive data types in a similar way as one can reason inductively about inductive data types.

Reasoning about inductive data types can be done by pattern matching. For instance for reasoning about natural numbers one makes a case distinction on whether the argument is 0 or a successor. For coinductive data types the dual is copattern matching, which is essentially a case distinction on the observations one can make for a coinductively defined set. For instance, streams have observations head and tail, and one can introduce a stream by determining its head and its tail.

We then look at examples of the use of coinductive data types. One is the notion of an object, as it occurs in object-oriented program. Objects are defined by their method calls, which are observations, so they are defined coinductively. The final example will be the representation of processes in dependent type theory, where we will refer to the process algebra CSP.

Seminars in JAIST

The JAIST Logic Seminar series will host the following seminars in August 2016.

The seminars below are held as a part of JSPS Core-to-Core Program, A. Advanced Research Networks, and EU FP7 Marie Curie Actions IRSES project CORCON.

  • Tuesday 2 August, 2016, 13:30-15:10
    Eugenio Moggi (University of Genova)
    Categories of Classes for Collection Types
    Collection types have been proposed by Buneman and others (in the ’90) as a way to capture database query languages in a typed setting. In 1998 Manes introduced the notion of collection monad on the category S of sets as a suitable semantics for collection types. The canonical example of collection monad is the finite powerset monad Pf. In order to account for the algorithmic aspects of database languages, the category S is unsuitable, and should be replaced with other categories, whose arrows are maps computable by “low complexity” algorithms. We propose “realizability for DSL” (Domain Specific Languages), where the starting point is a monoid C of endomaps on a set D, instead of a combinatory algebra on D, as a way to get such categories by constructions like the category A[C] of “assemblies”. To get Pf in a systematic way we borrow ideas from AST (Algebraic Set Theory, started by Joyal and Moerdijk in the ’90), where they fix a notion of “small” map in a category of “classes”, and read “small” as “finite”.
  • Thursday 4 August, 2016, 13:30-15:10
    Eugenio Moggi (University of Genova)
    Hybrid System Trajectories as Partial Continuous Maps
    Hybrid systems (HS) are dynamic systems that exhibit both continuous and discrete dynamic behavior: they can flow (according to a differential equation) and jump (according to a transition relation). HS can be used for modeling rigid body dynamics with impacts, and more generally Cyber-Physical Systems. HS can exhibit Zeno behaviors, that arise naturally in rigid body dynamics with impacts, but are absent from purely discrete or purely continuous systems. Dealing properly with these behaviors is a prerequisite to give sound definitions of concepts such as reachability. We propose the use of partial continuous maps (PCM) as trajectories that describe how a HS evolves over time. PCMs enable a notion of trajectory that can go beyond Zeno points.
  • Friday 5 August, 2016, 10:50-12:30
    Eugenio Moggi (University of Genova)
    Models, Over-approximations and Robustness
    Hybrid systems, and related formalisms, have been successfully  used to model Cyber-Physical Systems. The usual definition of “reachability”, in terms of the reflexive and transitive closure of a transition relation, is unsound for Zeno systems. We propose “safe reachability”, which gives an over-approximation of the set of states that are “reachable in finite time” from a set of initial states. Moreover, mathematical models are always a simplification of the system they are meant to describe, and one must be aware of this mismatch, when using these models for system analyses. In safety analysis it is acceptable to use over-approximations of the system behavior, indeed they are the bread and butter of counterexample guided abstraction refinement (CEGAR). We propose a notion of safe (time-bounded) reachability, which is also robust wrt arbitrary small overapproximations, and argue that it is particularly appropriate for safety analysis.
  • Monday 8 August, 2016, 13:30-15:10, JAIST, Collaboration room 7 (I-56)
    Marco Benini (University of Insubria)
    Variations on the Higman’s Lemma
    The Higman’s Lemma says that if A is a well-quasi-order, so is the set of finite sequences over A with the order induced by embedding. By considering the structure of the categories of well-founded quasi-orders and well-quasi-orders, another proof of the Lemma will be derived, along with a number of variants, which may be of some interest.
  • Thursday 25 August, 2016, 13:30-15:10
    Helmut Schwichtenberg (Ludwig-Maximilians-Universität München)
    Invariance axioms for realizability
    Kolmogorov (1932) proposed to consider mathematical formulas as problems asking for solutions. Following this idea it seems reasonable to extend arithmetical theories by adding invariance axioms, which state that every formula is equivalent to the (internal) formula stating that it has a realizer. We sketch such a theory, which in addition allows to fine-tune the computational content of proofs by decorations of the logical connectives. A soundness theorem holds.

Seminar announcement

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

JSPS Fellowships for Research in Japan

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.

Workshop announcement

JAIST Logic Workshop Series 2015:
Constructivism and Computability
Shiinoki Cultural Complex, Kanazawa, Japan
2 March 2015 – 6 March 2015

Programme Committee:
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)

Local Organizers:
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 ( and CORCON (, 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.

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.