- Sam Sanders, On the interplay between Nonstandard Analysis and computability theory
- Chuangjie Xu, Extracting computer programs from nonstandard proofs
- Kenji Miyamoto, Progress report on Minlog's soundness proof generator
- Iosif Petrakis, Constructive uniformities of pseudometrics
- Hajime Ishihara, Versions of the weak Koenig lemma and the disjunctive dependent choice (joint work with Josef Berger and Takako Nemoto)
- Takako Nemoto, Non-deterministic inductive definitions and Fullness
- Tatsuji Kawai, Localic completion of uniform space
- Masahiko Sato, Proof theory of the lambda-calculus

09:00-09:45 Sam Sanders 09:50-10:35 Chuangjie Xu 11:00-11:45 Kenji Miyamoto 11:50-12:35 Iosif Petrakis 14:30-15:15 Hajime Ishihara 15:20-16:05 Takako Nemoto 16:30-17:15 Tatsuji Kawai 17:20-18:05 Masahiko Sato

- Sam Sanders, On the interplay between Nonstandard Analysis and
computability theory

Abstract. We survey recent results on the connection between Nonstandard Analysis (NSA) and computability theory. We present a number of negative and positive results and how they translate back and forth between NSA and computability theory. Of particular interest is how a negative result regarding the axioms of NSA (namely 'Transfer =/=> Standardization') gives rise to two fundamentally different paths from second-order to higher-order mathematics (and the associated notions of computability). -
Chuangjie Xu, Extracting computer programs from nonstandard proofs

Abstract. A constructive fragment of Nelson's Internal Set Theory, namely system H (as it is based on Heyting Arithmetic), has been introduced by van den Berg et al. [1]. We are interested in H because it allows us to obtain computational content from Nonstandard Analysis via a nonstandard variant of the Dialectica interpretation [1]. To extract computer programs from nonstandard proofs, we reformulate the nonstandard Dialectica interpretation in a way that is suitable for a type-theoretic development. Then we embed H within the Agda proof assistant and formalise (parts of) the soundness proof of the Dialectica interpretation of H to obtain Agda programs from proofs in H.

[1] Benno van den Berg, Eyvind Briseid, and Pavol Safarik, A functional interpretation for nonstandard arithmetic, Annals of Pure and Applied Logic 163 (2012), no. 12, 1962?1994. - Kenji Miyamoto, Progress report on Minlog's soundness proof generator

Abstract: I am going to report the progress of the implementation of Minlog's soundness proof generator. Within the behind theory of Minlog, the soundness theorem of program extraction claims that for a given constructive proof M of a formula A, there exists another proof M', so-called a soundness proof, concluding that the program extracted from M is a realizer of A. Based on this theorem, Minlog can automatically generates soundness proofs, but not yet for all proofs in the theory. I talk about the recent work in order to extend this feature to support coinductive proofs. - Hajime Ishihara, Versions of the weak Koenig lemma and the disjunctive
dependent choice

Abstract. The weak Koenig lemma (WKL) is equivalent to the disjunctive dependent choice for $\Pi^0_1$ formulae and the lesser limited principle of omniscience (LLOP). We will look into a proof of the equivalence, and adoptations of it for the equivalences between WKL for trees having at most two nodes at each level and a version of the disjunctive dependent choice with LLPO, and between WKL for convex trees and another version of the disjunctive dependent choice with LLPO. - Iosif Petrakis, Constructive uniformities of pseudometrics

Abstract. We show how the theory of uniform spaces the uniformities of which are defined through pseudometrics can be developed in the same system and in a similar way to the theory of Bishop spaces. We also discuss the interplay between these two approaches to constructive function-theoretic topology. - Takako Nemoto, Non-deterministic inductive definitions and Fullness.

Abstract. We consider the non-deterministic inductive definition principle NID with the weak notion of a set-generated class introduced by van den Berg [2] and with the strong notion of a set-generated class adopted by Aczel et al. [1]. We introduce a principle, called nullary NID, and prove that nullary NID is equivalent to Fullness in a subsystem of the constructive Zermelo-Fraenkel set theory.

[1] Peter Aczel, Hajime Ishihara, Takako Nemoto and Yasushi Sangu, Generalized geometric theories and set-generated classes, Mathematical Structures Computer Science, Volume 25, Issue 7 (Computing with Infinite Data: Topological and Logical Foundations Part 1) October 2015, pp. 1466-1483

[2] Benno van den Berg, Non-deterministic inductive definitions, Archive for Mathematical Logic Volume 52, Issue 1, pp. 113-135 - Tatsuji Kawai, Localic completion of uniform space

Abstract. We extend the localic completion of generalised metric spaces by Steven Vickers to the setting of uniform spaces defined via family of pseudometrics. In particular, the localic completion gives rise to an embedding of Bishop's locally compact uniform spaces into formal topologies. As a by-product, the localic completion gives predicative completions of uniform spaces. - Masahiko Sato, Proof theory of the lambda-calculus

Abstract. We develop a proof theory of the lambda-calculus where we study the set of closed lambda terms by inductively defining the set as a free algebra. The novelty of the approach is that we construct and study lambda-calculus without using the notions of variables and alpha-equivalence. In this approach we can study lambda-terms as combinators and can have a clean proof of the Church-Rosser Theorem in the Minlog proof assistant. This is a joint work with Helmut Schwichtenberg and Takafumi Sakurai.

Helmut Schwichtenberg

Last change: 11. October 2016